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

1 files changed, 39 insertions, 3 deletions

diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e32ec85ad..f9dbe3438 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