New option [Set Bullet Behavior] allows to select the behaviour of bullets.

- Two predefined behaviours : "None" where bullet have no effect and
  "Strict Subproofs" (default) which acts as previously.
- More behaviours can be registered by plugins via
  [Proof_global.Bullet.register_behavior].

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

7 files changed, 152 insertions, 59 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 6dae6ee233..3593239023 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -103,9 +103,9 @@ GEXTEND Gram
     | b = bullet; tac = subgoal_command -> tac None (Some b)] ]
   ;
   bullet:
-  [ [ "-" -> Dash
-    | "*" -> Star
-    | "+" -> Plus ] ]
+  [ [ "-" -> Proof_global.Bullet.Dash
+    | "*" -> Proof_global.Bullet.Star
+    | "+" -> Proof_global.Bullet.Plus ] ]
   ;
   subgoal_command: 
     [ [ c = check_command; "." -> fun g _ -> c g
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4bf6e59f13..ebd8175d74 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -745,7 +745,12 @@ let rec pr_vernac = function
   (* Solving *)
   | VernacSolve (i,b,tac,deftac) ->
       (if i = 1 then mt() else int i ++ str ": ") ++
-      (match b with None -> mt () | Some Dash -> str"-" | Some Star -> str"*" | Some Plus -> str"+") ++
+      begin match b with
+      | None -> mt ()
+      | Some Proof_global.Bullet.Dash -> str"-"
+      | Some Proof_global.Bullet.Star -> str"*"
+      | Some Proof_global.Bullet.Plus -> str"+"
+      end ++
       pr_raw_tactic tac
       ++ (try if deftac then str ".." else mt ()
       with UserError _|Loc.Exc_located _ -> mt())
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index bcd9d6e0d3..f930486673 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -8,9 +8,9 @@
 
 (***********************************************************************)
 (*                                                                     *)
-(*      This module defines the global proof environment               *)
-(*      In particular it keeps tracks of whether or not there is          *)
-(*      a proof which is currently being edited.                       *)
+(*      This module defines proof facilities relevant to the           *)
+(*      toplevel. In particular it defines the global proof            *)
+(*      environment.                                                   *)
 (*                                                                     *)
 (***********************************************************************)
 
@@ -296,6 +296,105 @@ let maximal_unfocus k p =
     ()
   end
 
+
+(**********************************************************)
+(*                                                        *)
+(*                                 Bullets                *)
+(*                                                        *)
+(**********************************************************)
+
+module Bullet = struct
+
+  open Store.Field
+
+
+  type t = 
+    | Dash
+    | Star
+    | Plus
+
+  type behavior = {
+    name : string;
+    put : Proof.proof -> t -> unit
+  }
+
+  let behaviors = Hashtbl.create 4
+  let register_behavior b = Hashtbl.add behaviors b.name b
+
+  (*** initial modes ***)
+  let none = {
+    name = "None";
+    put = fun _ _ -> ()
+  }
+  let _ = register_behavior none
+
+  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 (get_bullets,set_bullets) =
+      let bullets = Store.field () in
+      begin fun pr -> Option.default [] (bullets.get (Proof.get_proof_info pr)) end ,
+      begin fun bs pr -> Proof.set_proof_info (bullets.set bs (Proof.get_proof_info pr)) pr end
+
+    let has_bullet bul pr =
+      let rec has_bullet = function
+	| b'::_ when bul=b' -> true
+	| _::l -> has_bullet l
+	| [] -> false
+      in
+      has_bullet (get_bullets pr)
+
+    (* precondition: the stack is not empty *)
+    let pop pr =
+      match get_bullets pr with
+      | b::stk -> 
+	Proof.unfocus bullet_kind pr ;
+	set_bullets stk pr ;
+	b
+      | [] -> Util.anomaly "Tried to pop bullet from an empty stack"
+
+    let push b pr =
+      Proof.focus bullet_cond () 1 pr ;
+      set_bullets (b::get_bullets pr) pr
+
+    let put p bul =
+      if has_bullet bul p then
+	begin 
+	  while bul <> pop p do () done;
+	  push bul p
+	end
+      else 
+	push bul p
+
+    let strict = {
+      name = "Strict Subproofs";
+      put = put
+    }
+    let _ = register_behavior strict
+  end
+
+  (* Current bullet behavior, controled by the option *)
+  let current_behavior = ref Strict.strict
+    
+  let _ =
+    Goptions.declare_string_option {Goptions.
+      optsync = true;
+      optname = "bullet behavior";
+      optkey = ["Bullet";"Behavior"];
+      optread = begin fun () ->
+	(!current_behavior).name
+      end;
+      optwrite = begin fun n ->
+	current_behavior := Hashtbl.find behaviors n
+      end
+    }
+
+  let put p b =
+    (!current_behavior).put p b
+end
+
+
 module V82 = struct
   let get_current_initial_conclusions () =
     let p = give_me_the_proof () in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e32ec85ad9..f9dbe3438a 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** This module defines the global proof environment
-
- Especially it keeps tracks of whether or not there is a proof which is currently being edited. *)
+(** This module defines proof facilities relevant to the
+     toplevel. In particular it defines the global proof
+     environment. *)
 
 (** Type of proof modes :
     - A name
@@ -95,6 +95,42 @@ val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
     focused goal or that the last focus isn't of kind [k]. *)
 val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit
 
+(**********************************************************)
+(*                                                        *)
+(*                                 Bullets                *)
+(*                                                        *)
+(**********************************************************)
+
+module Bullet : sig
+  type t = 
+    | Dash
+    | Star
+    | Plus
+
+  (** A [behavior] is the data of a put function which
+      is called when a bullet prefixes a tactic, together
+      with a name to identify it. *)
+  type behavior = {
+    name : string;
+    put : Proof.proof -> t -> unit
+  }
+
+  (** A registered behavior can then be accessed in Coq
+      through the command [Set Bullet Behavior "name"].
+
+      Two modes are registered originally:
+      * "Strict Subproofs":
+        - If this bullet follows another one of its kind, defocuses then focuses
+          (which fails if the focused subproof is not complete).
+        - If it is the first bullet of its kind, then focuses a new subproof.
+      * "None": bullets don't do anything *)
+  val register_behavior : behavior -> unit
+
+  (** Handles focusing/defocusing with bullets:
+       *)
+  val put : Proof.proof -> t -> unit
+end
+
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook)
 end
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 51fd69149a..3ce85c4656 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -652,48 +652,13 @@ let vernac_declare_class id =
 let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
-(* Gestion of bullets. *)
-open Store.Field
-(* 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 (get_bullets,set_bullets) =
-  let bullets = Store.field () in
-  ( begin fun pr -> Option.default [] (bullets.get (Proof.get_proof_info pr)) end ,
-    begin fun bs pr -> Proof.set_proof_info (bullets.set bs (Proof.get_proof_info pr)) pr end )
-let has_bullet bul pr =
-  let rec has_bullet = function
-    | b'::_ when bul=b' -> true
-    | _::l -> has_bullet l
-    | [] -> false
-  in
-  has_bullet (get_bullets pr)
-(* precondition: the stack is not empty *)
-let pop_bullet pr =
-  match get_bullets pr with
-  | b::stk -> Proof.unfocus bullet_kind pr ;
-                   set_bullets stk pr ;
-		   b
-  | [] -> Util.anomaly "Tried to pop bullet from an empty stack"
-let push_bullet b pr =
-  Proof.focus bullet_cond () 1 pr ;
-  set_bullets (b::get_bullets pr) pr
-
-let put_bullet p bul =
-  if has_bullet bul p then
-    begin 
-      while bul <> pop_bullet p do () done;
-      push_bullet bul p
-    end
-  else 
-    push_bullet bul p
 
 let vernac_solve n bullet tcom b =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode.";
   let p = Proof_global.give_me_the_proof () in
   Proof.transaction p begin fun () ->
-    Option.iter (put_bullet p) bullet ;
+    Option.iter (Proof_global.Bullet.put p) bullet ;
     solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b;
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index b619ca47b4..69684b78c8 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -56,10 +56,3 @@ val vernac_reset_name : identifier Util.located -> unit
 (* Print subgoals when the verbose flag is on. Meant to be used inside
     vernac commands from plugins. *)
 val print_subgoals : unit -> unit
-
-
-(* Handles focusing/defocusing with bullets:
-    - If this bullet follows another one of its kind, defocuses then focuses
-      (which fails if the focused subproof is not complete).
-    - If it is the first bullet of its kind, then focuses a new subproof. *)
-val put_bullet : Proof.proof -> bullet -> unit
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 216306f5e7..de121e93db 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -184,11 +184,6 @@ type syntax_modifier =
   | SetOnlyParsing
   | SetFormat of string located
 
-type bullet = 
-  | Dash
-  | Star
-  | Plus
-
 type proof_end =
   | Admitted
   | Proved of opacity_flag * (lident * theorem_kind option) option
@@ -276,7 +271,7 @@ type vernac_expr =
 
   (* Solving *)
 
-  | VernacSolve of int * bullet option * raw_tactic_expr * bool
+  | VernacSolve of int * Proof_global.Bullet.t option * raw_tactic_expr * bool
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)