Revert "Move bullet detection from lexer to parser (bug #5102)."

This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.

5 files changed, 39 insertions, 19 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index fcdc37c08..bec891f7f 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -479,6 +479,14 @@ let find_keyword loc id s =
   | None -> raise Not_found
   | Some c -> KEYWORD c
 
+let process_sequence loc 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), set_loc_pos loc bp (Stream.count cs)
+  in
+  aux 1 cs
+
 (* Must be a special token *)
 let process_chars loc bp c cs =
   let t = progress_from_byte loc None (-1) !token_tree cs c in
@@ -544,6 +552,12 @@ let rec next_token loc = parser bp
       | _ -> ()
       in
       (t, set_loc_pos loc bp ep)
+  | [< ' ('-'|'+'|'*' as c); s >] ->
+      let t,new_between_com =
+        if !between_com then process_sequence loc bp c s, true
+        else process_chars loc bp c s,false
+      in
+      comment_stop bp; between_com := new_between_com; t
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark loc bp s in
       comment_stop bp; (t, set_loc_pos loc ep bp)
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 5635eac7a..18bc8d664 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -259,6 +259,7 @@ IFDEF CAMLP5 THEN
     | Tok.INT s -> "INT", s
     | Tok.STRING s -> "STRING", s
     | Tok.LEFTQMARK -> "LEFTQMARK", ""
+    | Tok.BULLET s -> "BULLET", s
     | Tok.EOI -> "EOI", ""
     in
     Gramext.Stoken pattern
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 04f553ba2..96eede2b9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -33,6 +33,8 @@ let _ = List.iter CLexer.add_keyword vernac_kw
 
 let query_command = Gram.entry_create "vernac:query_command"
 
+let subprf = Gram.entry_create "vernac:subprf"
+
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
 let thm_token = Gram.entry_create "vernac:thm_token"
 let def_body = Gram.entry_create "vernac:def_body"
@@ -43,25 +45,13 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
 let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
-let subprf = Gram.Entry.of_parser "vernac:subprf" (fun strm ->
-  match get_tok (Stream.peek strm) with
-  | Some (KEYWORD "{") -> Stream.junk strm; VernacSubproof None
-  | Some (KEYWORD "}") -> Stream.junk strm; VernacEndSubproof
-  | Some (KEYWORD k) ->
-    (match k.[0] with
-    | ('-'|'+'|'*') as c ->
-      let n = String.length k in
-      for i = 1 to n - 1 do
-        if k.[i] != c then raise Stream.Failure
-      done;
-      Stream.junk strm;
-      VernacBullet (match c with
-        | '-' -> Dash n
-        | '+' -> Plus n
-        | '*' -> Star n
-        | _ -> assert false)
-    | _ -> raise Stream.Failure)
-  | _ -> raise Stream.Failure)
+let make_bullet s =
+  let n = String.length s in
+  match s.[0] with
+  | '-' -> Dash n
+  | '+' -> Plus n
+  | '*' -> Star n
+  | _ -> assert false
 
 GEXTEND Gram
   GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command;
@@ -112,6 +102,13 @@ GEXTEND Gram
     [ [ c = subgoal_command -> c None] ]
   ;
 
+  subprf:
+  [ [ s = BULLET -> VernacBullet (make_bullet s)
+    | "{" -> VernacSubproof None
+    | "}" -> VernacEndSubproof
+    ] ]
+  ;
+
   subgoal_command:
     [ [ c = query_command; "." ->
                   begin function
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 99d5c972c..8ae106512 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -18,6 +18,7 @@ type t =
   | INT of string
   | STRING of string
   | LEFTQMARK
+  | BULLET of string
   | EOI
 
 let equal t1 t2 = match t1, t2 with
@@ -29,6 +30,7 @@ let equal t1 t2 = match t1, t2 with
 | INT s1, INT s2 -> string_equal s1 s2
 | STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
+| BULLET s1, BULLET s2 -> string_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
@@ -50,6 +53,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
@@ -71,6 +75,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"
 
@@ -82,6 +87,7 @@ let to_pattern = function
   | INT s -> "INT", s
   | STRING s -> "STRING", s
   | LEFTQMARK -> "LEFTQMARK", ""
+  | BULLET s -> "BULLET", s
   | EOI -> "EOI", ""
 
 let match_pattern =
@@ -94,6 +100,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 b1e79dc90..b9286c53e 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -16,6 +16,7 @@ type t =
   | INT of string
   | STRING of string
   | LEFTQMARK
+  | BULLET of string
   | EOI
 
 val equal : t -> t -> bool