snapshot

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.mli

diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli
index 5112f6dbd89dcbd1d129052508bf00b4e2511a0d..1dd81ef9fa4a19298c74ae37c013fc49f1af5e75 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.mli
+++ b/helm/ocaml/cic_notation/cicNotationParser.mli
@@ -24,6 +24,7 @@
  *)
 
 exception Parse_error of Token.flocation * string
+exception Level_not_found of int
 
 (** {2 Parsing functions} *)
 
@@ -36,3 +37,23 @@ val parse_ast_pattern:    char Stream.t -> CicNotationPt.term
   (** interpretation: notation level 3 *)
 val parse_interpretation: char Stream.t -> CicNotationPt.cic_appl_pattern
 
+(** {2 Grammar extension} *)
+
+type env_type = (string * (CicNotationPt.value_type * CicNotationPt.value)) list
+
+type rule_id
+
+val extend:
+  CicNotationPt.term ->
+  ?precedence:int ->
+  ?associativity:Gramext.g_assoc ->
+  (env_type -> CicNotationPt.location -> CicNotationPt.term) ->
+    rule_id
+
+val delete: rule_id -> unit
+
+(** {2 Debugging} *)
+
+  (** print "level2_pattern" entry on stdout, flushing afterwards *)
+val print_level2_pattern: unit -> unit
+