Merge PR#441: Port Toplevel to the Stm API

4 files changed, 31 insertions, 72 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 3d6a2583f..eb97755fa 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -414,11 +414,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)); *)
@@ -433,8 +429,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
@@ -503,8 +498,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 0dfa03cca..4b95e983d 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -8,6 +8,7 @@
 (************************************************************************)
 
 open Vernacexpr
+open Vernacprop
 open CErrors
 open Util
 open Pp
@@ -60,25 +61,6 @@ let is_known_option cmd = match cmd with
   | VernacUnsetOption o -> coqide_known_option o
   | _ -> false
 
-let is_debug cmd = match cmd with
-  | VernacSetOption (["Ltac";"Debug"], _) -> true
-  | _ -> false
-
-let is_query cmd = match cmd with
-  | VernacChdir None
-  | VernacMemOption _
-  | VernacPrintOption _
-  | VernacCheckMayEval _
-  | VernacGlobalCheck _
-  | VernacPrint _
-  | VernacSearch _
-  | VernacLocate _ -> true
-  | _ -> false
-
-let is_undo cmd = match cmd with
-  | VernacUndo _ | VernacUndoTo _ -> true
-  | _ -> false
-
 (** Check whether a command is forbidden in the IDE *)
 
 let ide_cmd_checks (loc,ast) =
@@ -86,16 +68,19 @@ let ide_cmd_checks (loc,ast) =
   if is_debug ast then
     user_error "Debug mode not available in the IDE";
   if is_known_option ast then
-    Feedback.msg_warning (strbrk "Set this option from the IDE menu instead");
-  if Vernac.is_navigation_vernac ast || is_undo ast then
-    Feedback.msg_warning (strbrk "Use IDE navigation instead");
+    Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead");
+  if is_navigation_vernac ast || is_undo ast then
+    Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead");
   if is_query ast then
-    Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts")
+    Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts")
 
 (** 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 pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  let loc_ast = Stm.parse_sentence sid pa in
+  ide_cmd_checks loc_ast;
+  let newid, rc = Stm.add ~ontop:sid verbose loc_ast 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.
@@ -122,12 +107,14 @@ let edit_at id =
  * as not to break the core protocol for this minor change, but it should
  * be removed in the next version of the protocol.
  *)
-let query (s,id) = Stm.query ~at:id s; ""
+let query (s,id) =
+  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  Stm.query ~at:id pa; ""
 
 let annotate phrase =
   let (loc, ast) =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
-    Vernac.parse_sentence (pa,None)
+    Stm.parse_sentence (Stm.get_current_state ()) pa
   in
   (* XXX: Width should be a parameter of annotate... *)
   Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
@@ -370,43 +357,28 @@ let init =
   fun file ->
    if !initialized then anomaly (str "Already initialized")
    else begin
+     let init_sid = Stm.get_current_state () in
      initialized := true;
      match file with
-     | None -> Stm.get_current_state ()
+     | None -> init_sid
      | Some file ->
          let dir = Filename.dirname file in
          let open Loadpath in let open CUnix in
          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)
-           else Stm.get_current_state (), `NewTip in
+           if not (is_in_load_paths (physical_path_of_string dir)) then begin
+             let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in
+             let loc_ast = Stm.parse_sentence init_sid pa in
+             Stm.add false ~ontop:init_sid loc_ast
+           end else init_sid, `NewTip in
          if Filename.check_suffix file ".v" then
            Stm.set_compilation_hints file;
          Stm.finish ();
          initial_id
    end
 
-(* Retrocompatibility stuff *)
+(* Retrocompatibility stuff, disabled since 8.7 *)
 let interp ((_raw, verbose), s) =
-  let vernac_parse s =
-    let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-    Flags.with_option Flags.we_are_parsing (fun () ->
-      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
-      | None -> raise (Invalid_argument "vernac_parse")
-      | Some ast -> ast)
-    () in
-  Stm.interp verbose (vernac_parse s);
-  (* TODO: the "" parameter is a leftover of the times the protocol
-   * used to include stderr/stdout output.
-   *
-   * Currently, we force all the output meant for the to go via the
-   * feedback mechanism, and we don't manipulate stderr/stdout, which
-   * are left to the client's discrection. The parameter is still there
-   * as not to break the core protocol for this minor change, but it should
-   * be removed in the next version of the protocol.
-   *)
-  Stm.get_current_state (), CSig.Inl ""
+  Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add."
 
 (** When receiving the Quit call, we don't directly do an [exit 0],
     but rather set this reference, in order to send a final answer
@@ -494,9 +466,6 @@ let loop () =
   let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
   ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));
-  (* We'll handle goal fetching and display in our own way *)
-  Vernacentries.enable_goal_printing := false;
-  Vernacentries.qed_display_script := false;
   while not !quit do
     try
       let xml_query = Xml_parser.parse xml_ic in
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))