[stm] Remove edit_id.

We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.

Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.

XML protocol clients are unaffected, they rely on the instead on the
Fail value.

This commit supersedes PR#203.

4 files changed, 11 insertions, 21 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 45b5a1007..15150dce9 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -415,11 +415,7 @@ object(self)
     buffer#apply_tag Tags.Script.tooltip ~start ~stop;
     add_tooltip sentence pre post markup
 
-  method private is_dummy_id id =
-    match id with
-    | Edit 0 -> true
-    | State id when Stateid.equal id Stateid.dummy -> true
-    | _ -> false
+  method private is_dummy_id id = Stateid.equal id Stateid.dummy
 
   method private enqueue_feedback msg =
     (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *)
@@ -434,8 +430,7 @@ object(self)
       let sentence =
         let finder _ state_id s =
           match state_id, id with
-          | Some id', State id when Stateid.equal id id' -> Some (state_id, s)
-          | _, Edit id when id = s.edit_id -> Some (state_id, s)
+          | Some id', id when Stateid.equal id id' -> Some (state_id, s)
           | _ -> None in
         try Some (Doc.find_map document finder)
         with Not_found -> None in
@@ -505,8 +500,7 @@ object(self)
           else
             try
               match id, Doc.tip document with
-              | Edit _, _ -> ()
-              | State id1, id2 when Stateid.newer_than id2 id1 -> ()
+              | id1, id2 when Stateid.newer_than id2 id1 -> ()
               | _ -> Queue.add msg feedbacks
             with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks 
       end;
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 8cadf1a26..2d2b54678 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -95,7 +95,7 @@ let ide_cmd_checks (loc,ast) =
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
 let add ((s,eid),(sid,verbose)) =
-  let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in
+  let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks s in
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
   (* TODO: the "" parameter is a leftover of the times the protocol
    * used to include stderr/stdout output.
@@ -379,7 +379,7 @@ let init =
          let initial_id, _ =
            if not (is_in_load_paths (physical_path_of_string dir)) then
              Stm.add false ~ontop:(Stm.get_current_state ())
-               0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
+               (Printf.sprintf "Add LoadPath \"%s\". " dir)
            else Stm.get_current_state (), `NewTip in
          if Filename.check_suffix file ".v" then
            Stm.set_compilation_hints file;
diff --git a/ide/interface.mli b/ide/interface.mli
index 9ed606258..62f63aefb 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -111,8 +111,10 @@ type coq_info = {
 (** Calls result *)
 
 type location = (int * int) option (* start and end of the error *)
-type state_id = Feedback.state_id
-type edit_id = Feedback.edit_id
+type state_id = Stateid.t
+
+(* Obsolete *)
+type edit_id  = int
 
 (* The fail case carries the current state_id of the prover, the GUI
    should probably retract to that point *)
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d7950e5fd..bf52b0b52 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -907,9 +907,7 @@ let of_feedback_content = function
         of_string filename ]
   | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ]
 
-let of_edit_or_state_id = function
-  | Edit id -> ["object","edit"], of_edit_id id
-  | State id -> ["object","state"], of_stateid id
+let of_edit_or_state_id id = ["object","state"], of_stateid id
 
 let of_feedback msg =
   let content = of_feedback_content msg.contents in
@@ -921,12 +919,8 @@ let of_feedback msg_fmt =
   msg_format := msg_fmt; of_feedback
 
 let to_feedback xml = match xml with
-  | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
-      id = Edit(to_edit_id id);
-      route = int_of_string route;
-      contents = to_feedback_content content }
   | Element ("feedback", ["object","state";"route",route], [id;content]) -> { 
-      id = State(to_stateid id);
+      id = to_stateid id;
       route = int_of_string route;
       contents = to_feedback_content content }
   | x -> raise (Marshal_error("feedback",x))