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

6 files changed, 21 insertions, 3 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 9adcde1113..5036c01e37 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -60,6 +60,7 @@ GEXTEND Gram
       | IDENT "Focus" -> VernacFocus None
       | IDENT "Focus"; n = natural -> VernacFocus (Some n)
       | IDENT "Unfocus" -> VernacUnfocus
+      | IDENT "Unfocused" -> VernacUnfocused
       | IDENT "BeginSubproof" -> VernacSubproof None
       | IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n)
       | IDENT "EndSubproof" -> VernacEndSubproof
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 75442631c4..0852f846ac 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -439,6 +439,7 @@ let rec pr_vernac = function
   | VernacAbortAll -> str "Abort All"
   | VernacRestart -> str"Restart"
   | VernacUnfocus -> str"Unfocus"
+  | VernacUnfocused -> str"Unfocused"
   | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
   | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
   | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
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]. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2e01aa3ea7..355e693569 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1412,6 +1412,15 @@ let vernac_unfocus () =
   let p = Proof_global.give_me_the_proof () in
   Proof.unfocus command_focus p; print_subgoals ()
 
+(* Checks that a proof is fully unfocused. Raises an error if not. *)
+let vernac_unfocused () =
+  let p = Proof_global.give_me_the_proof () in
+  if Proof.unfocused p then
+    msg (str"The proof is indeed fully unfocused.")
+  else
+    error "The proof is not fully unfocused."
+
+
 (* BeginSubproof / EndSubproof. 
     BeginSubproof (vernac_subproof) focuses on the first goal, or the goal
     given as argument.
@@ -1591,6 +1600,7 @@ let interp c = match c with
   | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
+  | VernacUnfocused -> vernac_unfocused ()
   | VernacBullet b -> vernac_bullet b
   | VernacSubproof n -> vernac_subproof n
   | VernacEndSubproof -> vernac_end_subproof ()
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 7fecdb8a34..e9ecc95ecb 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -350,6 +350,7 @@ type vernac_expr =
   | VernacBacktrack of int*int*int
   | VernacFocus of int option
   | VernacUnfocus
+  | VernacUnfocused
   | VernacBullet of bullet
   | VernacSubproof of int option
   | VernacEndSubproof