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

That way, bullet detection no longer depends on a global variable
indicating whether a line is starting. This causes a small change in the
recognized language. Before the commit, "--++" was recognized as a bullet
"--" followed by a keyword "++" when at the start of a line; now it is
always recognized as a keyword "--++".

This also fixes a bug in Tok.to_string as a side-effect.

5 files changed, 19 insertions, 39 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index bec891f7f..fcdc37c08 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -479,14 +479,6 @@ 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
@@ -552,12 +544,6 @@ 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 18bc8d664..5635eac7a 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -259,7 +259,6 @@ 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 50e469dd2..0f450ff9c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -33,8 +33,6 @@ 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"
@@ -45,13 +43,25 @@ 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 make_bullet s =
-  let n = String.length s in
-  match s.[0] with
-  | '-' -> Dash n
-  | '+' -> Plus n
-  | '*' -> Star n
-  | _ -> assert false
+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)
 
 GEXTEND Gram
   GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command;
@@ -102,13 +112,6 @@ 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 8ae106512..99d5c972c 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -18,7 +18,6 @@ type t =
   | INT of string
   | STRING of string
   | LEFTQMARK
-  | BULLET of string
   | EOI
 
 let equal t1 t2 = match t1, t2 with
@@ -30,7 +29,6 @@ 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
 
@@ -42,7 +40,6 @@ let extract_string = function
   | FIELD s -> s
   | INT s -> s
   | LEFTQMARK -> "?"
-  | BULLET s -> s
   | EOI -> ""
 
 let to_string = function
@@ -53,7 +50,6 @@ 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
@@ -75,7 +71,6 @@ 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"
 
@@ -87,7 +82,6 @@ let to_pattern = function
   | INT s -> "INT", s
   | STRING s -> "STRING", s
   | LEFTQMARK -> "LEFTQMARK", ""
-  | BULLET s -> "BULLET", s
   | EOI -> "EOI", ""
 
 let match_pattern =
@@ -100,7 +94,6 @@ 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 b9286c53e..b1e79dc90 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -16,7 +16,6 @@ type t =
   | INT of string
   | STRING of string
   | LEFTQMARK
-  | BULLET of string
   | EOI
 
 val equal : t -> t -> bool