diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 21 | ||||
| -rw-r--r-- | interp/notation.mli | 6 |
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 *) |