]> matita.cs.unibo.it Git - helm.git/commitdiff
ZACK: export a top level function for parsing terms, it can't be bypassed due to...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 30 May 2006 10:22:57 +0000 (10:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 30 May 2006 10:22:57 +0000 (10:22 +0000)
helm/software/components/content_pres/cicNotationParser.ml
helm/software/components/content_pres/cicNotationParser.mli

index 5750ad816805a841d64b61fcecdb5c7c826924db..02c959ef78abd300712faf1d2238aa654f1c9369 100644 (file)
@@ -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 () =
index e25968bbbc4aa03cec62cda83aed3558086430e4..978daf9ff99c1ce6f304663e86cb1c202f7c191a 100644 (file)
@@ -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 *)