From 75f5e200f4f7eb6ca829869a8f8dada45e9751e9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 20 Jul 2018 23:37:23 +0200
Subject: 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.
---
 parsing/notgram_ops.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'parsing')

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 =
-- 
cgit v1.2.3