Arranged for the desirable behaviour that bullets do not see beyond braces.

i.e.: after a brace is open, one can use the bullets again without clashing with
bullets outside the brace. In particular, one can nest bullets with  arbitrary
depth (by interleaving them with occasional braces).

Also fixed a typo introduced in my previous commit which caused bullets
and braces to behave just like regular focuses.

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

3 files changed, 25 insertions, 24 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 42a522b7c..84b6c133c 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -40,7 +40,7 @@ type unfocusable =
   | Strict
 type _focus_condition = 
     (_focus_kind -> Proofview.proofview -> unfocusable) *
-    (_focus_kind -> focus_info -> focus_info)
+    (_focus_kind -> bool)
 type 'a focus_condition = _focus_condition
 
 let next_kind = ref 0
@@ -49,13 +49,8 @@ let new_focus_kind () =
   incr next_kind;
   r
 
-(* Auxiliary function to define conditions:
-   [check kind1 kind2 inf] returns [inf] if [kind1] and [kind2] match.
-   Otherwise it raises [CheckNext] *)
-exception CheckNext
-(* no handler: confined to this module. *)
-let check kind1 kind2 inf =
-  if kind1=kind2 then inf else raise CheckNext
+(* Auxiliary function to define conditions. *)
+let check kind1 kind2 = kind1=kind2
 
 (* To be authorized to unfocus one must meet the condition prescribed by
     the action which focused.*)
@@ -116,7 +111,7 @@ let no_cond ?loose_end = no_cond_gen CannotUnfocusThisWay ?loose_end
 let done_cond_gen e ~loose_end k0 =
   (cloose loose_end (kind e k0)) &&& pdone e
 let done_cond_gen e ?(loose_end=false) k = done_cond_gen e ~loose_end k , check k
-let done_cond ?loose_end = no_cond_gen CannotUnfocusThisWay ?loose_end
+let done_cond ?loose_end = done_cond_gen CannotUnfocusThisWay ?loose_end
 
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
@@ -342,24 +337,22 @@ let rec unfocus kind pr () =
 
 let unfocus kind pr =
   transaction pr (unfocus kind pr)
-      
-let get_at_point kind ((_,get),inf,_) = get kind inf
+
 exception NoSuchFocus
 (* no handler: should not be allowed to reach toplevel. *)
-exception GetDone of Obj.t
-(* no handler: confined to this module. *)
-let get_in_focus_stack kind stack =
-  try
-    List.iter begin fun pt ->
-      try 
-	raise (GetDone (get_at_point kind pt))
-      with CheckNext -> ()
-    end stack;
-    raise NoSuchFocus
-  with GetDone x -> x
+let rec get_in_focus_stack kind stack =
+  match stack with
+  | ((_,check),inf,_)::stack ->
+      if check kind then inf
+      else get_in_focus_stack kind stack
+  | [] -> raise NoSuchFocus
 let get_at_focus kind pr =
   Obj.magic (get_in_focus_stack kind pr.state.focus_stack)
 
+let is_last_focus kind pr =
+  let ((_,check),_,_) = List.hd pr.state.focus_stack in
+  check kind
+
 let no_focused_goal p =
   Proofview.finished p.state.proofview
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index ae3430535..ef402fe60 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -120,6 +120,9 @@ val unfocus : 'a focus_kind -> proof -> unit
 exception NoSuchFocus
 val get_at_focus : 'a focus_kind -> proof -> 'a
 
+(* [is_last_focus k] check if the most recent focus is of kind [k] *)
+val is_last_focus : 'a focus_kind -> proof -> bool
+
 (* returns [true] if there is no goal under focus. *)
 val no_focused_goal : proof -> bool
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 071858cd3..398e5d949 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -363,9 +363,14 @@ module Bullet = struct
     let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
     let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
 
+    (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
+       experience will tell if this is the right discipline of if we want to be finer and
+       reset them only for a choice of bullets. *)
     let get_bullets pr =
-      try Proof.get_at_focus bullet_kind pr
-      with Proof.NoSuchFocus -> []
+      if Proof.is_last_focus bullet_kind pr then
+	Proof.get_at_focus bullet_kind pr
+      else
+	[]
 
     let has_bullet bul pr =
       let rec has_bullet = function