Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation format + new notion of format associated to a given interpretation

Ack-by: maximedenes

1 files changed, 11 insertions, 9 deletions

diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index a5ade43295..661f9c5cad 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -14,21 +14,23 @@ open Util
 open Notation
 open Notation_gram
 
-(* Uninterpreted notation levels *)
+(* Register the level of notation for parsing and printing
+   (we also register a precomputed parsing rule) *)
 
 let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
 
-let declare_notation_level ?(onlyprint=false) ntn level =
+let declare_notation_level ntn ~onlyprint parsing_rule 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.")
+    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 (level,onlyprint) !notation_level_map
+  notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map
 
-let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
-  if onlyprint' && not onlyprint then raise Not_found;
-  level
+let level_of_notation ntn =
+  NotationMap.find ntn !notation_level_map
+
+let get_defined_notations () =
+  NotationSet.elements @@ NotationMap.domain !notation_level_map
 
 (**********************************************************************)
 (* Equality *)