Merge PR #9263: [STM] explicit handling of parsing states

Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes

2 files changed, 6 insertions, 131 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4cc73f419e..9ee9e7ae2c 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -22,51 +22,6 @@ open Names
 
 module NamedDecl = Context.Named.Declaration
 
-(*** Proof Modes ***)
-
-(* Type of proof modes :
-    - A function [set] to set it *from standard mode*
-    - A function [reset] to reset the *standard mode* from it *)
-type proof_mode_name = string
-type proof_mode = {
-  name : proof_mode_name ;
-  set : unit -> unit ;
-  reset : unit -> unit
-}
-
-let proof_modes = Hashtbl.create 6
-let find_proof_mode n =
-  try Hashtbl.find proof_modes n
-  with Not_found ->
-    CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n))
-
-let register_proof_mode ({name = n} as m) =
-  Hashtbl.add proof_modes n (CEphemeron.create m)
-
-(* initial mode: standard mode *)
-let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
-let _ = register_proof_mode standard
-
-(* Default proof mode, to be set at the beginning of proofs. *)
-let default_proof_mode = ref (find_proof_mode "No")
-
-let get_default_proof_mode_name () =
-  (CEphemeron.default !default_proof_mode standard).name
-
-let proof_mode_opt_name = ["Default";"Proof";"Mode"]
-let () =
-  Goptions.(declare_string_option {
-    optdepr = false;
-    optname = "default proof mode" ;
-    optkey = proof_mode_opt_name ;
-    optread = begin fun () ->
-      (CEphemeron.default !default_proof_mode standard).name
-    end;
-    optwrite = begin fun n ->
-      default_proof_mode := find_proof_mode n
-    end
-  })
-
 (*** Proof Global Environment ***)
 
 (* Extra info on proofs. *)
@@ -95,7 +50,6 @@ type pstate = {
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Constr.named_context option;
   proof : Proof.t;
-  mode : proof_mode CEphemeron.key;
   universe_decl: UState.universe_decl;
   strength : Decl_kinds.goal_kind;
 }
@@ -109,23 +63,8 @@ let apply_terminator f = f
    to be resumed when the current proof is closed or aborted. *)
 let pstates = ref ([] : pstate list)
 
-(* Current proof_mode, for bookkeeping *)
-let current_proof_mode = ref !default_proof_mode
-
-(* combinators for proof modes *)
-let update_proof_mode () =
-  match !pstates with
-  | { mode = m } :: _ ->
-      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
-      current_proof_mode := m;
-      CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ())
-  | _ ->
-      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
-      current_proof_mode := find_proof_mode "No"
-
 (* combinators for the current_proof lists *)
-let push a l = l := a::!l;
-  update_proof_mode ()
+let push a l = l := a::!l
 
 exception NoSuchProof
 let () = CErrors.register_handler begin function
@@ -221,25 +160,8 @@ let discard {CAst.loc;v=id} =
 
 let discard_current () =
   if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
-
 let discard_all () = pstates := []
 
-(* [set_proof_mode] sets the proof mode to be used after it's called. It is
-    typically called by the Proof Mode command. *)
-let set_proof_mode m id =
-  pstates := List.map
-      (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps)
-      !pstates;
-  update_proof_mode ()
-
-let set_proof_mode mn =
-  set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
-
-let activate_proof_mode mode =
-  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
-let disactivate_current_proof_mode () =
-  CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
-
 (** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
@@ -254,9 +176,8 @@ let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator
     proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
     endline_tactic = None;
     section_vars = None;
-    mode = find_proof_mode "No";
-    universe_decl = pl;
-    strength = kind } in
+    strength = kind;
+    universe_decl = pl } in
   push initial_state pstates
 
 let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
@@ -265,9 +186,8 @@ let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals termina
     proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
     endline_tactic = None;
     section_vars = None;
-    mode = find_proof_mode "No";
-    universe_decl = pl;
-    strength = kind } in
+    strength = kind;
+    universe_decl = pl } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
@@ -478,7 +398,7 @@ end
 let freeze ~marshallable =
   if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
   else !pstates
-let unfreeze s = pstates := s; update_proof_mode ()
+let unfreeze s = pstates := s
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
 let copy_terminators ~src ~tgt =
   assert(List.length src = List.length tgt);
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e762f3b7dc..40920f51a3 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,7 +13,6 @@
      environment. *)
 
 type t
-
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
@@ -139,47 +138,3 @@ val freeze : marshallable:bool -> t
 val unfreeze : t -> unit
 val proof_of_state : t -> Proof.t
 val copy_terminators : src:t -> tgt:t -> t
-
-
-(**********************************************************)
-(* Proof Mode API                                         *)
-(* The current Proof Mode API is deprecated and a new one *)
-(* will be (hopefully) defined in 8.8                     *)
-(**********************************************************)
-
-(** Type of proof modes :
-    - A name
-    - A function [set] to set it *from standard mode*
-    - A function [reset] to reset the *standard mode* from it 
-
-*)
-type proof_mode_name = string
-type proof_mode = {
-  name : proof_mode_name ;
-  set : unit -> unit ;
-  reset : unit -> unit
-}
-
-(** Registers a new proof mode which can then be adressed by name
-    in [set_default_proof_mode].
-    One mode is already registered - the standard mode - named "No",
-    It corresponds to Coq default setting are they are set when coqtop starts. *)
-val register_proof_mode : proof_mode -> unit
-(* Can't make this deprecated due to limitations of camlp5 *)
-(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *)
-
-val proof_mode_opt_name : string list
-
-val get_default_proof_mode_name : unit -> proof_mode_name
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-(** [set_proof_mode] sets the proof mode to be used after it's called. It is
-    typically called by the Proof Mode command. *)
-val set_proof_mode : proof_mode_name -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-val activate_proof_mode : proof_mode_name -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-val disactivate_current_proof_mode : unit -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]