From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 toplevel/vernac.ml | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'toplevel/vernac.ml')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index fdd0d4ed..c914bbec 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -28,10 +28,6 @@ let checknav_deep {CAst.loc;v=ast} =
   if is_deep_navigation_vernac ast then
     CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.")
 
-let disable_drop = function
-  | Drop -> CErrors.user_err Pp.(str "Drop is forbidden.")
-  | e -> e
-
 (* Echo from a buffer based on position.
    XXX: Should move to utility file. *)
 let vernac_echo ?loc in_chan = let open Loc in
@@ -80,17 +76,21 @@ module State = struct
     doc : Stm.doc;
     sid : Stateid.t;
     proof : Proof.t option;
+    time : bool;
   }
 
 end
 
-let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) =
+let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
   let open State in
     try
       (* The -time option is only supported from console-based clients
          due to the way it prints. *)
-      if time then print_cmd_header com;
-      let com = if time then CAst.make ?loc @@ VernacTime(time,com) else com in
+      let com = if state.time
+        then begin
+          print_cmd_header com;
+          CAst.make ?loc @@ VernacTime(state.time,com)
+        end else com in
       let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in
 
       (* Main STM interaction *)
@@ -102,7 +102,7 @@ let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) =
       (* Stm.observe nsid; *)
       let ndoc = if check then Stm.finish ~doc else doc in
       let new_proof = Proof_global.give_me_the_proof_opt () in
-      { doc = ndoc; sid = nsid; proof = new_proof }
+      { state with doc = ndoc; sid = nsid; proof = new_proof; }
     with reraise ->
       (* XXX: In non-interactive mode edit_at seems to do very weird
          things, so we better avoid it while we investigate *)
@@ -115,13 +115,13 @@ let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) =
       end in iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
-let load_vernac_core ~time ~echo ~check ~interactive ~state file =
+let load_vernac_core ~echo ~check ~interactive ~state file =
   (* Keep in sync *)
   let in_chan = open_utf8_file_in file in
   let in_echo = if echo then Some (open_utf8_file_in file) else None in
   let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
 
-  let in_pa   = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
+  let in_pa   = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
   let rstate  = ref state in
   (* For beautify, list of parsed sids *)
   let rids    = ref [] in
@@ -154,22 +154,22 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file =
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple ast;
-      let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) ast in
+      let state = Flags.silently (interp_vernac ~check ~interactive ~state:!rstate) ast in
       rids := state.sid :: !rids;
       rstate := state;
     done;
     input_cleanup ();
-    !rstate, !rids, Pcoq.Gram.comment_state in_pa
+    !rstate, !rids, Pcoq.Parsable.comment_state in_pa
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
     input_cleanup ();
     match e with
-    | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa
-    | reraise -> iraise (disable_drop e, info)
+    | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa
+    | reraise -> iraise (e, info)
 
-let process_expr ~time ~state loc_ast =
+let process_expr ~state loc_ast =
   checknav_deep loc_ast;
-  interp_vernac ~time ~interactive:true ~check:true ~state loc_ast
+  interp_vernac ~interactive:true ~check:true ~state loc_ast
 
 (******************************************************************************)
 (* Beautify-specific code                                                     *)
@@ -220,8 +220,8 @@ let beautify_pass ~doc ~comments ~ids ~filename =
 
 (* Main driver for file loading. For now, we only do one beautify
    pass. *)
-let load_vernac ~time ~echo ~check ~interactive ~state filename =
-  let ostate, ids, comments = load_vernac_core ~time ~echo ~check ~interactive ~state filename in
+let load_vernac ~echo ~check ~interactive ~state filename =
+  let ostate, ids, comments = load_vernac_core ~echo ~check ~interactive ~state filename in
   (* Pass for beautify *)
   if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename;
   (* End pass *)
-- 
cgit v1.2.3