Added a command "Unfocused" which returns an error when the proof is

not fully unfocused (in the style of the Guarded command).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15104 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 8 insertions, 3 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 84b6c133c4..27a65da4c7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -259,13 +259,13 @@ let save pr =
   push_undo (save_state pr) pr
 
 (* This function restores a state, presumably from the top of the undo stack. *)
-let restore_state save pr = 
+let restore_state save pr =
   match save with
   | State save -> pr.state <- save
   | Effect undo -> undo ()
 
 (* Interpretes the Undo command. *)
-let undo pr = 
+let undo pr =
   (* On a single line, since the effects commute *)
   restore_state (pop_undo pr) pr
 
@@ -362,8 +362,10 @@ let no_focused_goal p =
 let end_of_stack_kind = new_focus_kind ()
 let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind
 
+let unfocused = is_last_focus end_of_stack_kind
+
 let start goals =
-  let pr = 
+  let pr =
     { state = { proofview = Proofview.init goals ;
 	        focus_stack = [] ;
 	        intel = Store.empty} ;
diff --git a/proofs/proof.mli b/proofs/proof.mli
index ef402fe606..715b3341b6 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -114,6 +114,9 @@ exception CannotUnfocusThisWay
      is not met. *)
 val unfocus : 'a focus_kind -> proof -> unit
 
+(* [unfocused p] returns [true] when [p] is fully unfocused. *)
+val unfocused : proof -> bool
+
 (* [get_at_focus k] gets the information stored at the closest focus point
     of kind [k].
     Raises [NoSuchFocus] if there is no focus point of kind [k]. *)