From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 30 May 2006 10:22:57 +0000 (+0000)
Subject: ZACK: export a top level function for parsing terms, it can't be bypassed due to... 
X-Git-Tag: 0.4.95@7852~1383
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a408b8e26e4ea85755847f74bf9ca6998c2b47b0;p=helm.git

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

diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml
index 5750ad816..02c959ef7 100644
--- 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 e25968bbb..978daf9ff 100644
--- 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 *)