From 0f1b5603d1922718f36545f201212fc2796f41a4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 24 Sep 2016 20:36:59 +0200 Subject: [notation] Allow to retrieve defined notations. The ML side lacks a method to query Coq for notations with defined parsing/printing rules. This commit adds a method `get_defined_notations` to that purpose. This is very useful for instance in plugins like SerAPI. In the medium-term, the `Notation` interface may benefit from a bit of refactoring to allow programmatic access and manipulation of notations. --- interp/notation.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d..547c72e10 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1011,6 +1011,9 @@ 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 get_defined_notations () = + String.Set.elements @@ String.Map.domain !notation_rules + let add_notation_extra_printing_rule ntn k v = try notation_rules := -- cgit v1.2.3