[vernac] Move `Quit` and `Drop` to the toplevel layer.

This is a first step towards moving REPL-specific commands out of the
core layers. In particular, we remove `Quit` and `Drop` from the core
vernacular to specific toplevel-level parsing rules.

9 files changed, 121 insertions, 95 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 96a0bd5ec..3e7a83085 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -23,12 +23,12 @@ let set_debug () =
 
 let rcdefaultname = "coqrc"
 
-let load_rcfile ~rcfile ~time ~state =
+let load_rcfile ~rcfile ~state =
     try
       match rcfile with
       | Some rcfile ->
         if CUnix.file_readable_p rcfile then
-          Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile
+          Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
       | None ->
 	try
@@ -39,7 +39,7 @@ let load_rcfile ~rcfile ~time ~state =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc
+          Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc
         with Not_found -> state
 	(*
 	Flags.if_verbose
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 71b5523cd..c891e736b 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -12,12 +12,12 @@
 
 val set_debug : unit -> unit
 
-val load_rcfile : rcfile:(string option) -> time:bool -> state:Vernac.State.t -> Vernac.State.t
+val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t
 
 val init_ocaml_path : unit -> unit
 
 (* LoadPath for toploop toplevels *)
-val toplevel_init_load_path : unit ->  Mltop.coq_path list
+val toplevel_init_load_path : unit -> Mltop.coq_path list
 
 (* LoadPath for Coq user libraries *)
 val libs_init_load_path : load_init:bool -> Mltop.coq_path list
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index a103cfe7f..64d839f18 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -261,8 +261,8 @@ let rec discard_to_dot () =
     | e when CErrors.noncritical e -> ()
 
 let read_sentence ~state input =
-  let open Vernac.State in
-  try Stm.parse_sentence ~doc:state.doc state.sid input
+  (* XXX: careful with ignoring the state Eugene!*)
+  try G_toplevel.parse_toplevel input
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
@@ -293,40 +293,6 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   | Message (lvl,loc,msg) ->
     TopErr.print_error_for_buffer ?loc lvl msg top_buffer
 
-(** [do_vernac] reads and executes a toplevel phrase, and print error
-    messages when an exception is raised, except for the following:
-    - Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
-           Otherwise, exit.
-    - End_of_input: Ctrl-D was typed in, we will quit.
-
-    In particular, this is normally the only place where a Sys.Break
-    is caught and handled (i.e. not re-raised).
-*)
-
-let do_vernac ~time ~state =
-  let open Vernac.State in
-  top_stderr (fnl());
-  if !print_emacs then top_stderr (str (top_buffer.prompt state.doc));
-  resynch_buffer top_buffer;
-  try
-    let input = (top_buffer.tokens, None) in
-    Vernac.process_expr ~time ~state (read_sentence ~state (fst input))
-  with
-    | Stm.End_of_input | CErrors.Quit ->
-        top_stderr (fnl ()); raise CErrors.Quit
-    | CErrors.Drop ->  (* Last chance *)
-        if Mltop.is_ocaml_top() then raise CErrors.Drop
-        else (Feedback.msg_warning (str "There is no ML toplevel."); state)
-    (* Exception printing should be done by the feedback listener,
-       however this is not yet ready so we rely on the exception for
-       now. *)
-    | any ->
-      let (e, info) = CErrors.push any in
-      let loc = Loc.get_loc info in
-      let msg = CErrors.iprint (e, info) in
-      TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
-      state
-
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
     Normally, the only exceptions that can come out of [do_vernac] and
@@ -359,37 +325,55 @@ let cproof p1 p2 =
 
 let drop_last_doc = ref None
 
-let rec loop ~time ~state =
+(* Careful to keep this loop tail-rec *)
+let rec vernac_loop ~state =
+  let open CAst in
   let open Vernac.State in
-  Sys.catch_break true;
+  let open G_toplevel in
+  loop_flush_all ();
+  top_stderr (fnl());
+  if !print_emacs then top_stderr (str (top_buffer.prompt state.doc));
+  resynch_buffer top_buffer;
+  (* execute one command *)
   try
-    reset_input_buffer state.doc stdin top_buffer;
-    (* Be careful to keep this loop tail-recursive *)
-    let rec vernac_loop ~state =
-      let nstate = do_vernac ~time ~state in
+    let input = top_buffer.tokens in
+    match read_sentence ~state input with
+    | {v=VernacQuit} ->
+      exit 0
+    | {v=VernacDrop} ->
+      if Mltop.is_ocaml_top()
+      then (drop_last_doc := Some state; state)
+      else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state)
+    | {v=VernacControl c; loc} ->
+      let nstate = Vernac.process_expr ~state (make ?loc c) in
       let proof_changed = not (Option.equal cproof nstate.proof state.proof) in
       let print_goals = not !Flags.quiet &&
                         proof_changed && Proof_global.there_are_pending_proofs () in
       if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
-      loop_flush_all ();
       vernac_loop ~state:nstate
-    (* We recover the current stateid, threading from the caller is
-       not possible due exceptions. *)
-    in vernac_loop ~state
   with
-    | CErrors.Drop ->
-      (* Due to using exceptions as a form of control, state here goes
-         out of sync as [do_vernac] will never return. We must thus do
-         this hack until we make `Drop` a toplevel-only command. See
-         bug #6872. *)
-      let state = { state with sid = Stm.get_current_state ~doc:state.doc } in
-      drop_last_doc := Some state;
-      state
-    | CErrors.Quit -> exit 0
+  | Stm.End_of_input ->
+    top_stderr (fnl ()); exit 0
+  (* Exception printing should be done by the feedback listener,
+     however this is not yet ready so we rely on the exception for
+     now. *)
+  | any ->
+    let (e, info) = CErrors.push any in
+    let loc = Loc.get_loc info in
+    let msg = CErrors.iprint (e, info) in
+    TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+    vernac_loop ~state
+
+let rec loop ~state =
+  let open Vernac.State in
+  Sys.catch_break true;
+  try
+    reset_input_buffer state.doc stdin top_buffer;
+    vernac_loop ~state
+  with
     | any ->
-      top_stderr (str "Anomaly: main loop exited with exception: " ++
-                  str (Printexc.to_string any) ++
-                  fnl() ++
-                  str"Please report" ++
-                  strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
-      loop ~time ~state
+      top_stderr
+        (hov 0 (str "Anomaly: main loop exited with exception:" ++ spc () ++
+                str (Printexc.to_string any)) ++ spc () ++
+         hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str "."));
+      loop ~state
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index bbb9b1383..39a9de4f8 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,11 +32,8 @@ val set_prompt : (unit -> string) -> unit
 (** Toplevel feedback printer. *)
 val coqloop_feed : Feedback.feedback -> unit
 
-(** Parse and execute one vernac command. *)
-val do_vernac : time:bool -> state:Vernac.State.t -> Vernac.State.t
-
 (** Main entry point of Coq: read and execute vernac commands. *)
-val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t
+val loop : state:Vernac.State.t -> Vernac.State.t
 
 (** Last document seen after `Drop` *)
 val drop_last_doc : Vernac.State.t option ref
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cd831c05c..a08cfa9f4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -45,7 +45,7 @@ let console_toploop_run opts ~state =
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
-  let _ = Coqloop.loop ~time:opts.time ~state in
+  let _ = Coqloop.loop ~state in
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
   Mltop.ocaml_toploop();
@@ -95,7 +95,7 @@ let load_vernacular opts ~state =
     (fun state (f_in, echo) ->
       let s = Loadpath.locate_file f_in in
       (* Should make the beautify logic clearer *)
-      let load_vernac f = Vernac.load_vernac ~time:opts.time ~echo ~interactive:false ~check:true ~state f in
+      let load_vernac f = Vernac.load_vernac ~echo ~interactive:false ~check:true ~state f in
       if !Flags.beautify
       then Flags.with_option Flags.beautify_file load_vernac f_in
       else load_vernac s
@@ -103,7 +103,7 @@ let load_vernacular opts ~state =
 
 let load_init_vernaculars opts ~state =
   let state = if opts.load_rcfile then
-      Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state
+      Coqinit.load_rcfile ~rcfile:opts.rcfile ~state
     else begin
       Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
       state
@@ -223,7 +223,7 @@ let compile opts ~echo ~f_in ~f_out =
             iload_path; require_libs; stm_options;
           }) in
 
-      let state = { doc; sid; proof = None } in
+      let state = { doc; sid; proof = None; time = opts.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
       Aux_file.(start_aux_file
@@ -232,7 +232,7 @@ let compile opts ~echo ~f_in ~f_out =
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       let wall_clock1 = Unix.gettimeofday () in
-      let state = Vernac.load_vernac ~time:opts.time ~echo ~check:true ~interactive:false ~state long_f_dot_v in
+      let state = Vernac.load_vernac ~echo ~check:true ~interactive:false ~state long_f_dot_v in
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
@@ -270,10 +270,10 @@ let compile opts ~echo ~f_in ~f_out =
             iload_path; require_libs; stm_options;
           }) in
 
-      let state = { doc; sid; proof = None } in
+      let state = { doc; sid; proof = None; time = opts.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
-      let state = Vernac.load_vernac ~time:opts.time ~echo ~check:false ~interactive:false ~state long_f_dot_v in
+      let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
       let doc = Stm.finish ~doc:state.doc in
       check_pending_proofs ();
       let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
@@ -476,7 +476,7 @@ let init_toplevel arglist =
                    { doc_type = Interactive opts.toplevel_name;
                      iload_path; require_libs; stm_options;
                    }) in
-          let state = { doc; sid; proof = None } in
+          let state = { doc; sid; proof = None; time = opts.time } in
           Some (load_init_vernaculars opts ~state), opts
         with any -> flush_all(); fatal_error_exn any
       (* Non interactive: we perform a sequence of compilation steps *)
diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.ml4
new file mode 100644
index 000000000..7526f3071
--- /dev/null
+++ b/toplevel/g_toplevel.ml4
@@ -0,0 +1,43 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pcoq
+open Vernacexpr
+
+(* Vernaculars specific to the toplevel *)
+type vernac_toplevel =
+  | VernacDrop
+  | VernacQuit
+  | VernacControl of vernac_control
+
+module Toplevel_ : sig
+  val vernac_toplevel : vernac_toplevel CAst.t Gram.entry
+end = struct
+  let gec_vernac s = Gram.entry_create ("toplevel:" ^ s)
+  let vernac_toplevel = gec_vernac "vernac_toplevel"
+end
+
+open Toplevel_
+
+GEXTEND Gram
+  GLOBAL: vernac_toplevel;
+  vernac_toplevel: FIRST
+    [ [ IDENT "Drop"; "." -> CAst.make VernacDrop
+      | IDENT "Quit"; "." -> CAst.make VernacQuit
+      | cmd = main_entry ->
+              match cmd with
+              | None -> raise Stm.End_of_input
+              | Some (loc,c) -> CAst.make ~loc (VernacControl c)
+      ]
+    ]
+  ;
+END
+
+let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 9fb2e33d7..78b96e5e2 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,5 +1,6 @@
 Vernac
 Usage
+G_toplevel
 Coqloop
 Coqinit
 Coqargs
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index fdd0d4ed3..c1bbb20d5 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,7 +115,7 @@ 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
@@ -154,7 +154,7 @@ 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;
@@ -165,11 +165,11 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file =
     input_cleanup ();
     match e with
     | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa
-    | reraise -> iraise (disable_drop e, info)
+    | 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 *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 51758642e..126954023 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -15,6 +15,7 @@ module State : sig
     doc : Stm.doc;
     sid : Stateid.t;
     proof : Proof.t option;
+    time : bool;
   }
 
 end
@@ -23,10 +24,10 @@ end
     expected to handle and print errors in form of exceptions, however
     care is taken so the state machine is left in a consistent
     state. *)
-val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t
+val process_expr : state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t
 
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
     echo the commands if [echo] is set. Callers are expected to handle
     and print errors in form of exceptions. *)
-val load_vernac : time:bool -> echo:bool -> check:bool -> interactive:bool ->
+val load_vernac : echo:bool -> check:bool -> interactive:bool ->
   state:State.t -> string -> State.t