diff options
| author | Hugo Herbelin | 2018-07-20 23:37:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-02 13:18:14 +0200 |
| commit | 75f5e200f4f7eb6ca829869a8f8dada45e9751e9 (patch) | |
| tree | 033d58b65bb24a2cef81fea1ff4e0d60a67930f3 | |
| parent | 6f1c4ac389e595e09fdf4653847d8c3ccca0befb (diff) | |
Fixing #8106 (anomaly if declaring levels for only printing then only parsing).
Notations were not initially designed to support independent parsing
and printing rules. Some redesign of this part of the code shall be
necessary at some time.
| -rw-r--r-- | parsing/notgram_ops.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/8106.v | 4 |
2 files changed, 8 insertions, 2 deletions
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index c36b3b17bf..5cc1292c92 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -19,8 +19,10 @@ open Notation_gram let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty let declare_notation_level ?(onlyprint=false) ntn level = - if NotationMap.mem ntn !notation_level_map then - anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level."); + try + let (level,onlyprint) = NotationMap.find ntn !notation_level_map in + if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") + with Not_found -> notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map let level_of_notation ?(onlyprint=false) ntn = diff --git a/test-suite/bugs/closed/8106.v b/test-suite/bugs/closed/8106.v new file mode 100644 index 0000000000..a711c5adef --- /dev/null +++ b/test-suite/bugs/closed/8106.v @@ -0,0 +1,4 @@ +(* Was raising an anomaly "already assigned a level" on the second line *) + +Notation "c1 ; c2" := (c1 + c2) (only printing, at level 76, right associativity, c1 at level 76, c2 at level 76). +Notation "c1 ; c2" := (c1 + c2) (only parsing, at level 76, right associativity, c2 at level 76). |