[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.

11 files changed, 58 insertions, 75 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 45b5a1007a..15150dce99 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 8cadf1a263..2d2b54678f 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 9ed6062588..62f63aefb9 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 d7950e5fd5..bf52b0b52b 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))
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 6dfa64357c..88a4fa529a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -194,7 +194,7 @@ let rec unzip ctx j =
 let feedback_completion_typecheck =
   let open Feedback in
   Option.iter (fun state_id ->
-      feedback ~id:(State state_id) Feedback.Complete)
+      feedback ~id:state_id Feedback.Complete)
 
 let infer_declaration ~trust env kn dcl =
   match dcl with
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 7d9d6bf7f0..df6fe3a629 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -15,9 +15,6 @@ type level =
   | Warning
   | Error
 
-type edit_id = int
-type state_id = Stateid.t
-type edit_or_state_id = Edit of edit_id | State of state_id
 type route_id = int
 
 type feedback_content =
@@ -38,9 +35,9 @@ type feedback_content =
   | Message of level * Loc.t option * Pp.std_ppcmds
 
 type feedback = {
-  id : edit_or_state_id;
+  id       : Stateid.t;
+  route    : route_id;
   contents : feedback_content;
-  route : route_id;
 }
 
 let default_route = 0
@@ -56,7 +53,8 @@ let add_feeder =
 
 let del_feeder fid = Hashtbl.remove feeders fid
 
-let feedback_id    = ref (Edit 0)
+let default_route = 0
+let feedback_id    = ref Stateid.dummy
 let feedback_route = ref default_route
 
 let set_id_for_feedback ?(route=default_route) i =
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 4bbdfcb5b6..bdd236ac78 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -16,11 +16,8 @@ type level =
   | Warning
   | Error
 
-(** Coq "semantic" infos obtained during parsing/execution *)
-type edit_id = int
-type state_id = Stateid.t
-type edit_or_state_id = Edit of edit_id | State of state_id
 
+(** Coq "semantic" infos obtained during execution *)
 type route_id = int
 
 val default_route : route_id
@@ -46,17 +43,16 @@ type feedback_content =
   | Message of level * Loc.t option * Pp.std_ppcmds
 
 type feedback = {
-  id       : edit_or_state_id;  (* The document part concerned *)
-  contents : feedback_content;  (* The payload *)
+  id       : Stateid.t;         (* The document part concerned *)
   route    : route_id;          (* Extra routing info *)
+  contents : feedback_content;  (* The payload *)
 }
 
 (** {6 Feedback sent, even asynchronously, to the user interface} *)
-(* Morally the parser gets a string and an edit_id, and gives back an AST.
- * Feedbacks during the parsing phase are attached to this edit_id.
- * The interpreter assignes an exec_id to the ast, and feedbacks happening
- * during interpretation are attached to the exec_id.
- * Only one among state_id and edit_id can be provided. *)
+
+(* The interpreter assignes an state_id to the ast, and feedbacks happening
+ * during interpretation are attached to it.
+ *)
 
 (** [add_feeder f] adds a feeder listiner [f], returning its id *)
 val add_feeder : (feedback -> unit) -> int
@@ -67,11 +63,10 @@ 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:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+val feedback : ?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 -> edit_or_state_id -> unit
+val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit
 
 (** {6 output functions}
 
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 58123f63ef..bcb28f77ce 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -374,7 +374,7 @@ let data = ref SM.empty
 
 let _ =
   Feedback.(add_feeder (function
-    | { id = State s; contents = Custom (_, "ltacprof_results", xml) } ->
+    | { id = s; contents = Custom (_, "ltacprof_results", xml) } ->
         let results = to_ltacprof_results xml in
         let other_results = (* Multi success can cause this *)
           try SM.find s !data
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 1254919880..3459156a43 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -105,7 +105,7 @@ module Make(T : Task) = struct
 
   let report_status ?(id = !Flags.async_proofs_worker_id) s =
     let open Feedback in
-    feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
+    feedback ~id:Stateid.initial (WorkerStatus(id, s))
 
   module Worker = Spawn.Sync(struct end)
 
diff --git a/stm/stm.ml b/stm/stm.ml
index ba5e8a11fb..f8d959f97a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -24,14 +24,14 @@ open Vernac_classifier
 open Feedback
 
 let execution_error state_id loc msg =
-    feedback ~id:(State state_id)
+    feedback ~id:state_id
       (Message (Error, Some loc, msg))
 
 module Hooks = struct
 
 let state_computed, state_computed_hook = Hook.make
  ~default:(fun state_id ~in_cache ->
-    feedback ~id:(State state_id) Processed) ()
+    feedback ~id:state_id Processed) ()
 
 let state_ready, state_ready_hook = Hook.make
  ~default:(fun state_id -> ()) ()
@@ -43,10 +43,6 @@ let forward_feedback, forward_feedback_hook =
         try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
         with e -> Mutex.unlock m; raise e) ()
 
-let parse_error, parse_error_hook = Hook.make
- ~default:(fun id loc msg ->
-        feedback ~id (Message(Error, Some loc, msg))) ()
-
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
 
@@ -109,24 +105,30 @@ let indentation_of_string s =
       | _ -> n, precise, len in
   aux 0 0 false
 
-let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
-  let feedback_id = 
-    if Option.is_empty newtip then Edit eid
-    else State (Option.get newtip) in
+(* We must parse on top of a state id, it should be something like:
+
+   - get parsing information for that state.
+   - feed the parsable / parser with the right parsing information.
+   - call the parser
+
+   Now, the invariant in ensured by the callers, but this is a bit
+   problematic.
+*)
+let stm_parse ?(indlen_prev=fun() -> 0) s =
   let indentation, precise, strlen = indentation_of_string s in
   let indentation =
     if precise then indentation else indlen_prev () + indentation in
-  set_id_for_feedback ?route feedback_id;
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   Flags.with_option Flags.we_are_parsing (fun () ->
     try
       match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
-      | None -> raise (Invalid_argument "vernac_parse")
+      | None            -> raise (Invalid_argument "stm_parse")
       | Some (loc, ast) -> indentation, strlen, loc, ast
     with e when CErrors.noncritical e ->
       let (e, info) = CErrors.push e in
-      let loc = Option.default Loc.ghost (Loc.get_loc info) in
-      Hooks.(call parse_error feedback_id loc (iprint (e, info)));
+      (* This is the old error recovery strategy.             *)
+      (* let loc = Loc.get_loc info in                        *)
+      (* feedback (?newtip || eid) (Message(Error, loc, msg)) *)
       iraise (e, info))
   ()
 
@@ -845,7 +847,7 @@ end = struct (* {{{ *)
   let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
         f id
   =
-    feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
+    feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
     let str_id = Stateid.to_string id in
     if is_cached id && not redefine then
       anomaly (str"defining state "++str str_id++str" twice");
@@ -977,7 +979,7 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
   (* The Stm will gain the capability to interpret commmads affecting
      the whole document state, such as backtrack, etc... so we start
      to design the stm command interpreter now *)
-  set_id_for_feedback ?route (State id);
+  set_id_for_feedback ?route id;
   Aux_file.record_in_aux_set_at loc;
   (* We need to check if a command should be filtered from
    * vernac_entries, as it cannot handle it. This should go away in
@@ -1391,7 +1393,7 @@ end = struct (* {{{ *)
       Aux_file.record_in_aux_at loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       let p = Proof_global.return_proof ~allow_partial:drop_pt () in
-      if drop_pt then feedback ~id:(State id) Complete;
+      if drop_pt then feedback ~id Complete;
       p)
 
   let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1935,11 +1937,11 @@ end = struct (* {{{ *)
     Reach.known_state ~cache:`No r_where;
     try
       stm_vernac_interp r_for { r_what with verbose = true };
-      feedback ~id:(State r_for) Processed
+      feedback ~id:r_for Processed
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
       let msg = iprint e     in
-      feedback ~id:(State r_for) (Message (Error, None, msg))
+      feedback ~id:r_for (Message (Error, None, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
   let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -2141,7 +2143,7 @@ let known_state ?(redefine_qed=false) ~cache id =
            | Valid { proof } ->
                Proof_global.unfreeze proof;
                Proof_global.with_current_proof (fun _ p ->
-                 feedback ~id:(State id) Feedback.AddedAxiom;
+                 feedback ~id:id Feedback.AddedAxiom;
                  fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
                Option.iter (fun expr -> stm_vernac_interp id {
                   verbose = true; loc = Loc.ghost; expr; indentation = 0;
@@ -2289,7 +2291,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     stm_vernac_interp id ~proof x;
-                    feedback ~id:(State id) Incomplete
+                    feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
                 Proof_global.discard_all ()
@@ -2715,13 +2717,13 @@ let ind_len_of id =
        indentation + strlen
   | _ -> 0
 
-let add ~ontop ?newtip ?(check=ignore) verb eid s =
+let add ~ontop ?newtip ?(check=ignore) verb s =
   let cur_tip = VCS.cur_tip () in
   if not (Stateid.equal ontop cur_tip) then
     (* For now, arbitrary edits should be announced with edit_at *)
     anomaly(str"Not yet implemented, the GUI should not try this");
   let indentation, strlen, loc, ast =
-    vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in
+    stm_parse ~indlen_prev:(fun () -> ind_len_of ontop) s in
   CWarnings.set_current_loc loc;
   check(loc,ast);
   let clas = classify_vernac ast in
@@ -2742,8 +2744,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
   Future.purify (fun s ->
     if Stateid.equal at Stateid.dummy then finish ()
     else Reach.known_state ~cache:`Yes at;
-    let newtip, route = report_with in
-    let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in
+    let indentation, strlen, loc, ast = stm_parse s in
     CWarnings.set_current_loc loc;
     let clas = classify_vernac ast in
     let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
@@ -2932,8 +2933,8 @@ let get_all_proof_names () =
 (* Export hooks *)
 let state_computed_hook = Hooks.state_computed_hook
 let state_ready_hook = Hooks.state_ready_hook
-let parse_error_hook = Hooks.parse_error_hook
 let forward_feedback_hook = Hooks.forward_feedback_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
 let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index a89062c298..d3e5dde39c 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -13,8 +13,8 @@ open Loc
 
 (** state-transaction-machine interface *)
 
-(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]
-   having edit id [eid].  [check] is called on the AST.
+(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop].
+   [check] is called on the AST.
    The [ontop] parameter is just for asserting the GUI is on sync, but
    will eventually call edit_at on the fly if needed.
    The sentence [s] is parsed in the state [ontop].
@@ -23,7 +23,7 @@ open Loc
 val add :
   ontop:Stateid.t -> ?newtip:Stateid.t ->
   ?check:(vernac_expr located -> unit) ->
-  bool -> edit_id -> string ->
+  bool -> string ->
     Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
 (* parses and executes a command at a given state, throws away its side effects
@@ -182,9 +182,8 @@ val register_proof_block_delimiter :
  * the name of the Task(s) above) *)
 
 val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
-val parse_error_hook :
-  (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
+
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t