Printing priority to most recent notation in case of non-open scopes with delim.

This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.

Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).

1 files changed, 39 insertions, 23 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 3f973b5230..ea6d0f8871 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -173,6 +173,7 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of KerName.t
 
+type scoped_notation_rule_core = scope_name * notation * interpretation * int option
 type notation_rule_core = interp_rule * interpretation * int option
 type notation_rule = notation_rule_core * delimiters option * bool
 
@@ -312,18 +313,26 @@ let key_compare k1 k2 = match k1, k2 with
 module KeyOrd = struct type t = key let compare = key_compare end
 module KeyMap = Map.Make(KeyOrd)
 
-let keymap_add key sc interp map =
-  let oldkeymap = try ScopeMap.find sc map with Not_found -> KeyMap.empty in
+let keymap_add key sc interp (scope_map,global_map) =
+  (* Adding to scope keymap for printing based on open scopes *)
+  let oldkeymap = try ScopeMap.find sc scope_map with Not_found -> KeyMap.empty in
   let oldscmap = try KeyMap.find key oldkeymap with Not_found -> [] in
   let newscmap = KeyMap.add key (interp :: oldscmap) oldkeymap in
-  ScopeMap.add sc newscmap map
+  let scope_map = ScopeMap.add sc newscmap scope_map in
+  (* Adding to global keymap of scoped notations in case the scope is not open *)
+  let global_map = match interp with
+  | NotationRule (Some sc,ntn), interp, c ->
+      let oldglobalkeymap = try KeyMap.find key global_map with Not_found -> [] in
+      KeyMap.add key ((sc,ntn,interp,c) :: oldglobalkeymap) global_map
+  | (NotationRule (None,_) | SynDefRule _), _, _ -> global_map in
+  (scope_map, global_map)
 
 let keymap_extract keys sc map =
-  let keymap, map =
-    try ScopeMap.find (Some sc) map, ScopeMap.remove (Some sc) map
-    with Not_found -> KeyMap.empty, map in
+  let keymap =
+    try ScopeMap.find (Some sc) map
+    with Not_found -> KeyMap.empty in
   let add_scope rule = (rule,(String.Map.find sc !scope_map).delimiters,false) in
-  List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys, map
+  List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys
 
 let find_with_delimiters = function
   | None -> None
@@ -332,17 +341,22 @@ let find_with_delimiters = function
         | Some key -> Some (Some key)
         | None -> None
 
-let keymap_extract_remainder keys map =
-  ScopeMap.fold (fun sc keymap acc ->
-      match find_with_delimiters sc with
-      | None -> acc
-      | Some delim ->
-         let add_scope rule = (rule,delim,true) in
-         let l = List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys in
-      l @ acc) map []
+let rec keymap_extract_remainder scope_seen = function
+  | [] -> []
+  | (sc,ntn,interp,c) :: l ->
+      if String.Set.mem sc scope_seen then keymap_extract_remainder scope_seen l
+      else
+        match find_with_delimiters (Some sc) with
+        | None -> keymap_extract_remainder scope_seen l
+        | Some delim ->
+           let rule = (NotationRule (Some sc, ntn), interp, c) in
+           (rule,delim,true) :: keymap_extract_remainder scope_seen l
 
 (* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref (ScopeMap.empty : notation_rule_core list KeyMap.t ScopeMap.t)
+let notations_key_table =
+  ref ((ScopeMap.empty, KeyMap.empty) :
+       notation_rule_core list KeyMap.t ScopeMap.t *
+       scoped_notation_rule_core list KeyMap.t)
 
 let glob_prim_constr_key c = match DAst.get c with
   | GRef (ref, _) -> Some (canonical_gr ref)
@@ -1051,13 +1065,15 @@ let interp_notation ?loc ntn local_scopes =
 
 let extract_notations scopes keys =
   if keys == [] then [] (* shortcut *) else
-  let rec aux scopes map =
+  let scope_map, global_map = !notations_key_table in
+  let rec aux scopes seen =
   match scopes with
-  | UninterpScope sc :: scopes ->
-      let l, map = keymap_extract keys sc map in l @ aux scopes map
-  | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes map
-  | [] -> keymap_extract_remainder keys map
-  in aux scopes !notations_key_table
+  | UninterpScope sc :: scopes -> keymap_extract keys sc scope_map @ aux scopes (String.Set.add sc seen)
+  | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes seen
+  | [] ->
+      let find key = try KeyMap.find key global_map with Not_found -> [] in
+      keymap_extract_remainder seen (List.flatten (List.map find keys))
+  in aux scopes String.Set.empty
 
 let uninterp_notations scopes c =
   let scopes = make_current_uninterp_scopes scopes in
@@ -1773,7 +1789,7 @@ let init () =
   init_scope_map ();
   uninterp_scope_stack := [];
   delimiters_map := String.Map.empty;
-  notations_key_table := ScopeMap.empty;
+  notations_key_table := (ScopeMap.empty,KeyMap.empty);
   scope_class_map := initial_scope_class_map;
   prim_token_interp_infos := String.Map.empty;
   prim_token_uninterp_infos := GlobRef.Map.empty