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: make_still_working~7280
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8d55798c22b29c00febc623234db5f57483c0401;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/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 5750ad816..02c959ef7 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/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/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli
index e25968bbb..978daf9ff 100644
--- a/helm/software/components/content_pres/cicNotationParser.mli
+++ b/helm/software/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 *)