diff options
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 4 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 2 | ||||
| -rw-r--r-- | ide/coqide/coq_lex.mll | 74 | ||||
| -rw-r--r-- | parsing/cLexer.ml | 39 |
6 files changed, 64 insertions, 60 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 11162ec96b..d533470f22 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -298,7 +298,7 @@ Summary of the commands .. cmd:: Class @inductive_definition {* with @inductive_definition } The :cmd:`Class` command is used to declare a typeclass with parameters - :token:`binders` and fields the declared record fields. + :n:`{* @binder }` and fields the declared record fields. Like any command declaring a record, this command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, @@ -337,7 +337,7 @@ Summary of the commands fields defined by :token:`field_def`, where each field must be a declared field of the class. - An arbitrary context of :token:`binders` can be put after the name of the + An arbitrary context of :n:`{* @binder }` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for :tacn:`auto` hints. If the priority :token:`natural` is not specified, it defaults to the number diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index ee8784fc02..a8a574c861 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -183,11 +183,8 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ - 'binders', 'collection', - 'modpath', 'tactic', - 'destruction_arg', 'bindings', 'induction_clause', 'conversion', diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index ca69072cb9..f8375e93ce 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -217,7 +217,7 @@ usual implicit arguments disambiguation syntax. The syntax is also supported in internal binders. For instance, in the following kinds of expressions, the type of each declaration present -in :token:`binders` can be bracketed to mark the declaration as +in :n:`{* @binder }` can be bracketed to mark the declaration as implicit: * :n:`fun (@ident:forall {* @binder }, @type) => @term`, * :n:`forall (@ident:forall {* @binder }, @type), @type`, diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index e05be7c2c2..8e23e61018 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -203,7 +203,7 @@ Generation of inversion principles with ``Derive`` ``Inversion`` This command generates an inversion principle for the :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name of the generated principle. The second :token:`ident` should be an inductive - predicate, and :token:`binders` the variables occurring in the term + predicate, and :n:`{* @binder }` the variables occurring in the term :token:`term`. This command generates the inversion lemma for the sort :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`. When applied, it is equivalent to having inverted the instance with the diff --git a/ide/coqide/coq_lex.mll b/ide/coqide/coq_lex.mll index a65954d566..5d5e5f0e14 100644 --- a/ide/coqide/coq_lex.mll +++ b/ide/coqide/coq_lex.mll @@ -50,52 +50,40 @@ and comment = parse | utf8_extra_byte { incr utf8_adjust; comment lexbuf } | _ { comment lexbuf } -and quotation o c n l = parse +and quotation n l = parse | eof { raise Unterminated } -| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } -| _ { - let x = Lexing.lexeme lexbuf in - if x = o then quotation_nesting o c n l 1 lexbuf - else if x = c then - if n = 1 && l = 1 then () - else quotation_closing o c n l 1 lexbuf - else quotation o c n l lexbuf -} +| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf } +| "{" { quotation_nesting n l 1 lexbuf } +| "}" { quotation_closing n l 1 lexbuf } +| _ { quotation n l lexbuf } -and quotation_nesting o c n l v = parse +and quotation_nesting n l v = parse | eof { raise Unterminated } -| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } -| _ { - let x = Lexing.lexeme lexbuf in - if x = o then - if n = v+1 then quotation o c n (l+1) lexbuf - else quotation_nesting o c n l (v+1) lexbuf - else if x = c then quotation_closing o c n l 1 lexbuf - else quotation o c n l lexbuf +| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf } +| "{" { + if n = v+1 then quotation n (l+1) lexbuf + else quotation_nesting n l (v+1) lexbuf } +| "}" { quotation_closing n l 1 lexbuf } +| _ { quotation n l lexbuf } -and quotation_closing o c n l v = parse +and quotation_closing n l v = parse | eof { raise Unterminated } -| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } -| _ { - let x = Lexing.lexeme lexbuf in - if x = c then - if n = v+1 then - if l = 1 then () - else quotation o c n (l-1) lexbuf - else quotation_closing o c n l (v+1) lexbuf - else if x = o then quotation_nesting o c n l 1 lexbuf - else quotation o c n l lexbuf +| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf } +| "}" { + if n = v+1 then + if l = 1 then () + else quotation n (l-1) lexbuf + else quotation_closing n l (v+1) lexbuf } +| "{" { quotation_nesting n l 1 lexbuf } +| _ { quotation n l lexbuf } -and quotation_start o c n = parse +and quotation_start n = parse | eof { raise Unterminated } -| utf8_extra_byte { incr utf8_adjust; quotation o c n 1 lexbuf } -| _ { - let x = Lexing.lexeme lexbuf in - if x = o then quotation_start o c (n+1) lexbuf - else quotation o c n 1 lexbuf -} +| utf8_extra_byte { incr utf8_adjust; quotation n 1 lexbuf } +| "{" { quotation_start (n+1) lexbuf } +| _ { quotation n 1 lexbuf } (** NB : [mkiter] should be called on increasing offsets *) @@ -130,16 +118,8 @@ and sentence initial stamp = parse if initial then stamp (utf8_lexeme_start lexbuf + String.length (Lexing.lexeme lexbuf) - 1) Tags.Script.sentence; sentence initial stamp lexbuf } - | ['a'-'z' 'A'-'Z'] ":{" { - quotation_start "{" "}" 1 lexbuf; - sentence false stamp lexbuf - } - | ['a'-'z' 'A'-'Z'] ":[" { - quotation_start "[" "]" 1 lexbuf; - sentence false stamp lexbuf - } - | ['a'-'z' 'A'-'Z'] ":(" { - quotation_start "(" ")" 1 lexbuf; + | ['a'-'z' 'A'-'Z'] ":{{" { + quotation_start 2 lexbuf; sentence false stamp lexbuf } | space+ { diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index a98cf3b7de..f485970eec 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -512,6 +512,12 @@ and progress_utf8 loc last nj n c tt cs = and progress_from_byte loc last nj tt cs c = progress_utf8 loc last nj (utf8_char_size loc cs c) c tt cs +let blank_or_eof cs = + match Stream.peek cs with + | None -> true + | Some (' ' | '\t' | '\n' |'\r') -> true + | _ -> false + type marker = Delimited of int * char list * char list | ImmediateAsciiIdent let peek_marker_len b e s = @@ -542,6 +548,11 @@ let parse_quotation loc bp s = in get_buff len, set_loc_pos loc bp (Stream.count s) | Delimited (lenmarker, bmarker, emarker) -> + let dot_gobbling = + (* only quotations starting with two curly braces can gobble sentences *) + match bmarker with + | '{' :: '{' :: _ -> true + | _ -> false in let b = Buffer.create 80 in let commit1 c = Buffer.add_char b c; Stream.junk s in let commit l = List.iter commit1 l in @@ -557,6 +568,10 @@ let parse_quotation loc bp s = commit1 '\n'; let loc = bump_loc_line_last loc (Stream.count s) in quotation loc depth + | '.' :: _ -> + commit1 '.'; + if not dot_gobbling && blank_or_eof s then raise Stream.Failure; + quotation loc depth | c :: cs -> commit1 c; quotation loc depth @@ -565,8 +580,26 @@ let parse_quotation loc bp s = let loc = quotation loc 0 in Buffer.contents b, set_loc_pos loc bp (Stream.count s) +let peek_string v s = + let l = String.length v in + let rec aux i = + if Int.equal i l then true + else + let l' = Stream.npeek (i + 1) s in + match List.nth l' i with + | c -> Char.equal c v.[i] && aux (i + 1) + | exception _ -> false (* EOF *) in + aux 0 let find_keyword loc id bp s = + if peek_string ":{{" s then + begin + (* "xxx:{{" always starts a sentence-gobbling quotation, whether registered or not *) + Stream.junk s; + let txt, loc = parse_quotation loc bp s in + QUOTATION (id ^ ":", txt), loc + end + else let tt = ttree_find !token_tree id in match progress_further loc tt.node 0 tt s with | None -> raise Not_found @@ -645,12 +678,6 @@ let parse_after_qmark ~diff_mode loc bp s = | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars ~diff_mode loc bp '?' s) -let blank_or_eof cs = - match Stream.peek cs with - | None -> true - | Some (' ' | '\t' | '\n' |'\r') -> true - | _ -> false - (* Parse a token in a char stream *) let rec next_token ~diff_mode loc s = |