diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:08:48 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:24 +0200 |
commit | 467db5040fe2f311f8f5493f89dc8f95647a9a0b (patch) | |
tree | 5ebbe4139abc44bbef7362aa860c57711d6dcfd9 /parsing | |
parent | 8e3c749e69649fb45750355e464ce7c16a4462c7 (diff) |
Uncountably many bullets (+,-,*,++,--,**,+++,...).
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/g_vernac.ml4 | 15 | ||||
-rw-r--r-- | parsing/lexer.ml4 | 19 | ||||
-rw-r--r-- | parsing/tok.ml | 7 | ||||
-rw-r--r-- | parsing/tok.mli | 1 |
4 files changed, 34 insertions, 8 deletions
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 |