Fixed bullets so that they would play well with { }.

We can now have script like
 assert P.
  { destruct n.
     - solve_case1.
     - solve_case2.
  }
  solve_goal

However there is an undesirable interaction with Focus (which we might, anyway, consider deprecated in favour of {}). Indeed, for compatibility with v8.3, Unfocus is called implicitely after each proof command if there is no focused goal. And the new behaviour of bullets is to allow arbitrary unfocusing command "pass trough" them. As a result, a script like
Focus.
  split
  - solves_first_goal
will result in a fully unfocused proof.

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

3 files changed, 123 insertions, 51 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 7e5941025..c9b90ac38 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -34,8 +34,12 @@ open Term
 type _focus_kind = int
 type 'a focus_kind = _focus_kind
 type focus_info = Obj.t
+type unfocusable =
+  | Cannot
+  | Loose
+  | Strict
 type _focus_condition = 
-    (_focus_kind -> Proofview.proofview -> bool) *
+    (_focus_kind -> Proofview.proofview -> unfocusable) *
     (_focus_kind -> focus_info -> focus_info)
 type 'a focus_condition = _focus_condition
 
@@ -59,12 +63,45 @@ let check kind1 kind2 inf =
     of just one, if anyone needs it *)
 (* [no_cond] only checks that the unfocusing command uses the right
     [focus_kind]. *)
-let no_cond k0 k _ = k0 = k
-let no_cond k = no_cond k , check k
+
+module Cond = struct
+  (* first attempt at an algebra of condition *)
+  (* semantics:
+     - [Cannot] means that the condition is not met
+     - [Strict] that the condition is meant
+     - [Loose] that the condition is not quite meant
+       but authorises to unfocus provided a condition
+       of a previous focus on the stack is (strictly)
+       met.
+  *)
+  let bool b =
+    if b then fun _ _ -> Strict
+    else fun _ _ -> Cannot
+  let loose c k p = match c k p with
+    | Cannot -> Loose
+    | c -> c
+  let cloose l c =
+    if l then loose c
+    else c
+  let (&&&) c1 c2 k p=
+    match c1 k p , c2 k p with
+    | Cannot , _ 
+    | _ , Cannot -> Cannot
+    | Strict, Strict -> Strict
+    | _ , _ -> Loose
+  let kind k0 k p = bool (k0=k) k p 
+  let pdone k p = bool (Proofview.finished p) k p
+end
+
+open Cond
+let no_cond ~loose_end k0 =
+  cloose loose_end (kind k0)
+let no_cond ?(loose_end=false) k = no_cond ~loose_end k , check k
 (* [done_cond] checks that the unfocusing command uses the right [focus_kind]
     and that the focused proofview is complete. *)
-let done_cond k0 k p = k0 = k && Proofview.finished p
-let done_cond k = done_cond k , check k
+let done_cond ~loose_end k0 =
+  (cloose loose_end (kind k0)) &&& pdone
+let done_cond ?(loose_end=false) k = done_cond ~loose_end k , check k
 
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
@@ -145,6 +182,7 @@ let return p =
   else
     Proofview.return p.state.proofview
 
+
 (*** The following functions implement the basic internal mechanisms
      of proofs, they are not meant to be exported in the .mli ***)
 
@@ -244,6 +282,44 @@ let undo pr =
 let add_undo effect pr =
   push_undo (Effect effect) pr
 
+
+
+(*** Transactions ***)
+
+let init_transaction pr =
+  pr.transactions <- []::pr.transactions
+
+let commit_stack pr stack =
+  let push s = push_undo s pr in
+  List.iter push (List.rev stack)
+
+(* Invariant: [commit] should be called only when a transaction
+   is open. It closes the current transaction. *)
+let commit pr =
+  match pr.transactions with
+  | stack::trans' ->
+    pr.transactions <- trans';
+    commit_stack pr stack
+  | [] -> assert false
+
+(* Invariant: [rollback] should be called only when a transaction
+   is open. It closes the current transaction. *)
+let rec rollback pr =
+  try
+    undo pr;
+    rollback pr
+  with EmptyUndoStack ->
+    match pr.transactions with
+    | []::trans' -> pr.transactions <- trans'
+    | _ -> assert false
+
+
+let transaction pr t =
+  init_transaction pr;
+  try t (); commit pr
+  with e -> rollback pr; raise e
+
+
 (* Focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
@@ -253,14 +329,31 @@ let focus cond inf i pr =
 
 (* Unfocus command.
    Fails if the proof is not focused. *)
-let unfocus kind pr =
+exception CannotUnfocusThisWay
+let _ = Errors.register_handler begin function
+  | CannotUnfocusThisWay ->
+    Util.error "This proof is focused, but cannot be unfocused this way"
+  | _ -> raise Errors.Unhandled
+end
+
+let rec unfocus kind pr () =
   let starting_point = save_state pr in
   let cond = cond_of_focus pr in
-  if fst cond kind pr.state.proofview then
+  match fst cond kind pr.state.proofview with
+  | Cannot -> raise CannotUnfocusThisWay
+  | Strict -> 
     (_unfocus pr;
      push_undo starting_point pr)
-  else
-    Util.error "This proof is focused, but cannot be unfocused this way"
+  | Loose ->
+    begin try
+	    _unfocus pr;
+	    push_undo starting_point pr;
+	    unfocus kind pr ()
+      with FullyUnfocused -> raise CannotUnfocusThisWay
+    end
+
+let unfocus kind pr =
+  transaction pr (unfocus kind pr)
       
 let get_at_point kind ((_,get),inf,_) = get kind inf
 exception NoSuchFocus
@@ -306,40 +399,6 @@ let run_tactic env tac pr =
     raise e
 
 
-(*** Transactions ***)
-
-let init_transaction pr =
-  pr.transactions <- []::pr.transactions
-
-let commit_stack pr stack =
-  let push s = push_undo s pr in
-  List.iter push (List.rev stack)
-
-(* Invariant: [commit] should be called only when a transaction
-   is open. It closes the current transaction. *)
-let commit pr =
-  match pr.transactions with
-  | stack::trans' ->
-    pr.transactions <- trans';
-    commit_stack pr stack
-  | [] -> assert false
-
-(* Invariant: [rollback] should be called only when a transaction
-   is open. It closes the current transaction. *)
-let rec rollback pr =
-  try
-    undo pr;
-    rollback pr
-  with EmptyUndoStack ->
-    match pr.transactions with
-    | []::trans' -> pr.transactions <- trans'
-    | _ -> assert false
-
-
-let transaction pr t =
-  init_transaction pr;
-  try t (); commit pr
-  with e -> rollback pr; raise e
 
 
 (*** Compatibility layer with <=v8.2 ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index cbde9244a..7de0a9fdf 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -85,11 +85,21 @@ val new_focus_kind : unit -> 'a focus_kind
     from it.*)
 type 'a focus_condition 
 (* [no_cond] only checks that the unfocusing command uses the right
-    [focus_kind]. *)
-val no_cond : 'a focus_kind -> 'a focus_condition
+    [focus_kind].
+   If [loose_end] (default [false]) is [true], then if the [focus_kind]
+   doesn't match, then unfocusing can occur, provided it unfocuses
+   an earlier focus.
+   For instance bullets can be unfocused in the following situation
+   [{- solve_goal. }] because they use a loose-end condition. *)
+val no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
 (* [done_cond] checks that the unfocusing command uses the right [focus_kind]
-    and that the focused proofview is complete. *)
-val done_cond : 'a focus_kind -> 'a focus_condition
+    and that the focused proofview is complete.
+   If [loose_end] (default [false]) is [true], then if the [focus_kind]
+   doesn't match, then unfocusing can occur, provided it unfocuses
+   an earlier focus.
+   For instance bullets can be unfocused in the following situation
+   [{ - solve_goal. }] because they use a loose-end condition.  *)
+val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
 
 (* focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
@@ -97,8 +107,11 @@ val done_cond : 'a focus_kind -> 'a focus_condition
 val focus : 'a focus_condition -> 'a -> int -> proof -> unit
 
 exception FullyUnfocused
+exception CannotUnfocusThisWay
 (* Unfocusing command.
-   Raises [FullyUnfocused] if the proof is not focused. *)
+   Raises [FullyUnfocused] if the proof is not focused.
+   Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
+     is not met. *)
 val unfocus : 'a focus_kind -> proof -> unit
 
 (* [get_at_focus k] gets the information stored at the closest focus point
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 186472be2..a5e19e306 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -300,7 +300,7 @@ let maximal_unfocus k p =
   begin try while Proof.no_focused_goal p do
     Proof.unfocus k p
   done
-  with Proof.FullyUnfocused | Util.UserError _ -> ()
+  with Proof.FullyUnfocused | Proof.CannotUnfocusThisWay -> ()
   end
 
 
@@ -335,7 +335,7 @@ module Bullet = struct
   module Strict = struct
     (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
     let bullet_kind = Proof.new_focus_kind () 
-    let bullet_cond = Proof.done_cond bullet_kind
+    let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
     let (get_bullets,set_bullets) =
       let bullets = Store.field () in
       begin fun pr -> Option.default [] (bullets.get (Proof.get_proof_info pr)) end ,
@@ -364,7 +364,7 @@ module Bullet = struct
 
     let put p bul =
       if has_bullet bul p then
-	begin 
+	Proof.transaction p begin fun () ->
 	  while bul <> pop p do () done;
 	  push bul p
 	end