diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 3868f9d799dc6a5b0e15bb248aae35e4ec5705da..b2d3c354e9c9396a29a5fe36b6ab6343bc6e377f 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -240,6 +240,32 @@ struct with Not_found -> Data.failure "Undefined function '%s'" key end +module KfMarker = struct + type record + let record : record Record.signature = Record.signature () + let fct = Record.field record ~name:"function" + ~descr:(Md.plain "Function") (module Kf) + let marker = Record.field record ~name:"marker" + ~descr:(Md.plain "Marker") (module Marker) + + 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 + + let to_json (kf, loc) = + R.default |> + R.set fct kf |> + R.set marker loc |> + R.to_json + + let of_json json = + let r = R.of_json json in + R.get fct r, R.get marker r +end + (* -------------------------------------------------------------------------- *) (* --- Functions --- *) (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli index c0d3d0ff73090d3c5c7d839b3494ba4fe4dbe259..6832e10f4ed79ccfd685b8bd8f966de80c09bd63 100644 --- a/src/plugins/server/kernel_ast.mli +++ b/src/plugins/server/kernel_ast.mli @@ -47,6 +47,8 @@ sig val lookup : string -> t (** Get back the localizable, if any. *) end +module KfMarker : Data.S with type t = kernel_function * Printer_tag.localizable + (* -------------------------------------------------------------------------- *) (** Ast Printer *) (* -------------------------------------------------------------------------- *)