Merge PR#717: [proof] Deprecate "proof mode" API

4 files changed, 55 insertions, 46 deletions

diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 52bbd9ac5..22cc8cf59 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -10,26 +10,6 @@
      toplevel. In particular it defines the global proof
      environment. *)
 
-(** 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
-val get_default_proof_mode_name : unit -> proof_mode_name
-
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
@@ -40,10 +20,6 @@ val discard : Names.Id.t Loc.located -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
-(** [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
-
 exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
 (** @raise NoCurrentProof when outside proof mode. *)
@@ -147,16 +123,6 @@ val get_universe_binders : unit -> universe_binders option
 
 (**********************************************************)
 (*                                                        *)
-(*                            Proof modes                 *)
-(*                                                        *)
-(**********************************************************)
-
-
-val activate_proof_mode : proof_mode_name -> unit
-val disactivate_current_proof_mode : unit -> unit
-
-(**********************************************************)
-(*                                                        *)
 (*                                 Bullets                *)
 (*                                                        *)
 (**********************************************************)
@@ -211,3 +177,46 @@ val freeze : marshallable:[`Yes | `No | `Shallow] -> state
 val unfreeze : state -> unit
 val proof_of_state : state -> Proof.proof
 val copy_terminators : src:state -> tgt:state -> state
+
+
+(**********************************************************)
+(* 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 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 "]
+
diff --git a/stm/stm.ml b/stm/stm.ml
index e95bec099..a79bf5426 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -80,7 +80,7 @@ type aast = {
 }
 let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
 
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
 
 (* Commands piercing opaque *)
 let may_pierce_opaque = function
@@ -502,7 +502,7 @@ end = struct (* {{{ *)
     if List.mem edit_branch (Vcs_.branches !vcs) then begin
       checkout edit_branch;
       match get_branch edit_branch with
-      | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode
+      | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
       | _ -> assert false
     end else
       let pl = proof_nesting () in
@@ -511,10 +511,10 @@ end = struct (* {{{ *)
           | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
         checkout branch;
         stm_prerr_endline (fun () -> "mode:" ^ mode);
-        Proof_global.activate_proof_mode mode
+        Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
       with Failure _ ->
         checkout Branch.master;
-        Proof_global.disactivate_current_proof_mode ()
+        Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"]
 
   (* copies the transaction on every open branch *)
   let propagate_sideff ~action =
@@ -2368,8 +2368,8 @@ let finish () =
      hides true bugs cf bug #5363. Also, what happens with observe? *)
   (* Some commands may by side effect change the proof mode *)
   match VCS.get_branch head with
-  | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
-  | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
+  | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
+  | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
   | _ -> ()
 
 let wait () =
@@ -2551,7 +2551,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
             VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
             VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
           end;
-          Proof_global.activate_proof_mode mode;
+          Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtProofMode _, VtLater ->
           anomaly(str"VtProofMode must be executed VtNow.")
@@ -2632,7 +2632,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
               VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[]));
               let proof_mode = default_proof_mode () in
               VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
-              Proof_global.activate_proof_mode proof_mode;
+              Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
             end else begin
               VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
               (* We hope it can be replayed, but we can't really know *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index d597f64ad..471e05e45 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -10,7 +10,7 @@ open Vernacexpr
 open CErrors
 open Pp
 
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
 
 let string_of_in_script b = if b then " (inside script)" else ""
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1332a7052..69492759b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1868,8 +1868,8 @@ exception End_of_input
  *)
 let vernac_load interp fname =
   let interp x =
-    let proof_mode = Proof_global.get_default_proof_mode_name () in
-    Proof_global.activate_proof_mode proof_mode;
+    let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
+    Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
     interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
@@ -2052,7 +2052,7 @@ let interp ?proof ?loc locality poly c =
   | VernacProof (Some tac, Some l) -> 
       Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes";
       vernac_set_end_tac tac; vernac_set_used_variables l
-  | VernacProofMode mn -> Proof_global.set_proof_mode mn
+  | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
   (* Extensions *)
   | VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args)