Uncountably many bullets (+,-,*,++,--,**,+++,...).

10 files changed, 52 insertions, 24 deletions

diff --git a/CHANGES b/CHANGES
index 00f15a62a..be41a7724 100644
--- a/CHANGES
+++ b/CHANGES
@@ -170,7 +170,8 @@ Tactics
   (possible source of incompatibilities solvable by avoiding clearing
   the relevant hypotheses).
 - New construct "uconstr:c" and "type_term c" to build untyped terms.
-- The good bullet (-/+/*) is suggested sometimes when user gives a wrong one.
+- New bullets --, ++, **, ---, +++, ***, ... made available.
+- The good bullet is suggested sometimes when user gives a wrong one.
 - New tactic "enough", symmetric to "assert", but with subgoals
   swapped, as a more friendly replacement of "cut".
 - In destruct/induction, experimental modifier "!" prefixing the
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index bfd045d47..52d8c09c1 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -266,7 +266,8 @@ focused with the same bullet $b$. See the example below.
 Different bullets can be used to nest levels. The scope of bullet does
 not go beyond enclosing {\tt \{} and {\tt \}}, so bullets can be
 reused as further nesting levels provided they are delimited by these.
-Available bullets are {\tt -}, {\tt +} and {\tt *} (without a
+Available bullets are {\tt -}, {\tt +}, {\tt *}, {\tt --}, {\tt ++}, {\tt **},
+{\tt ---}, {\tt +++}, {\tt ***}, ... (without a
 terminating period).
 
 The following example script illustrates all these features:
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 7eb0f28c8..c8e5b939f 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -17,7 +17,7 @@
 
 let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *)
 
-let undotted_sep = [ '{' '}' '-' '+' '*' ]
+let undotted_sep = '{' | '}' | '-'+ | '+'+ | '*'+
 
 let dot_sep = '.' (space | eof)
 
@@ -68,7 +68,7 @@ and sentence initial stamp = parse
   | undotted_sep {
       (* Separators like { or } and bullets * - + are only active
 	 at the start of a sentence *)
-      if initial then stamp (utf8_lexeme_start lexbuf) Tags.Script.sentence;
+      if initial then stamp (Lexing.lexeme_end lexbuf) Tags.Script.sentence;
       sentence initial stamp lexbuf
     }
   | space+ {
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ff5b71b91..ee3a0dcf1 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -230,9 +230,9 @@ type register_kind =
   | RegisterInline
 
 type bullet =
-    | Dash
-    | Star
-    | Plus
+    | Dash of int
+    | Star of int
+    | Plus of int
 
 (** {6 Types concerning Stm} *)
 type 'a stm_vernac =
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 84e4f55de..288263322 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -62,6 +62,14 @@ let _ = Proof_global.register_proof_mode {Proof_global.
 					    reset = set_noedit_mode
 					 }
 
+let make_bullet s =
+  let n = String.length s in
+  match s.[0] with
+  | '-' -> Dash n
+  | '+' -> Plus n
+  | '*' -> Star n
+  | _ -> assert false
+
 let default_command_entry =
   Gram.Entry.of_parser "command_entry"
     (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
@@ -129,17 +137,12 @@ GEXTEND Gram
   ;
 
   subprf:
-  [ [
-      "-" -> VernacBullet Dash
-    | "*" -> VernacBullet Star
-    | "+" -> VernacBullet Plus
+  [ [ s = BULLET -> VernacBullet (make_bullet s)
     | "{" -> VernacSubproof None
     | "}" -> VernacEndSubproof
     ] ]
   ;
 
-
-
   subgoal_command: 
     [ [ c = check_command; "." ->
                   begin function
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index d37331449..88590fa4a 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -435,6 +435,14 @@ let find_keyword id s =
   | None -> raise Not_found
   | Some c -> KEYWORD c
 
+let process_sequence bp c cs =
+  let rec aux n cs =
+    match Stream.peek cs with
+    | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs
+    | _ -> BULLET (String.make n c), (bp, Stream.count cs)
+  in
+  aux 1 cs
+
 (* Must be a special token *)
 let process_chars bp c cs =
   let t = progress_from_byte None (-1) !token_tree cs c in
@@ -495,10 +503,15 @@ let rec next_token = parser bp
       let () = match t with
       | KEYWORD "." ->
         if not (blank_or_eof s) then err (bp,ep+1) Undefined_token;
-        if Flags.do_beautify() then between_com := true;
+        between_com := true;
       | _ -> ()
       in
       (t, (bp,ep))
+  | [< ' ('-'|'+'|'*' as c); s >] ->
+      let t =
+        if !between_com then process_sequence bp c s else process_chars bp c s
+      in
+      comment_stop bp; t
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
@@ -531,7 +544,9 @@ let rec next_token = parser bp
             (try find_keyword id s with Not_found -> IDENT id), (bp, ep)
         | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) ->
             let t = process_chars bp (Stream.next s) s in
-            comment_stop bp; t
+            let new_between_com = match t with
+              (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in
+            comment_stop bp; between_com := new_between_com; t
         | EmptyStream ->
             comment_stop bp; (EOI, (bp, bp + 1))
 
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 0ff94d395..799baeb14 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -17,6 +17,7 @@ type t =
   | INT of string
   | STRING of string
   | LEFTQMARK
+  | BULLET of string
   | EOI
 
 let equal t1 t2 = match t1, t2 with
@@ -28,6 +29,7 @@ let equal t1 t2 = match t1, t2 with
 | INT s1, INT s2 -> CString.equal s1 s2
 | STRING s1, STRING s2 -> CString.equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
+| BULLET s1, BULLET s2 -> CString.equal s1 s2
 | EOI, EOI -> true
 | _ -> false
 
@@ -40,6 +42,7 @@ let extract_string = function
   | FIELD s -> s
   | INT s -> s
   | LEFTQMARK -> "?"
+  | BULLET s -> s
   | EOI -> ""
 
 let to_string = function
@@ -51,6 +54,7 @@ let to_string = function
   | INT s -> Format.sprintf "INT %s" s
   | STRING s -> Format.sprintf "STRING %S" s
   | LEFTQMARK -> "LEFTQMARK"
+  | BULLET s -> Format.sprintf "STRING %S" s
   | EOI -> "EOI"
 
 let match_keyword kwd = function
@@ -73,6 +77,7 @@ let of_pattern = function
   | "INT", s -> INT s
   | "STRING", s -> STRING s
   | "LEFTQMARK", _ -> LEFTQMARK
+  | "BULLET", s -> BULLET s
   | "EOI", _ -> EOI
   | _ -> failwith "Tok.of_pattern: not a constructor"
 
@@ -85,6 +90,7 @@ let to_pattern = function
   | INT s -> "INT", s
   | STRING s -> "STRING", s
   | LEFTQMARK -> "LEFTQMARK", ""
+  | BULLET s -> "BULLET", s
   | EOI -> "EOI", ""
 
 let match_pattern =
@@ -98,6 +104,7 @@ let match_pattern =
     | "INT", "" -> (function INT s -> s | _ -> err ())
     | "STRING", "" -> (function STRING s -> s | _ -> err ())
     | "LEFTQMARK", "" -> (function LEFTQMARK -> ""  | _ -> err ())
+    | "BULLET", "" ->  (function BULLET s -> s  | _ -> err ())
     | "EOI", "" -> (function EOI -> "" | _ -> err ())
     | pat ->
 	let tok = of_pattern pat in
diff --git a/parsing/tok.mli b/parsing/tok.mli
index a7f15c981..74f2206be 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -17,6 +17,7 @@ type t =
   | INT of string
   | STRING of string
   | LEFTQMARK
+  | BULLET of string
   | EOI
 
 val extract_string : t -> string
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 263cc6a17..d01e6a028 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -953,9 +953,9 @@ let rec pr_vernac = function
       str "with" ++ spc() ++pr_raw_tactic te
   | VernacProofMode s -> str ("Proof Mode "^s)
   | VernacBullet b -> begin match b with
-      | Dash -> str"-"
-      | Star -> str"*"
-      | Plus -> str"+"
+      | Dash n -> str (String.make n '-')
+      | Star n -> str (String.make n '*')
+      | Plus n -> str (String.make n '+')
   end ++ spc()
   | VernacSubproof None -> str "{"
   | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 96bc265fc..52282375f 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -386,16 +386,16 @@ module Bullet = struct
   exception FailedFocusBullet of t
 
   let bullet_eq b1 b2 = match b1, b2 with
-  | Vernacexpr.Dash, Vernacexpr.Dash -> true
-  | Vernacexpr.Star, Vernacexpr.Star -> true
-  | Vernacexpr.Plus, Vernacexpr.Plus -> true
+  | Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
+  | Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
+  | Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
   | _ -> false
 
   let pr_bullet b =
     match b with
-    | Vernacexpr.Dash -> str "-"
-    | Vernacexpr.Star -> str "*"
-    | Vernacexpr.Plus -> str "+"
+    | Vernacexpr.Dash n -> str (String.make n '-')
+    | Vernacexpr.Star n -> str (String.make n '*')
+    | Vernacexpr.Plus n -> str (String.make n '+')
 
   let _ = Errors.register_handler
     begin function