Pfedit.get_current_context refinement (fix #4523)

Return the most appropriate evar_map for commands that can run on
non-focused proofs (like Check, Show and debug printers) so that
universes and existentials are printed correctly (they are global
to the proof). The API is backwards compatible.

6 files changed, 28 insertions, 23 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6e5b048ccd..4c733dd4f7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -485,9 +485,7 @@ let ppist ist =
 (* Vernac-level debugging commands                                    *)
 
 let in_current_context f c =
-  let (evmap,sign) =
-    try Pfedit.get_current_goal_context ()
-    with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in
+  let (evmap,sign) = Pfedit.get_current_context () in
   f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
 
 (* We expand the result of preprocessing to be independent of camlp4
diff --git a/printing/printer.ml b/printing/printer.ml
index 8469490f05..ac20eeb6f5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -28,10 +28,7 @@ let delayed_emacs_cmd s =
   if !Flags.print_emacs then s () else str ""
 
 let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    let env = Global.env () in
-    (Evd.from_env env, env)
+  Pfedit.get_current_context ()
 
 (**********************************************************************)
 (** Terms                                                             *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2f5c1d1c2b..a515c9e750 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -71,23 +71,34 @@ let get_nth_V82_goal i =
   with Failure _ -> raise NoSuchGoal
     
 let get_goal_context_gen i =
-  try
-let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
-(sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
-  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+  let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
+  (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
 
 let get_goal_context i =
   try get_goal_context_gen i
-  with NoSuchGoal -> Errors.error "No such goal."
+  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+     | NoSuchGoal -> Errors.error "No such goal."
 
 let get_current_goal_context () =
   try get_goal_context_gen 1
-  with NoSuchGoal ->
+  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+     | NoSuchGoal -> 
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
         there is no accessible evar either *)
     let env = Global.env () in
     (Evd.from_env env, env)
 
+let get_current_context () =
+  try get_goal_context_gen 1
+  with Proof_global.NoCurrentProof ->
+    let env = Global.env () in
+    (Evd.from_env env, env)
+     | NoSuchGoal ->
+        (* No more focused goals ? *)
+        let p = get_pftreestate () in
+        let evd = Proof.in_proof p (fun x -> x) in
+        (evd, Global.env ())
+
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
     | (id,([concl],strength)) -> id,strength,concl
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index cd89920151..cfab8bd630 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -93,6 +93,14 @@ val get_goal_context : int -> Evd.evar_map * env
 
 val get_current_goal_context : unit -> Evd.evar_map * env
 
+(** [get_current_context ()] returns the context of the
+  current focused goal. If there is no focused goal but there
+  is a proof in progress, it returns the corresponding evar_map.
+  If there is no pending proof then it returns the current global
+  environment and empty evar_map. *)
+
+val get_current_context : unit -> Evd.evar_map * env
+
 (** [current_proof_statement] *)
 
 val current_proof_statement :
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index fb64a10c6c..5b205e79ef 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -509,13 +509,5 @@ let save_proof ?proof = function
 (* Miscellaneous *)
 
 let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    try (* No more focused goals ? *)
-      let p = Pfedit.get_pftreestate () in
-      let evd = Proof.in_proof p (fun x -> x) in
-      (evd, Global.env ())
-    with Proof_global.NoCurrentProof ->
-      let env = Global.env () in
-      (Evd.from_env env, env)
+  Pfedit.get_current_context ()
            
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 16e54e318e..ca6af9a3fa 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -60,4 +60,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
-