aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml78
-rw-r--r--parsing/cLexer.mli2
-rw-r--r--parsing/extend.ml2
-rw-r--r--parsing/g_constr.mlg2
-rw-r--r--parsing/g_prim.mlg2
-rw-r--r--parsing/notation_gram.ml2
-rw-r--r--parsing/notgram_ops.ml2
-rw-r--r--parsing/notgram_ops.mli2
-rw-r--r--parsing/pcoq.ml17
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/ppextend.ml2
-rw-r--r--parsing/ppextend.mli2
-rw-r--r--parsing/tok.ml2
-rw-r--r--parsing/tok.mli2
14 files changed, 77 insertions, 42 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 42ca5f8c05..a27d6450b7 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -548,7 +548,7 @@ let peek_marker s =
| ('a'..'z' | 'A'..'Z' | '_') -> ImmediateAsciiIdent
| _ -> raise Stream.Failure
-let parse_quotation loc s =
+let parse_quotation loc bp s =
match peek_marker s with
| ImmediateAsciiIdent ->
let c = Stream.next s in
@@ -556,34 +556,42 @@ let parse_quotation loc s =
try ident_tail loc (store 0 c) s with
Stream.Failure -> raise (Stream.Error "")
in
- get_buff len
+ get_buff len, set_loc_pos loc bp (Stream.count s)
| Delimited (lenmarker, bmarker, emarker) ->
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
- let rec quotation depth =
+ let rec quotation loc depth =
match Stream.npeek lenmarker s with
| l when l = bmarker ->
commit l;
- quotation (depth + 1)
+ quotation loc (depth + 1)
| l when l = emarker ->
commit l;
- if depth > 1 then quotation (depth - 1)
+ if depth > 1 then quotation loc (depth - 1) else loc
+ | '\n' :: cs ->
+ commit1 '\n';
+ let loc = bump_loc_line_last loc (Stream.count s) in
+ quotation loc depth
| c :: cs ->
commit1 c;
- quotation depth
+ quotation loc depth
| [] -> raise Stream.Failure
in
- quotation 0;
- Buffer.contents b
+ let loc = quotation loc 0 in
+ Buffer.contents b, set_loc_pos loc bp (Stream.count s)
-let find_keyword loc id s =
+let find_keyword loc id bp s =
let tt = ttree_find !token_tree id in
match progress_further loc tt.node 0 tt s with
| None -> raise Not_found
- | Some (c,NoQuotation) -> KEYWORD c
- | Some (c,Quotation) -> QUOTATION(c, parse_quotation loc s)
+ | Some (c,NoQuotation) ->
+ let ep = Stream.count s in
+ KEYWORD c, set_loc_pos loc bp ep
+ | Some (c,Quotation) ->
+ let txt, loc = parse_quotation loc bp s in
+ QUOTATION(c, txt), loc
let process_sequence loc bp c cs =
let rec aux n cs =
@@ -599,7 +607,9 @@ let process_chars ~diff_mode loc bp c cs =
let ep = Stream.count cs in
match t with
| Some (t,NoQuotation) -> (KEYWORD t, set_loc_pos loc bp ep)
- | Some (c,Quotation) -> (QUOTATION(c, parse_quotation loc cs), set_loc_pos loc bp ep)
+ | Some (c,Quotation) ->
+ let txt, loc = parse_quotation loc bp cs in
+ QUOTATION(c, txt), loc
| None ->
let ep' = bp + utf8_char_size loc cs c in
if diff_mode then begin
@@ -623,14 +633,21 @@ let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with
Stream.Failure -> raise (Stream.Error "")
in
let field = get_buff len in
- (try find_keyword loc ("."^field) s with Not_found -> FIELD field)
+ begin try find_keyword loc ("."^field) bp s
+ with Not_found ->
+ let ep = Stream.count s in
+ FIELD field, set_loc_pos loc bp ep end
| _ ->
match lookup_utf8 loc s with
| Utf8Token (st, n) when Unicode.is_valid_ident_initial st ->
let len = ident_tail loc (nstore n 0 s) s in
let field = get_buff len in
- (try find_keyword loc ("."^field) s with Not_found -> FIELD field)
- | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars ~diff_mode loc bp c s)
+ begin try find_keyword loc ("."^field) bp s
+ with Not_found ->
+ let ep = Stream.count s in
+ FIELD field, set_loc_pos loc bp ep end
+ | AsciiChar | Utf8Token _ | EmptyStream ->
+ process_chars ~diff_mode loc bp c s
(* Parse what follows a question mark *)
@@ -664,22 +681,23 @@ let rec next_token ~diff_mode loc s =
comm_loc bp; push_char c; next_token ~diff_mode loc s
| Some ('.' as c) ->
Stream.junk s;
- let t =
+ let t, newloc =
try parse_after_dot ~diff_mode loc c bp s with
Stream.Failure -> raise (Stream.Error "")
in
- let ep = Stream.count s in
comment_stop bp;
(* We enforce that "." should either be part of a larger keyword,
for instance ".(", or followed by a blank or eof. *)
let () = match t with
- | KEYWORD ("." | "...") ->
- if not (blank_or_eof s) then
- err (set_loc_pos loc bp (ep+1)) Undefined_token;
- between_commands := true;
- | _ -> ()
+ | KEYWORD ("." | "...") ->
+ if not (blank_or_eof s) then begin
+ let ep = Stream.count s in
+ err (set_loc_pos loc bp (ep+1)) Undefined_token
+ end;
+ between_commands := true;
+ | _ -> ()
in
- t, set_loc_pos loc bp ep
+ t, newloc
| Some ('-' | '+' | '*' as c) ->
Stream.junk s;
let t,new_between_commands =
@@ -698,10 +716,12 @@ let rec next_token ~diff_mode loc s =
try ident_tail loc (store 0 c) s with
Stream.Failure -> raise (Stream.Error "")
in
- let ep = Stream.count s in
let id = get_buff len in
comment_stop bp;
- (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
+ begin try find_keyword loc id bp s
+ with Not_found ->
+ let ep = Stream.count s in
+ IDENT id, set_loc_pos loc bp ep end
| Some ('0'..'9') ->
let n = NumTok.parse s in
let ep = Stream.count s in
@@ -745,9 +765,11 @@ let rec next_token ~diff_mode loc s =
| Utf8Token (st, n) when Unicode.is_valid_ident_initial st ->
let len = ident_tail loc (nstore n 0 s) s in
let id = get_buff len in
- let ep = Stream.count s in
comment_stop bp;
- (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
+ begin try find_keyword loc id bp s
+ with Not_found ->
+ let ep = Stream.count s in
+ IDENT id, set_loc_pos loc bp ep end
| AsciiChar | Utf8Token _ ->
let t = process_chars ~diff_mode loc bp (Stream.next s) s in
comment_stop bp; t
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 464bcf614d..964689f5f5 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index dd7c301dfb..63e121c0d1 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 79cfe33b12..8fdec7d1a8 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 9653964262..c1f52c5b39 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 6df0d6f21a..9f133ca9d4 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 5cc1292c92..009dafdb13 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index f427a607b7..c31f4505e7 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b375c526ad..3aaba27579 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -363,8 +363,21 @@ end
module Grammar = Register(GrammarObj)
+let warn_deprecated_intropattern =
+ let open CWarnings in
+ create ~name:"deprecated-intropattern-entry" ~category:"deprecated"
+ (fun () -> Pp.strbrk "Entry name intropattern has been renamed in order \
+ to be consistent with the documented grammar of tactics. Use \
+ \"simple_intropattern\" instead.")
+
+let check_compatibility = function
+ | Genarg.ExtraArg s when ArgT.repr s = "intropattern" -> warn_deprecated_intropattern ()
+ | _ -> ()
+
let register_grammar = Grammar.register0
-let genarg_grammar = Grammar.obj
+let genarg_grammar x =
+ check_compatibility x;
+ Grammar.obj x
let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t =
let e = new_entry u s in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 196835f184..cde867d2ef 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index e1f5e20117..7368f4109e 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 7eb5967a3e..be5af75e72 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 71e2d4aa80..419b5a3d7f 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/parsing/tok.mli b/parsing/tok.mli
index a5fb5ad9cd..a6cb4f8506 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 11:04:33 +0000