Merge PR#511: [stm] Remove some obsolete vernacs/classification.

6 files changed, 14 insertions, 71 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 8827bc132..f782dd639 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -283,14 +283,9 @@ type bullet =
     | Plus of int
 
 (** {6 Types concerning Stm} *)
-type 'a stm_vernac =
+type stm_vernac =
   | JoinDocument
-  | Finish
   | Wait
-  | PrintDag
-  | Observe of Stateid.t
-  | Command of 'a (* An out of flow command not to be recorded by Stm *)
-  | PGLast of 'a (* To ease the life of PG *)
 
 (** {6 Types concerning the module layer} *)
 
@@ -450,8 +445,9 @@ type vernac_expr =
   | VernacRegister of lident * register_kind
   | VernacComments of comment list
 
-  (* Stm backdoor *)
-  | VernacStm of vernac_expr stm_vernac
+  (* Stm backdoor: used in fake_id, will be removed when fake_ide
+     becomes aware of feedback about completed jobs. *)
+  | VernacStm of stm_vernac
 
   (* Proof management *)
   | VernacGoal of constr_expr
@@ -509,16 +505,11 @@ and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *)
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Id.t list
 and vernac_sideff_type = Id.t list
-and vernac_is_alias = bool
 and vernac_part_of_script = bool
 and vernac_control =
-  | VtFinish
   | VtWait
   | VtJoinDocument
-  | VtPrintDag
-  | VtObserve of Stateid.t
   | VtBack of Stateid.t
-  | VtPG
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 18807113c..23f1dccaf 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -66,13 +66,7 @@ GEXTEND Gram
 
       (* Stm backdoor *)
       | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument
-      | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish
       | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait
-      | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag
-      | IDENT "Stm"; IDENT "Observe"; id = INT; "." ->
-          VernacStm (Observe (Stateid.of_int (int_of_string id)))
-      | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
-      | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
 
       | v = vernac_poly -> v ]
     ]
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 78ef4d4ba..cfc2e48d1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -534,18 +534,8 @@ open Decl_kinds
       (* Stm *)
       | VernacStm JoinDocument ->
         return (keyword "Stm JoinDocument")
-      | VernacStm PrintDag ->
-        return (keyword "Stm PrintDag")
-      | VernacStm Finish ->
-        return (keyword "Stm Finish")
       | VernacStm Wait ->
         return (keyword "Stm Wait")
-      | VernacStm (Observe id) ->
-        return (keyword "Stm Observe " ++ str(Stateid.to_string id))
-      | VernacStm (Command v) ->
-        return (keyword "Stm Command " ++ pr_vernac_body v)
-      | VernacStm (PGLast v) ->
-        return (keyword "Stm PGLast " ++ pr_vernac_body v)
 
       (* Proof management *)
       | VernacAbortAll ->
diff --git a/stm/stm.ml b/stm/stm.ml
index b9dbb7891..b592aab0d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2525,20 +2525,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       stm_prerr_endline (fun () ->
         "  classified as: " ^ string_of_vernac_classification c);
       match c with
-      (* PG stuff *)    
-      | VtStm(VtPG,false), VtNow -> stm_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 ->
+      | VtStm (VtWait, b),         VtNow -> finish (); wait (); `Ok
+      | VtStm ((VtJoinDocument|VtWait),_), VtLater ->
           anomaly(str"classifier: join actions cannot be classified as VtLater")
-      
+
       (* Back *)
       | VtStm (VtBack oid, true), w ->
           let id = VCS.new_node ~id:newtip () in
@@ -2701,15 +2693,6 @@ 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
-          stm_vernac_interp Stateid.dummy
-            { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
-              expr = VernacShow (ShowGoal OpenSubgoals) }
-      | _ -> ()
-    end;
     stm_prerr_endline (fun () -> "processed }}}");
     VCS.print ();
     rc
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index dc5be08a3..5908c09d0 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -33,9 +33,7 @@ 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
-  | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
-      "Stm " ^ string_of_in_script b
-  | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
+  | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b
   | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
 
 let string_of_vernac_when = function
@@ -52,12 +50,6 @@ let declare_vernac_classifier
 =
   classifiers := !classifiers @ [s,f]
 
-let elide_part_of_script_and_now (a, _) =
-  match a with
-  | VtQuery (_,id) -> VtQuery (false,id), VtNow
-  | VtStm (x, _) -> VtStm (x, false), VtNow
-  | x -> x, VtNow
-
 let make_polymorphic (a, b as x) =
   match a with
   | VtStartProof (x, _, ids) ->
@@ -69,23 +61,14 @@ 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 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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f17908400..ca03ba3f3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2209,6 +2209,11 @@ let with_fail b f =
 let interp ?(verbosely=true) ?proof (loc,c) =
   let orig_program_mode = Flags.is_program_mode () in
   let rec aux ?locality ?polymorphism isprogcmd = function
+
+    (* This assert case will be removed when fake_ide can understand
+       completion feedback *)
+    | VernacStm _ -> assert false (* Done by Stm *)
+
     | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
     | VernacProgram _ -> CErrors.error "Program mode specified twice"
     | VernacLocal (b, c) when Option.is_empty locality -> 
@@ -2217,9 +2222,6 @@ let interp ?(verbosely=true) ?proof (loc,c) =
       aux ?locality ~polymorphism:b isprogcmd c
     | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
     | VernacLocal _ -> CErrors.error "Locality specified twice"
-    | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c
-    | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c
-    | VernacStm _ -> assert false (* Done by Stm *)
     | VernacFail v ->
         with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
     | VernacTimeout (n,v) ->