aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml424
-rw-r--r--parsing/g_tactic.ml412
-rw-r--r--parsing/g_vernac.ml454
3 files changed, 57 insertions, 33 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index b04c7633a..711d2240b 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -206,12 +206,16 @@ let check_keyword str =
in
loop_symb (Stream.of_string str)
+let warn_unparsable_keyword =
+ CWarnings.create ~name:"unparsable-keyword" ~category:"parsing"
+ (fun (s,unicode) ->
+ strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
+ which will not be parsable." s unicode))
+
let check_keyword_to_add s =
try check_keyword s
with Error.E (UnsupportedUnicode unicode) ->
- Flags.if_verbose Feedback.msg_warning
- (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
- which will not be parsable." s unicode))
+ warn_unparsable_keyword (s,unicode)
let check_ident str =
let rec loop_id intail = parser
@@ -316,6 +320,14 @@ let rec number_or_index loc bp l len = parser
| ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 loc l len
| _ -> true, len
+let warn_comment_terminator_in_string =
+ CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing"
+ (fun () ->
+ (strbrk
+ "Not interpreting \"*)\" as the end of current \
+ non-terminated comment because it occurs in a \
+ non-terminated string of the comment."))
+
(* If the string being lexed is in a comment, [comm_level] is Some i with i the
current level of comments nesting. Otherwise, [comm_level] is None. *)
let rec string loc ~comm_level bp len = parser
@@ -335,11 +347,7 @@ let rec string loc ~comm_level bp len = parser
| [< '')'; s >] ->
let () = match comm_level with
| Some 0 ->
- Feedback.msg_warning
- (strbrk
- "Not interpreting \"*)\" as the end of current \
- non-terminated comment because it occurs in a \
- non-terminated string of the comment.")
+ warn_comment_terminator_in_string ~loc:!@loc ()
| _ -> ()
in
let comm_level = Option.map pred comm_level in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d0bca9ee3..8a83bc2d1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -211,6 +211,10 @@ let merge_occurrences loc cl = function
in
(Some p, ans)
+let warn_deprecated_eqn_syntax =
+ CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated"
+ (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg))
+
(* Auxiliary grammar rules *)
GEXTEND Gram
@@ -469,11 +473,11 @@ GEXTEND Gram
eqn_ipat:
[ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
| IDENT "_eqn"; ":"; pat = naming_intropattern ->
- let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in
- Feedback.msg_warning (strbrk msg); Some (!@loc, pat)
+ let loc = !@loc in
+ warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat)
| IDENT "_eqn" ->
- let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in
- Feedback.msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
+ let loc = !@loc in
+ warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous)
| -> None ] ]
;
as_name:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f0475ee25..ecbe3ac96 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -123,16 +123,18 @@ GEXTEND Gram
;
END
-let test_plural_form = function
+let warn_plural_command =
+ CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:Disabled
+ (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd))
+
+let test_plural_form loc kwd = function
| [(_,([_],_))] ->
- Flags.if_verbose Feedback.msg_warning
- (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
+ warn_plural_command ~loc:!@loc kwd
| _ -> ()
-let test_plural_form_types = function
+let test_plural_form_types loc kwd = function
| [([_],_)] ->
- Flags.if_verbose Feedback.msg_warning
- (strbrk "Keywords Implicit Types expect more than one type")
+ warn_plural_command ~loc:!@loc kwd
| _ -> ()
let fresh_var env c =
@@ -155,8 +157,8 @@ GEXTEND Gram
VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
| stre = assumption_token; nl = inline; bl = assum_list ->
VernacAssumption (stre, nl, bl)
- | stre = assumptions_token; nl = inline; bl = assum_list ->
- test_plural_form bl;
+ | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
+ test_plural_form loc kwd bl;
VernacAssumption (stre, nl, bl)
| d = def_token; id = pidentref; b = def_body ->
VernacDefinition (d, id, b)
@@ -209,11 +211,11 @@ GEXTEND Gram
| IDENT "Conjecture" -> (None, Conjectural) ] ]
;
assumptions_token:
- [ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
- | IDENT "Variables" -> (Some Discharge, Definitional)
- | IDENT "Axioms" -> (None, Logical)
- | IDENT "Parameters" -> (None, Definitional)
- | IDENT "Conjectures" -> (None, Conjectural) ] ]
+ [ [ kwd = IDENT "Hypotheses" -> (kwd, (Some Discharge, Logical))
+ | kwd = IDENT "Variables" -> (kwd, (Some Discharge, Definitional))
+ | kwd = IDENT "Axioms" -> (kwd, (None, Logical))
+ | kwd = IDENT "Parameters" -> (kwd, (None, Definitional))
+ | kwd = IDENT "Conjectures" -> (kwd, (None, Conjectural)) ] ]
;
inline:
[ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
@@ -422,6 +424,10 @@ let starredidentreflist_to_expr l =
| [] -> SsEmpty
| x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
+let warn_deprecated_include_type =
+ CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated"
+ (fun () -> strbrk "Include Type is deprecated; use Include instead")
+
(* Modules and Sections *)
GEXTEND Gram
GLOBAL: gallina_ext module_expr module_type section_subset_expr;
@@ -461,9 +467,8 @@ GEXTEND Gram
| IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
VernacInclude(e::l)
| IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
- Flags.if_verbose
- Feedback.msg_warning (strbrk "Include Type is deprecated; use Include instead");
- VernacInclude(e::l) ] ]
+ warn_deprecated_include_type ~loc:!@loc ();
+ VernacInclude(e::l) ] ]
;
export_token:
[ [ IDENT "Import" -> Some false
@@ -567,6 +572,14 @@ GEXTEND Gram
;
END
+let warn_deprecated_arguments_scope =
+ CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated"
+ (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead")
+
+let warn_deprecated_implicit_arguments =
+ CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated"
+ (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead")
+
(* Extensions: implicits, coercions, etc. *)
GEXTEND Gram
GLOBAL: gallina_ext instance_name;
@@ -681,22 +694,21 @@ GEXTEND Gram
(* moved there so that camlp5 factors it with the previous rule *)
| IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
"["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
- Feedback. msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
+ warn_deprecated_arguments_scope ~loc:!@loc ();
VernacArgumentsScope (qid,scl)
(* Implicit *)
| IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
- Flags.if_verbose
- Feedback.msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
- VernacDeclareImplicits (qid,pos)
+ warn_deprecated_implicit_arguments ~loc:!@loc ();
+ VernacDeclareImplicits (qid,pos)
| IDENT "Implicit"; "Type"; bl = reserv_list ->
VernacReserve bl
| IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
- test_plural_form_types bl;
+ test_plural_form_types loc "Implicit Types" bl;
VernacReserve bl
| IDENT "Generalizable";
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 16:33:05 +0000