Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"

This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.

It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.

2 files changed, 55 insertions, 18 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 0ddaf604a..e387e6322 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -989,7 +989,7 @@ end = struct (* {{{ *)
     try
       match v with
       | VernacResetInitial ->
-          VtBack (Stateid.initial, true), VtNow
+          VtStm (VtBack Stateid.initial, true), VtNow
       | VernacResetName (_,name) ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
@@ -997,20 +997,20 @@ end = struct (* {{{ *)
               fold_until (fun b (id,_,label,_,_) ->
                 if b then `Stop id else `Cont (List.mem name label))
               false id in
-            VtBack (oid, true), VtNow
+            VtStm (VtBack oid, true), VtNow
           with Not_found ->
-            VtBack (id, true), VtNow)
+            VtStm (VtBack id, true), VtNow)
       | VernacBack n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          VtBack (oid, true), VtNow
+          VtStm (VtBack oid, true), VtNow
       | VernacUndo n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_,tactic,undo) ->
             let value = (if tactic then 1 else 0) - undo in
             if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
-          VtBack (oid, true), VtLater
+          VtStm (VtBack oid, true), VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1027,16 +1027,16 @@ end = struct (* {{{ *)
             0 id in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
-          VtBack (oid, true), VtLater
+          VtStm (VtBack oid, true), VtLater
       | VernacAbortAll ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun () (id,vcs,_,_,_) ->
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
-          VtBack (oid, true), VtLater
+          VtStm (VtBack oid, true), VtLater
       | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
-          VtBack (Stateid.of_int id, not !Flags.print_emacs), VtNow
+          VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
@@ -2428,8 +2428,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       prerr_endline (fun () ->
         "  classified as: " ^ string_of_vernac_classification c);
       match c with
+      (* PG stuff *)    
+      | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
+      | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
+      (* Joining various parts of the document *)
+      | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
+      | VtStm (VtFinish, b),       VtNow -> finish (); `Ok
+      | VtStm (VtWait, b),     VtNow -> finish (); wait (); `Ok
+      | VtStm (VtPrintDag, b), VtNow ->
+          VCS.print ~now:true (); `Ok
+      | VtStm (VtObserve id, b),   VtNow -> observe id; `Ok
+      | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
+                |VtPrintDag |VtWait),_), VtLater ->
+          anomaly(str"classifier: join actions cannot be classified as VtLater")
+      
       (* Back *)
-      | VtBack(oid, true), w ->
+      | VtStm (VtBack oid, true), w ->
           let id = VCS.new_node ~id:newtip () in
           let { mine; others } = Backtrack.branches_of oid in
           let valid = VCS.get_branch_pos head in
@@ -2448,12 +2462,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           VCS.checkout_shallowest_proof_branch ();
           VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
-      | VtBack (id, false), VtNow ->
+      | VtStm (VtBack id, false), VtNow ->
           prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id; `Ok
-      | VtBack (id, false), VtLater ->
+      | VtStm (VtBack id, false), VtLater ->
           anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
 
       (* Query *)
@@ -2590,6 +2604,15 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       | VtUnknown, VtLater ->
           anomaly(str"classifier: VtUnknown must imply VtNow")
     end in
+    (* Proof General *)
+    begin match expr with 
+      | VernacStm (PGLast _) ->
+        if not (VCS.Branch.equal head VCS.Branch.master) then
+          vernac_interp Stateid.dummy
+            { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
+              expr = VernacShow (ShowGoal OpenSubgoals) }
+      | _ -> ()
+    end;
     prerr_endline (fun () -> "processed }}}");
     VCS.print ();
     rc
@@ -2651,8 +2674,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
     let clas = classify_vernac ast in
     let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
     match clas with
-    | VtBack (w,_), _ ->
-       ignore(process_transaction ~tty:false aast (VtBack (w,false), VtNow))
+    | VtStm (w,_), _ ->
+       ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
     | _ ->
        ignore(process_transaction
          ~tty:false aast (VtQuery (false,report_with), VtNow)))
@@ -2799,7 +2822,7 @@ let interp verb (loc,e) =
     let print_goals =
       verb && match clas with
        | VtQuery _, _ -> false
-       | (VtProofStep _ | VtBack (_, _) | VtStartProof _), _ -> true
+       | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
        | _ -> not !Flags.coqtop_ui in
     try finish ~print_goals ()
     with e ->
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f9bf9653f..dc5be08a3 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -33,7 +33,10 @@ let string_of_vernac_type = function
   | VtQuery (b,(id,route)) ->
       "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
       " route " ^ string_of_int route
-  | VtBack(_, b) -> "Stm Back " ^ string_of_in_script b
+  | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
+      "Stm " ^ string_of_in_script b
+  | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
+  | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
 
 let string_of_vernac_when = function
   | VtLater -> "Later"
@@ -52,7 +55,7 @@ let declare_vernac_classifier
 let elide_part_of_script_and_now (a, _) =
   match a with
   | VtQuery (_,id) -> VtQuery (false,id), VtNow
-  | VtBack (x, _) -> VtBack (x, false), VtNow
+  | VtStm (x, _) -> VtStm (x, false), VtNow
   | x -> x, VtNow
 
 let make_polymorphic (a, b as x) =
@@ -66,12 +69,23 @@ let set_undo_classifier f = undo_classifier := f
 
 let rec classify_vernac e =
   let static_classifier e = match e with
+    (* PG compatibility *)
+    | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
+    | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
+      when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
     | VernacSetOption (["Universe"; "Polymorphism"],_)
     | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
-
+    (* Stm *)
+    | VernacStm Finish -> VtStm (VtFinish, true), VtNow
+    | VernacStm Wait -> VtStm (VtWait, true), VtNow
+    | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
+    | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
+    | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
+    | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
+    | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
     (* Nested vernac exprs *)
     | VernacProgram e -> classify_vernac e
     | VernacLocal (_,e) -> classify_vernac e
@@ -84,7 +98,7 @@ let rec classify_vernac e =
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
-          | VtBack _ | VtProofMode _ ), _ as x -> x
+          | VtStm _ | VtProofMode _ ), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtNow