diff options
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/cLexer.ml4 | 14 | ||||
-rw-r--r-- | parsing/compat.ml4 | 1 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 35 | ||||
-rw-r--r-- | parsing/tok.ml | 7 | ||||
-rw-r--r-- | parsing/tok.mli | 1 |
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 |