From ae27de7dbce680e91353982bf23d568adca0d017 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 28 Feb 2018 20:24:18 +0100
Subject: [toplevel] Update state when `Drop` exception is thrown [#6872]

`Drop` is implemented using exceptions-as-control flow, so the
toplevel state gets corrupted as `do_vernac` will never return when
`Drop` occurs in the input.

The right fix would be to remove `Drop` from the vernacular and make
it a toplevel-only command, but meanwhile we can just patch the state
in the exception handler.

We also need to keep the global state in `Coqloop` as the main
`coqtop` entry point won't be called by `go ()`.

Fixes #6872.
---
 toplevel/coqloop.ml  | 11 ++++++++++-
 toplevel/coqloop.mli |  3 +++
 toplevel/coqtop.ml   |  4 +---
 toplevel/coqtop.mli  |  3 ---
 4 files changed, 14 insertions(+), 7 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index ae0b94476..7ad8e2c05 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -339,6 +339,8 @@ let loop_flush_all () =
   Format.pp_print_flush !Topfmt.std_ft ();
   Format.pp_print_flush !Topfmt.err_ft ()
 
+let drop_last_doc = ref None
+
 let rec loop ~time ~state =
   let open Vernac.State in
   Sys.catch_break true;
@@ -353,7 +355,14 @@ let rec loop ~time ~state =
        not possible due exceptions. *)
     in vernac_loop ~state
   with
-    | CErrors.Drop -> state
+    | 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
     | any ->
       top_stderr (str "Anomaly: main loop exited with exception: " ++
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 1c1309051..928f3609a 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -35,3 +35,6 @@ 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
+
+(** 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 26ede1834..deb2c2038 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -34,7 +34,6 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
    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 opts ~state =
@@ -44,9 +43,8 @@ let console_toploop_run opts ~state =
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
-  let state = Coqloop.loop ~time:opts.time ~state in
+  let _ = Coqloop.loop ~time:opts.time ~state in
   (* Initialise and launch the Ocaml toplevel *)
-  drop_last_doc := Some state;
   Coqinit.init_ocaml_path();
   Mltop.ocaml_toploop();
   (* We let the feeder in place for users of Drop *)
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index dedb298e2..510e10dd1 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -15,9 +15,6 @@ 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 : 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 -> state:Vernac.State.t -> unit) ref
-- 
cgit v1.2.3