diff options
| author | Hugo Herbelin | 2019-10-05 22:07:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-21 18:49:31 +0100 |
| commit | d8dc892dc4e50462163053124c9bafcd312433a5 (patch) | |
| tree | ac389a9bcdc6444296d89aa2af1ad113c014dde2 /parsing/notgram_ops.ml | |
| parent | e1f2a1b97bb61e9c5ebaffda55a3be1ea3267c6b (diff) | |
Notations: Avoiding computing parsing rule when in onlyprinting mode.
In particular, this fixes #9741.
Diffstat (limited to 'parsing/notgram_ops.ml')
| -rw-r--r-- | parsing/notgram_ops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index 661f9c5cad..a84d2a4cb0 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -15,16 +15,16 @@ open Notation open Notation_gram (* Register the level of notation for parsing and printing - (we also register a precomputed parsing rule) *) + (also register the parsing rule if not onlyprinting) *) let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty -let declare_notation_level ntn ~onlyprint parsing_rule level = +let declare_notation_level ntn parsing_rule level = try let _ = NotationMap.find ntn !notation_level_map in anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") with Not_found -> - notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map + notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map let level_of_notation ntn = NotationMap.find ntn !notation_level_map |