Merge branch 'trunk' into pr379

2 files changed, 12 insertions, 43 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index b8a406430..2b6ee5511 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2235,10 +2235,13 @@ let known_state ?(redefine_qed=false) ~cache id =
 	    if eff then update_global_env ()
           ), (if eff then `Yes else cache), true
       | `Cmd { cast = x; ceff = eff } -> (fun () ->
-            resilient_command reach view.next;
-            stm_vernac_interp id x;
-	    if eff then update_global_env ()
-          ), (if eff then `Yes else cache), true
+          (match !Flags.async_proofs_mode with
+           | Flags.APon | Flags.APonLazy ->
+             resilient_command reach view.next
+           | Flags.APoff -> reach view.next);
+          stm_vernac_interp id x;
+          if eff then update_global_env ()
+        ), (if eff then `Yes else cache), true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             resilient_command reach view.next;
             stm_vernac_interp id x;
@@ -2528,20 +2531,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
@@ -2704,15 +2699,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