ZACK: export a top level function for parsing terms, it can't be bypassed due to...

diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml
index 5750ad816805a841d64b61fcecdb5c7c826924db..02c959ef78abd300712faf1d2238aa654f1c9369 100644 (file)
--- a/components/content_pres/cicNotationParser.ml
+++ b/components/content_pres/cicNotationParser.ml
@@ -637,6 +637,10 @@ let _ =
   parse_level2_ast_ref := parse_level2_ast;
   parse_level2_meta_ref := parse_level2_meta
 
+let parse_term lexbuf =
+  exc_located_wrapper
+    (fun () -> (Grammar.Entry.parse term (Obj.magic lexbuf)))
+
 (** {2 Debugging} *)
 
 let print_l2_pattern () =

diff --git a/components/content_pres/cicNotationParser.mli b/components/content_pres/cicNotationParser.mli
index e25968bbbc4aa03cec62cda83aed3558086430e4..978daf9ff99c1ce6f304663e86cb1c202f7c191a 100644 (file)
--- a/components/content_pres/cicNotationParser.mli
+++ b/components/content_pres/cicNotationParser.mli
@@ -59,6 +59,8 @@ val let_defs :
   (CicNotationPt.capture_variable * CicNotationPt.term * int) list
     Grammar.Entry.e
 
+val parse_term: Ulexing.lexbuf -> CicNotationPt.term
+
 (** {2 Debugging} *)
 
   (** print "level2_pattern" entry on stdout, flushing afterwards *)