diff options
| -rw-r--r-- | vernac/metasyntax.ml | 38 |
1 files changed, 24 insertions, 14 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 875a69f687..8ce59c40c3 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1412,8 +1412,7 @@ type notation_obj = { notobj_scope : scope_name option; notobj_interp : interpretation; notobj_coercion : entry_coercion_kind option; - notobj_onlyparse : bool; - notobj_onlyprint : bool; + notobj_use : notation_use option; notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; notobj_specific_pp_rules : syntax_printing_extension option; @@ -1439,20 +1438,17 @@ let open_notation i (_, nobj) = let pat = nobj.notobj_interp in let deprecation = nobj.notobj_deprecation in let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in - let use = match nobj.notobj_onlyparse, nobj.notobj_onlyprint with - | false, false -> ParsingAndPrinting - | true, false -> OnlyParsing - | false, true -> OnlyPrinting - | true, true -> assert false in (* Declare the notation *) - Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation; + (match nobj.notobj_use with + | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation + | None -> ()); (* Declare specific format if any *) - match nobj.notobj_specific_pp_rules with + (match nobj.notobj_specific_pp_rules with | Some pp_sy -> if specific_format_to_declare (scope,ntn) pp_sy then Ppextend.declare_specific_notation_printing_rules (scope,ntn) ~extra:pp_sy.synext_extra pp_sy.synext_unparsing - | None -> () + | None -> ()) end let cache_notation o = @@ -1582,6 +1578,20 @@ let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in synext_extra = sd.extra; } +let warn_unused_interpretation = + CWarnings.create ~name:"unused-notation" ~category:"parsing" + (fun b -> + strbrk "interpretation is used neither for printing nor for parsing, " ++ + (if b then strbrk "the declaration could be replaced by \"Reserved Notation\"." + else strbrk "the declaration could be removed.")) + +let make_use reserved onlyparse onlyprint = + match onlyparse, onlyprint with + | false, false -> Some ParsingAndPrinting + | true, false -> Some OnlyParsing + | false, true -> Some OnlyPrinting + | true, true -> warn_unused_interpretation reserved; None + (**********************************************************************) (* Main functions about notations *) @@ -1613,14 +1623,14 @@ let add_notation_in_scope ~local deprecation df env c mods scope = let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in let notation, location = sd.info in + let use = make_use true onlyparse sd.only_printing in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (* Order is important here! *) - notobj_onlyparse = onlyparse; + notobj_use = use; notobj_coercion = coe; - notobj_onlyprint = sd.only_printing; notobj_deprecation = sd.deprecation; notobj_notation = (notation, location); notobj_specific_pp_rules = sy_pp_rules; @@ -1656,14 +1666,14 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse,coe = printability level i_typs onlyparse reversibility ac in + let use = make_use false onlyparse onlyprint in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (* Order is important here! *) - notobj_onlyparse = onlyparse; + notobj_use = use; notobj_coercion = coe; - notobj_onlyprint = onlyprint; notobj_deprecation = deprecation; notobj_notation = df'; notobj_specific_pp_rules = pp_sy; |