diff options
| author | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
| commit | dd84c113a154742dff86328ebc758097e9aac8eb (patch) | |
| tree | 67795fb720516f564d074d55d9e2aa90e3d4e7f2 /parsing/ppextend.ml | |
| parent | 231f679965745a4d7677166e8d5f62a38ebde4e7 (diff) | |
| parent | 569ad299a8092778611fcc8ae2842151c4b276db (diff) | |
Merge PR #8115: Support for custom entries in notations (take 2, feature part)
Diffstat (limited to 'parsing/ppextend.ml')
| -rw-r--r-- | parsing/ppextend.ml | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index d2b50fa83d..e1f5e20117 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -11,6 +11,7 @@ open Util open Pp open CErrors +open Notation open Notation_gram (*s Pretty-print. *) @@ -48,29 +49,29 @@ type unparsing_rule = unparsing list * precedence type extra_unparsing_rules = (string * string) list (* Concrete syntax for symbolic-extension table *) let notation_rules = - Summary.ref ~name:"notation-rules" (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) + Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t) let declare_notation_rule ntn ~extra unpl gram = - notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules + notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules let find_notation_printing_rule ntn = - try pi1 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") + try pi1 (NotationMap.find ntn !notation_rules) + with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".") let find_notation_extra_printing_rules ntn = - try pi2 (String.Map.find ntn !notation_rules) + try pi2 (NotationMap.find ntn !notation_rules) with Not_found -> [] let find_notation_parsing_rules ntn = - try pi3 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") + try pi3 (NotationMap.find ntn !notation_rules) + with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".") let get_defined_notations () = - String.Set.elements @@ String.Map.domain !notation_rules + NotationSet.elements @@ NotationMap.domain !notation_rules let add_notation_extra_printing_rule ntn k v = try notation_rules := - let p, pp, gr = String.Map.find ntn !notation_rules in - String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules + let p, pp, gr = NotationMap.find ntn !notation_rules in + NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules with Not_found -> user_err ~hdr:"add_notation_extra_printing_rule" (str "No such Notation.") |