[vernac] Adapt to removal of imperative proof state.

1 files changed, 80 insertions, 6 deletions

diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index c691dc8559..01c7068f33 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -28,10 +28,10 @@ module Parser = struct
 end
 
 type t = {
-  parsing: Parser.state;
-  system : States.state; (* summary + libstack *)
-  proof : Proof_global.t; (* proof state *)
-  shallow : bool; (* is the state trimmed down (libstack) *)
+  parsing : Parser.state;
+  system  : States.state;          (* summary + libstack *)
+  proof   : Proof_global.t option; (* proof state *)
+  shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
 let s_cache = ref None
@@ -55,14 +55,14 @@ let do_if_not_cached rf f v =
 
 let freeze_interp_state ~marshallable =
   { system = update_cache s_cache (States.freeze ~marshallable);
-    proof  = update_cache s_proof (Proof_global.freeze ~marshallable);
+    proof  = !s_proof;
     shallow = false;
     parsing = Parser.cur_state ();
   }
 
 let unfreeze_interp_state { system; proof; parsing } =
   do_if_not_cached s_cache States.unfreeze system;
-  do_if_not_cached s_proof Proof_global.unfreeze proof;
+  s_proof := proof;
   Pcoq.unfreeze parsing
 
 let make_shallow st =
@@ -71,3 +71,77 @@ let make_shallow st =
     system = States.replace_lib st.system @@ Lib.drop_objects lib;
     shallow = true;
   }
+
+(* Compatibility module *)
+module Proof_global = struct
+
+  let with_fail ~st f = f ()
+
+  let get () = !s_proof
+  let set x = s_proof := x
+
+  let freeze ~marshallable:_ = get ()
+  let unfreeze x = s_proof := Some x
+
+  exception NoCurrentProof
+
+  let () =
+    CErrors.register_handler begin function
+      | NoCurrentProof ->
+        CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
+      | _ -> raise CErrors.Unhandled
+    end
+
+  open Proof_global
+
+  let cc f = match !s_proof with
+    | None -> raise NoCurrentProof
+    | Some x -> f x
+
+  let dd f = match !s_proof with
+    | None -> raise NoCurrentProof
+    | Some x -> s_proof := Some (f x)
+
+  let there_are_pending_proofs () = !s_proof <> None
+  let get_open_goals () = cc get_open_goals
+
+  let set_terminator x = dd (set_terminator x)
+  let give_me_the_proof_opt () = Option.map give_me_the_proof !s_proof
+  let give_me_the_proof () = cc give_me_the_proof
+  let get_current_proof_name () = cc get_current_proof_name
+
+  let simple_with_current_proof f =
+    dd (simple_with_current_proof f)
+
+  let with_current_proof f =
+    let pf, res = cc (with_current_proof f) in
+    s_proof := Some pf; res
+
+  let install_state s = s_proof := Some s
+
+  let return_proof ?allow_partial () =
+    cc (return_proof ?allow_partial)
+
+  let close_future_proof ~opaque ~feedback_id pf =
+    cc (fun st -> close_future_proof ~opaque ~feedback_id st pf)
+
+  let close_proof ~opaque ~keep_body_ucst_separate f =
+    cc (close_proof ~opaque ~keep_body_ucst_separate f)
+
+  let discard_all () = s_proof := None
+  let update_global_env () = dd update_global_env
+
+  let get_current_context () = cc Pfedit.get_current_context
+
+  let get_all_proof_names () =
+    try cc get_all_proof_names
+    with NoCurrentProof -> []
+
+  let copy_terminators ~src ~tgt =
+    match src, tgt with
+    | None, None -> None
+    | Some _ , None -> None
+    | None, Some x -> Some x
+    | Some src, Some tgt -> Some (copy_terminators ~src ~tgt)
+
+end