diff options
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index b19fd9e1f..7ad104d03 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -967,23 +967,27 @@ let pr_visibility prglob = function 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 * extra_unparsing_rules) String.Map.t) +let notation_rules = + ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) -let declare_notation_printing_rule ntn ~extra unpl = - printing_rules := String.Map.add ntn (unpl,extra) !printing_rules +let declare_notation_rule ntn ~extra unpl gram = + notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules let find_notation_printing_rule ntn = - try fst (String.Map.find ntn !printing_rules) + try pi1 (String.Map.find ntn !notation_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) + try pi2 (String.Map.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) + 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 + notation_rules := + let p, pp, gr = String.Map.find ntn !notation_rules in + String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules with Not_found -> user_err_loc (Loc.ghost,"add_notation_extra_printing_rule", str "No such Notation.") @@ -993,7 +997,7 @@ let add_notation_extra_printing_rule ntn k v = let freeze _ = (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, - !delimiters_map, !notations_key_table, !printing_rules, + !delimiters_map, !notations_key_table, !notation_rules, !scope_class_map) let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = @@ -1003,7 +1007,7 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; - printing_rules := pprules; + notation_rules := pprules; scope_class_map := clsc let init () = @@ -1011,7 +1015,7 @@ let init () = notation_level_map := String.Map.empty; delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - printing_rules := String.Map.empty; + notation_rules := String.Map.empty; scope_class_map := initial_scope_class_map let _ = |