[stm] Switch to a functional API

We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.

For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.

Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.

2 files changed, 24 insertions, 14 deletions

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 54d16a9be3..7a126363cc 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -15,6 +15,7 @@ type level =
   | Warning
   | Error
 
+type doc_id = int
 type route_id = int
 
 type feedback_content =
@@ -35,7 +36,8 @@ type feedback_content =
   | Message of level * Loc.t option * Pp.t
 
 type feedback = {
-  id       : Stateid.t;
+  doc_id   : doc_id;            (* The document being concerned *)
+  span_id  : Stateid.t;
   route    : route_id;
   contents : feedback_content;
 }
@@ -52,23 +54,27 @@ let add_feeder =
 let del_feeder fid = Hashtbl.remove feeders fid
 
 let default_route = 0
-let feedback_id    = ref Stateid.dummy
+let span_id    = ref Stateid.dummy
+let doc_id     = ref 0
 let feedback_route = ref default_route
 
-let set_id_for_feedback ?(route=default_route) i =
-  feedback_id := i; feedback_route := route
+let set_id_for_feedback ?(route=default_route) d i =
+  doc_id := d;
+  span_id := i;
+  feedback_route := route
 
-let feedback ?id ?route what =
+let feedback ?did ?id ?route what =
   let m = {
      contents = what;
-     route = Option.default !feedback_route route;
-     id    = Option.default !feedback_id id;
+     route    = Option.default !feedback_route route;
+     doc_id   = Option.default !doc_id did;
+     span_id  = Option.default !span_id id;
   } in
   Hashtbl.iter (fun _ f -> f m) feeders
 
 (* Logging messages *)
 let feedback_logger ?loc lvl msg =
-  feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, msg))
+  feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, msg))
 
 let msg_info    ?loc x = feedback_logger ?loc Info x
 let msg_notice  ?loc x = feedback_logger ?loc Notice x
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 45a02d384a..73b84614f1 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -17,6 +17,9 @@ type level =
   | Error
 
 
+(** Document unique identifier for serialization *)
+type doc_id = int
+
 (** Coq "semantic" infos obtained during execution *)
 type route_id = int
 
@@ -43,7 +46,8 @@ type feedback_content =
   | Message of level * Loc.t option * Pp.t
 
 type feedback = {
-  id       : Stateid.t;         (* The document part concerned *)
+  doc_id   : doc_id;            (* The document being concerned *)
+  span_id  : Stateid.t;         (* The document part concerned *)
   route    : route_id;          (* Extra routing info *)
   contents : feedback_content;  (* The payload *)
 }
@@ -60,13 +64,13 @@ val add_feeder : (feedback -> unit) -> int
 (** [del_feeder fid] removes the feeder with id [fid] *)
 val del_feeder : int -> unit
 
-(** [feedback ?id ?route fb] produces feedback fb, with [route] and
-    [id] set appropiatedly, if absent, it will use the defaults set by
-    [set_id_for_feedback] *)
-val feedback : ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
+(** [feedback ?did ?sid ?route fb] produces feedback [fb], with
+    [route] and [did, sid] set appropiatedly, if absent, it will use
+    the defaults set by [set_id_for_feedback] *)
+val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
 
 (** [set_id_for_feedback route id] Set the defaults for feedback *)
-val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit
+val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit
 
 (** {6 output functions}