[toplevel] Export the last document seen after `Drop`.

After `Drop`, `Coqtop.drop_last_doc` will contain the current document
used by `Coqloop`. This is useful for people wanting to restart Coq
after a `Drop`.

5 files changed, 12 insertions, 8 deletions

diff --git a/dev/base_include b/dev/base_include
index 79ecd73e0..f2912e112 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -233,8 +233,7 @@ let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
   (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
-open Coqloop
-let go = loop
+let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc)
 
 let _ =
  print_string
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index c16e2751b..910c81381 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -350,7 +350,7 @@ let rec loop doc =
        not possible due exceptions. *)
     in vernac_loop doc (Stm.get_current_state ~doc)
   with
-    | CErrors.Drop -> ()
+    | CErrors.Drop -> doc
     | CErrors.Quit -> exit 0
     | any ->
       Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 46dabf995..46934f326 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -36,4 +36,4 @@ val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
 
 (** Main entry point of Coq: read and execute vernac commands. *)
 
-val loop : Stm.doc -> unit
+val loop : Stm.doc -> Stm.doc
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 19fcd9993..f3d5d9b85 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -79,6 +79,7 @@ let toploop_init = ref begin fun x ->
    will not be generally be initialized, thus stateid, etc... may be
    bogus. For now we just print to the console too *)
 let coqtop_init_feed = Coqloop.coqloop_feed
+let drop_last_doc = ref None
 
 (* Default toplevel loop *)
 let console_toploop_run doc =
@@ -88,8 +89,9 @@ let console_toploop_run doc =
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
-  Coqloop.loop doc;
+  let doc = Coqloop.loop doc in
   (* Initialise and launch the Ocaml toplevel *)
+  drop_last_doc := Some doc;
   Coqinit.init_ocaml_path();
   Mltop.ocaml_toploop();
   (* We let the feeder in place for users of Drop *)
@@ -183,9 +185,9 @@ let load_vernacular doc sid =
     (fun (doc,sid) (f_in, verbosely) ->
       let s = Loadpath.locate_file f_in in
       if !Flags.beautify then
-	Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in
+        Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in
       else
-	Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
+        Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
     (doc, sid) (List.rev !load_vernacular_list)
 
 let load_init_vernaculars doc sid =
@@ -726,7 +728,7 @@ let parse_args arglist =
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
     |"-native-compiler" ->
       if Coq_config.no_native_compiler then
-	warning "Native compilation was disabled at configure time."
+        warning "Native compilation was disabled at configure time."
       else Flags.native_compiler := true
     |"-output-context" -> output_context := true
     |"-profile-ltac" -> Flags.profile_ltac := true
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 1c7c3f944..5b9494eaa 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -15,6 +15,9 @@ val init_toplevel : string list -> (Stm.doc * Stateid.t) option
 
 val start : unit -> unit
 
+(* Last document seen after `Drop` *)
+val drop_last_doc : Stm.doc option ref
+
 (* For other toploops *)
 val toploop_init : (string list -> string list) ref
 val toploop_run : (Stm.doc -> unit) ref