diff options
| -rw-r--r-- | interp/notation.ml | 10 | ||||
| -rw-r--r-- | interp/notation.mli | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/7462.v | 7 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 6 |
4 files changed, 18 insertions, 9 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 76d0efb72..20e46bfe3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -429,13 +429,15 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* Uninterpreted notation levels *) -let declare_notation_level ntn level = +let declare_notation_level ?(onlyprint=false) ntn level = if String.Map.mem ntn !notation_level_map then anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); - notation_level_map := String.Map.add ntn level !notation_level_map + notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map -let level_of_notation ntn = - String.Map.find ntn !notation_level_map +let level_of_notation ?(onlyprint=false) ntn = + let (level,onlyprint') = String.Map.find ntn !notation_level_map in + if onlyprint' && not onlyprint then raise Not_found; + level (* The mapping between notations and their interpretation *) diff --git a/interp/notation.mli b/interp/notation.mli index eac87414f..ccc67fe49 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -137,8 +137,8 @@ val availability_of_notation : scope_name option * notation -> local_scopes -> (** {6 Declare and test the level of a (possibly uninterpreted) notation } *) -val declare_notation_level : notation -> level -> unit -val level_of_notation : notation -> level (** raise [Not_found] if no level *) +val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit +val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) (** {6 Miscellaneous} *) diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v index 37af64caa..40ca39e38 100644 --- a/test-suite/bugs/closed/7462.v +++ b/test-suite/bugs/closed/7462.v @@ -4,3 +4,10 @@ Notation "$ x" := (@id nat x) (only parsing, at level 0). Notation "$ x" := (@id bool x) (only printing, at level 0). Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *) + +(* Adding an only-printing notation should not let believe + that a parsing rule has been given *) + +Notation "$ x" := (@id bool x) (only printing, at level 0). +Notation "$ x" := (@id nat x) (only parsing, at level 0). +Check $1. (* Was: Error: Syntax Error: Lexer: Undefined token *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index feeca6075..76958b05f 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -738,12 +738,12 @@ let cache_one_syntax_extension se = let prec = se.synext_level in let onlyprint = se.synext_notgram.notgram_onlyprinting in try - let oldprec = Notation.level_of_notation ntn in + let oldprec = Notation.level_of_notation ~onlyprint ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> if is_active_compat se.synext_compat then begin (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; + Notation.declare_notation_level ntn prec ~onlyprint; (* Declare the parsing rule *) if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) @@ -1274,7 +1274,7 @@ exception NoSyntaxRule let recover_notation_syntax ntn = try - let prec = Notation.level_of_notation ntn in + let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in let pp_rule,_ = Notation.find_notation_printing_rule ntn in let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in let pa_rule = Notation.find_notation_parsing_rules ntn in |