From 8b3d513dc48d4d6a24948bef34528ef7ffd5058b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 5 Dec 2022 18:22:53 +0100
Subject: [PATCH] [server] registering type markers
---
ivette/src/frama-c/richtext.tsx | 8 ++++++--
src/plugins/server/kernel_ast.ml | 7 ++++++-
src/plugins/server/kernel_ast.mli | 1 +
3 files changed, 13 insertions(+), 3 deletions(-)
diff --git a/ivette/src/frama-c/richtext.tsx b/ivette/src/frama-c/richtext.tsx
index 5f35ba83508..f819ccae152 100644
--- a/ivette/src/frama-c/richtext.tsx
+++ b/ivette/src/frama-c/richtext.tsx
@@ -83,7 +83,7 @@ interface MarkerProps {
function Marker(props: MarkerProps): JSX.Element {
const { marker, onMarker, children } = props;
- const onClick = (): void => {if (onMarker) onMarker(marker);};
+ const onClick = (): void => { if (onMarker) onMarker(marker); };
return (
<span
className="kernel-text-marker"
@@ -109,7 +109,11 @@ export function Text(props: TextProps): JSX.Element {
const array = marker ? text.slice(1) : text;
const contents = React.Children.toArray(array.map(makeContents));
if (marker) {
- return <Marker marker={tag} onMarker={props.onMarker}>{contents}</Marker>;
+ return (
+ <Marker marker={tag} onMarker={props.onMarker}>
+ {contents}
+ </Marker>
+ );
}
return <>{contents}</>;
} if (typeof text === 'string') {
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index f24c0839196..170fafd311e 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -336,6 +336,7 @@ struct
let jterm = jmarker "term"
let jglobal = jmarker "global"
let jproperty = jmarker "property"
+ let jtyp = jmarker "type"
let jtype = Data.declare ~package ~name:"marker"
~descr:(Md.plain "Localizable AST markers")
@@ -427,6 +428,7 @@ end
module KfMarker = struct
type record
let record : record Record.signature = Record.signature ()
+
let fct = Record.field record ~name:"fct"
~descr:(Md.plain "Function") (module Kf)
let marker = Record.field record ~name:"marker"
@@ -435,6 +437,7 @@ module KfMarker = struct
let data =
Record.publish ~package ~name:"location"
~descr:(Md.plain "Location: function and marker") record
+
module R : Record.S with type r = record = (val data)
type t = kernel_function * Printer_tag.localizable
let jtype = R.jtype
@@ -647,7 +650,9 @@ struct
let update () = Request.emit signal
- let register ~id ~label ~descr ?(title = descr) ?(enable = fun _ -> true) pretty =
+ let register ~id ~label ~descr
+ ?(title = descr)
+ ?(enable = fun _ -> true) pretty =
let rank = incr rankId ; !rankId in
let info = { id ; rank ; label ; descr; title ; enable ; pretty } in
if Hashtbl.mem registry id then
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 7379bff9e5c..1ffebc5e66f 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -46,6 +46,7 @@ sig
val jterm : jtype
val jglobal : jtype
val jproperty : jtype
+ val jtyp : jtype
val create : t -> string
(** Memoized unique identifier. *)
--
GitLab