diff options
-rw-r--r-- | CHANGES | 3 | ||||
-rw-r--r-- | doc/refman/RefMan-pro.tex | 3 | ||||
-rw-r--r-- | ide/coq_lex.mll | 4 | ||||
-rw-r--r-- | intf/vernacexpr.mli | 6 | ||||
-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 | ||||
-rw-r--r-- | printing/ppvernac.ml | 6 | ||||
-rw-r--r-- | proofs/proof_global.ml | 12 |
10 files changed, 52 insertions, 24 deletions
@@ -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 |