[toplevel] Make toplevel state into a record.

We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.

8 files changed, 107 insertions, 79 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8574092b8..d8aaf3db8 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -21,12 +21,12 @@ let set_debug () =
 
 let rcdefaultname = "coqrc"
 
-let load_rcfile ~rcfile ~time doc sid =
+let load_rcfile ~rcfile ~time ~state =
     try
       match rcfile with
       | Some rcfile ->
         if CUnix.file_readable_p rcfile then
-          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid rcfile
+          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
       | None ->
 	try
@@ -37,8 +37,8 @@ let load_rcfile ~rcfile ~time doc sid =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
-	with Not_found -> doc, sid
+          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state inferedrc
+        with Not_found -> state
 	(*
 	Flags.if_verbose
 	  mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 0ceba5b38..14f39170c 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -10,7 +10,7 @@
 
 val set_debug : unit -> unit
 
-val load_rcfile : rcfile:(string option) -> time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val load_rcfile : rcfile:(string option) -> time:bool -> state:Vernac.State.t -> Vernac.State.t
 
 val init_ocaml_path : unit -> unit
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index aade101a4..ae0b94476 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -258,8 +258,9 @@ let rec discard_to_dot () =
     | Stm.End_of_input -> raise Stm.End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_sentence ~doc sid input =
-  try Stm.parse_sentence ~doc sid input
+let read_sentence ~state input =
+  let open Vernac.State in
+  try Stm.parse_sentence ~doc:state.doc state.sid input
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
@@ -300,19 +301,20 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
     is caught and handled (i.e. not re-raised).
 *)
 
-let do_vernac ~time doc sid =
+let do_vernac ~time ~state =
+  let open Vernac.State in
   top_stderr (fnl());
-  if !print_emacs then top_stderr (str (top_buffer.prompt doc));
+  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 doc sid (read_sentence ~doc sid (fst input))
+    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."); doc, sid)
+        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. *)
@@ -321,7 +323,7 @@ let do_vernac ~time doc sid =
       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;
-      doc, sid
+      state
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -337,20 +339,21 @@ let loop_flush_all () =
   Format.pp_print_flush !Topfmt.std_ft ();
   Format.pp_print_flush !Topfmt.err_ft ()
 
-let rec loop ~time doc =
+let rec loop ~time ~state =
+  let open Vernac.State in
   Sys.catch_break true;
   try
-    reset_input_buffer doc stdin top_buffer;
+    reset_input_buffer state.doc stdin top_buffer;
     (* Be careful to keep this loop tail-recursive *)
-    let rec vernac_loop doc sid =
-      let ndoc, nsid = do_vernac ~time doc sid in
+    let rec vernac_loop ~state =
+      let nstate = do_vernac ~time ~state in
       loop_flush_all ();
-      vernac_loop ndoc nsid
+      vernac_loop ~state:nstate
     (* We recover the current stateid, threading from the caller is
        not possible due exceptions. *)
-    in vernac_loop doc (Stm.get_current_state ~doc)
+    in vernac_loop ~state
   with
-    | CErrors.Drop -> doc
+    | CErrors.Drop -> state
     | CErrors.Quit -> exit 0
     | any ->
       top_stderr (str "Anomaly: main loop exited with exception: " ++
@@ -358,4 +361,4 @@ let rec loop ~time doc =
                   fnl() ++
                   str"Please report" ++
                   strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
-      loop ~time doc
+      loop ~time ~state
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 09240ec82..1c1309051 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -31,9 +31,7 @@ val set_prompt : (unit -> string) -> unit
 val coqloop_feed : Feedback.feedback -> unit
 
 (** Parse and execute one vernac command. *)
-
-val do_vernac : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+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 -> Stm.doc -> Stm.doc
+val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9058f0846..26ede1834 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -37,16 +37,16 @@ let coqtop_init_feed = Coqloop.coqloop_feed
 let drop_last_doc = ref None
 
 (* Default toplevel loop *)
-let console_toploop_run opts doc =
+let console_toploop_run opts ~state =
   (* We initialize the console only if we run the toploop_run *)
   let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
   if Dumpglob.dump () then begin
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
-  let doc = Coqloop.loop ~time:opts.time doc in
+  let state = Coqloop.loop ~time:opts.time ~state in
   (* Initialise and launch the Ocaml toplevel *)
-  drop_last_doc := Some doc;
+  drop_last_doc := Some state;
   Coqinit.init_ocaml_path();
   Mltop.ocaml_toploop();
   (* We let the feeder in place for users of Drop *)
@@ -90,24 +90,26 @@ let outputstate opts =
 (******************************************************************************)
 (* Interactive Load File Simulation                                           *)
 (******************************************************************************)
-let load_vernacular opts doc sid =
+let load_vernacular opts ~state =
   List.fold_left
-    (fun (doc,sid) (f_in, verbosely) ->
+    (fun state (f_in, verbosely) ->
       let s = Loadpath.locate_file f_in in
-      if !Flags.beautify then
-        Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid) f_in
-      else
-        Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid s)
-    (doc, sid) (List.rev opts.load_vernacular_list)
-
-let load_init_vernaculars opts doc sid =
-  let doc, sid = if opts.load_rcfile then
-      Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time doc sid
+      (* Should make the beautify logic clearer *)
+      let load_vernac f = Vernac.load_vernac ~time:opts.time ~verbosely ~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
+    ) state (List.rev opts.load_vernacular_list)
+
+let load_init_vernaculars opts ~state =
+  let state = if opts.load_rcfile then
+      Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state
     else begin
       Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
-      doc,sid
+      state
     end in
-  load_vernacular opts doc sid
+
+  load_vernacular opts ~state
 
 (******************************************************************************)
 (* Startup LoadPath and Modules                                               *)
@@ -193,6 +195,7 @@ let ensure_exists f =
 
 (* Compile a vernac file *)
 let compile opts ~verbosely ~f_in ~f_out =
+  let open Vernac.State in
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
     if not (CList.is_empty pfs) then
@@ -220,16 +223,17 @@ let compile opts ~verbosely ~f_in ~f_out =
             iload_path; require_libs; stm_options;
           }) in
 
-      let doc, sid = load_init_vernaculars opts doc sid in
-      let ldir = Stm.get_ldir ~doc in
+      let state = { doc; sid; proof = None } in
+      let state = load_init_vernaculars opts ~state in
+      let ldir = Stm.get_ldir ~doc:state.doc in
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_vo)
         ~v_file:long_f_dot_v);
       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 doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
-      let _doc = Stm.join ~doc in
+      let state = Vernac.load_vernac ~time:opts.time ~verbosely ~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 ();
       Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
@@ -266,11 +270,11 @@ let compile opts ~verbosely ~f_in ~f_out =
             iload_path; require_libs; stm_options;
           }) in
 
-      let doc, sid = load_init_vernaculars opts doc sid in
-
-      let ldir = Stm.get_ldir ~doc in
-      let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
-      let doc = Stm.finish ~doc in
+      let state = { doc; sid; proof = None } 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 ~verbosely ~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
       Stm.reset_task_queue ()
@@ -465,12 +469,15 @@ let init_toplevel arglist =
         let iload_path = build_load_path opts in
         let require_libs = require_libs opts in
         let stm_options = opts.stm_flags in
-        try let doc, sid =
-              Stm.(new_doc
-                     { doc_type = Interactive opts.toplevel_name;
-                       iload_path; require_libs; stm_options;
-                     }) in
-          Some (load_init_vernaculars opts doc sid), opts
+        try
+          let open Vernac.State in
+          let doc, sid =
+            Stm.(new_doc
+                   { doc_type = Interactive opts.toplevel_name;
+                     iload_path; require_libs; stm_options;
+                   }) in
+          let state = { doc; sid; proof = None } 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 *)
       end else begin
@@ -496,8 +503,8 @@ let init_toplevel arglist =
 let start () =
   match init_toplevel (List.tl (Array.to_list Sys.argv)) with
   (* Batch mode *)
-  | Some (doc, sid), opts when not opts.batch_mode ->
-    !toploop_run opts doc;
+  | Some state, opts when not opts.batch_mode ->
+    !toploop_run opts ~state;
     exit 1
   | _ , opts ->
     flush_all();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 4d625a03d..dedb298e2 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -11,14 +11,13 @@
    state, load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch [Coqloop.loop]. *)
 
-val init_toplevel : string list -> (Stm.doc * Stateid.t) option * Coqargs.coq_cmdopts
+val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts
 
 val start : unit -> unit
 
 (* Last document seen after `Drop` *)
-val drop_last_doc : Stm.doc option ref
+val drop_last_doc : Vernac.State.t option ref
 
 (* For other toploops *)
 val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref
-val toploop_run : (Coqargs.coq_cmdopts -> Stm.doc -> unit) ref
-
+val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6b45a94bc..1f681d9cf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -110,14 +110,25 @@ let pr_open_cur_subgoals () =
 (*     Stm.End_of_input -> true *)
 (*   | _ -> false *)
 
-let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
+module State = struct
+
+  type t = {
+    doc : Stm.doc;
+    sid : Stateid.t;
+    proof : Proof.t option;
+  }
+
+end
+
+let rec interp_vernac ~time ~check ~interactive ~state (loc,com) =
+  let open State in
   let interp v =
     match under_control v with
     | VernacLoad (verbosely, fname) ->
         let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
-        load_vernac ~time ~verbosely ~check ~interactive doc sid f
+        load_vernac ~time ~verbosely ~check ~interactive ~state f
     | _ ->
       (* XXX: We need to run this before add as the classification is
          highly dynamic and depends on the structure of the
@@ -134,7 +145,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
       in
       CWarnings.set_flags wflags;
 
-      let doc, nsid, ntip = Stm.add ~doc ~ontop:sid (not !Flags.quiet) (loc,v) in
+      let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,v) in
 
       (* Main STM interaction *)
       if ntip <> `NewTip then
@@ -152,7 +163,8 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
                         is_proof_step && Proof_global.there_are_pending_proofs () in
 
       if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
-      ndoc, nsid
+      let new_proof = Proof_global.give_me_the_proof_opt () in
+      { doc = ndoc; sid = nsid; proof = new_proof }
   in
     try
       (* The -time option is only supported from console-based
@@ -163,7 +175,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
     with reraise ->
       (* XXX: In non-interactive mode edit_at seems to do very weird
          things, so we better avoid it while we investigate *)
-      if interactive then ignore(Stm.edit_at ~doc sid);
+      if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid);
       let (reraise, info) = CErrors.push reraise in
       let info = begin
         match Loc.get_loc info with
@@ -172,7 +184,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
       end in iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
+and load_vernac ~time ~verbosely ~check ~interactive ~state file =
   let ft_beautify, close_beautify =
     if !Flags.beautify_file then
       let chan_beautify = open_out (file^beautify_suffix) in
@@ -183,14 +195,14 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
   let in_chan = open_utf8_file_in file in
   let in_echo = if verbosely then Some (open_utf8_file_in file) else None in
   let in_pa   = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
-  let rsid = ref sid in
-  let rdoc = ref doc in
+  let rstate  = ref state in
+  let open State in
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc, ast =
-          Stm.parse_sentence ~doc:!rdoc !rsid in_pa
+          Stm.parse_sentence ~doc:!rstate.doc !rstate.sid in_pa
         (* If an error in parsing occurs, we propagate the exception
            so the caller of load_vernac will take care of it. However,
            in the future it could be possible that we want to handle
@@ -214,11 +226,10 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
-      let ndoc, nsid = Flags.silently (interp_vernac ~time ~check ~interactive !rdoc !rsid) (loc, ast) in
-      rsid := nsid;
-      rdoc := ndoc
+      let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) (loc, ast) in
+      rstate := state;
     done;
-    !rdoc, !rsid
+    !rstate
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
     close_in in_chan;
@@ -229,7 +240,7 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
           if !Flags.beautify then
             pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None;
           if !Flags.beautify_file then close_beautify ();
-          !rdoc, !rsid
+          !rstate
       | reraise ->
          if !Flags.beautify_file then close_beautify ();
 	 iraise (disable_drop e, info)
@@ -241,6 +252,6 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-let process_expr ~time doc sid loc_ast =
+let process_expr ~time ~state loc_ast =
   checknav_deep loc_ast;
-  interp_vernac ~time ~interactive:true ~check:true doc sid loc_ast
+  interp_vernac ~time ~interactive:true ~check:true ~state loc_ast
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index b77b024fa..e909ada1e 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -7,14 +7,24 @@
 (************************************************************************)
 
 (** Parsing of vernacular. *)
+module State : sig
+
+  type t = {
+    doc : Stm.doc;
+    sid : Stateid.t;
+    proof : Proof.t option;
+  }
+
+end
 
 (** [process_expr sid cmd] Executes vernac command [cmd]. Callers are
     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 -> Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t
+val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.located -> 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 -> verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
+val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool ->
+  state:State.t -> string -> State.t