From a405cbced27ad3c47e5f209216739b2f51179150 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 22 Oct 2021 19:24:18 +0200
Subject: [PATCH] [server] Adds request getMarkerAt returning the marker at a
given file position.
---
.../frama-c/api/generated/kernel/ast/index.ts | 21 ++++++++++++++++
src/plugins/server/kernel_ast.ml | 25 +++++++++++++++++++
2 files changed, 46 insertions(+)
diff --git a/ivette/src/frama-c/api/generated/kernel/ast/index.ts b/ivette/src/frama-c/api/generated/kernel/ast/index.ts
index 89d14dc6e85..e971013dd12 100644
--- a/ivette/src/frama-c/api/generated/kernel/ast/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/ast/index.ts
@@ -468,6 +468,27 @@ const getInfo_internal: Server.GetRequest<marker,text> = {
/** Get textual information about a marker */
export const getInfo: Server.GetRequest<marker,text>= getInfo_internal;
+const getMarkerAt_internal: Server.GetRequest<
+ [ string, number, number ],
+ [ Json.key<'#fct'> | undefined, marker | undefined ]
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.getMarkerAt',
+ input: Json.jTry(
+ Json.jTriple(
+ Json.jFail(Json.jString,'String expected'),
+ Json.jFail(Json.jNumber,'Number expected'),
+ Json.jFail(Json.jNumber,'Number expected'),
+ )),
+ output: Json.jTry(Json.jPair( Json.jKey<'#fct'>('#fct'), jMarker,)),
+ signals: [],
+};
+/** Returns the marker and function at a source file position, if any. Input: file path, line and column. */
+export const getMarkerAt: Server.GetRequest<
+ [ string, number, number ],
+ [ Json.key<'#fct'> | undefined, marker | undefined ]
+ >= getMarkerAt_internal;
+
const getFiles_internal: Server.GetRequest<null,string[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getFiles',
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index d130f00bdd8..916a1277ace 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -612,6 +612,31 @@ let () = Request.register ~package
~input:(module Marker) ~output:(module Jtext)
Info.get_marker_info
+(* -------------------------------------------------------------------------- *)
+(* --- Marker at a position --- *)
+(* -------------------------------------------------------------------------- *)
+
+let get_kf_marker (file, line, col) =
+ let pos_path = Filepath.Normalized.of_string file in
+ let pos =
+ Filepath.{ pos_path; pos_lnum = line; pos_cnum = col; pos_bol = 0; }
+ in
+ let tag = Printer_tag.loc_to_localizable ~precise_col:true pos in
+ let kf = Option.bind tag Printer_tag.kf_of_localizable in
+ kf, tag
+
+let () =
+ let descr =
+ Md.plain
+ "Returns the marker and function at a source file position, if any. \
+ Input: file path, line and column."
+ in
+ Request.register
+ ~package ~descr ~kind:`GET ~name:"getMarkerAt"
+ ~input:(module Jtriple (Jstring) (Jint) (Jint))
+ ~output:(module Jpair (Joption (Kf)) (Joption (Marker)))
+ get_kf_marker
+
(* -------------------------------------------------------------------------- *)
(* --- Files --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab