Notation: option to attach extra pretty printing rules to notations

so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).

Available syntax:
- all in one:
  Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
  Format Notation "a /\ b" "latex" "#1 \wedge #2".

2 files changed, 21 insertions, 6 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index e765701d48..93e6f31c03 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -940,17 +940,28 @@ let pr_visibility prglob = function
 (* Mapping notations to concrete syntax *)
 
 type unparsing_rule = unparsing list * precedence
-
+type extra_unparsing_rules = (string * string) list
 (* Concrete syntax for symbolic-extension table *)
 let printing_rules =
-  ref (String.Map.empty : unparsing_rule String.Map.t)
+  ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t)
 
-let declare_notation_printing_rule ntn unpl =
-  printing_rules := String.Map.add ntn unpl !printing_rules
+let declare_notation_printing_rule ntn ~extra unpl =
+  printing_rules := String.Map.add ntn (unpl,extra) !printing_rules
 
 let find_notation_printing_rule ntn =
-  try String.Map.find ntn !printing_rules
+  try fst (String.Map.find ntn !printing_rules)
   with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
+let find_notation_extra_printing_rules ntn =
+  try snd (String.Map.find ntn !printing_rules)
+  with Not_found -> []
+let add_notation_extra_printing_rule ntn k v =
+  try
+    printing_rules := 
+      let p, pp = String.Map.find ntn !printing_rules in
+      String.Map.add ntn (p, (k,v) :: pp) !printing_rules
+  with Not_found ->
+    user_err_loc (Loc.ghost,"add_notation_extra_printing_rule",
+      str "No such Notation.")
 
 (**********************************************************************)
 (* Synchronisation with reset *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 95e176064c..961e1e12ea 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -185,8 +185,12 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
 
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing_rule = unparsing list * precedence
-val declare_notation_printing_rule : notation -> unparsing_rule -> unit
+type extra_unparsing_rules = (string * string) list
+val declare_notation_printing_rule :
+  notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val add_notation_extra_printing_rule : notation -> string -> string -> unit
 
 (** Rem: printing rules for primitive token are canonical *)