From b9d43a8a16771b2464c59e6c4a33fe3c5c1e98e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 21 Mar 2022 14:53:32 +0100
Subject: [PATCH] [server] Adds the location in marker informations.
---
src/plugins/server/kernel_ast.ml | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 8693bbf3113..f9fadabefdc 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -640,6 +640,15 @@ let () = Request.register ~package
(* --- Default Kernel Informations --- *)
(* -------------------------------------------------------------------------- *)
+let () = Informations.register
+ ~id:"kernel.ast.location"
+ ~label:"Location"
+ ~title:"Source file location"
+ begin fun fmt loc ->
+ let location = Printer_tag.loc_of_localizable loc in
+ Filepath.pp_pos fmt (fst location)
+ end
+
let () = Informations.register
~id:"kernel.ast.varinfo"
~label:"Var"
--
GitLab