From a408b8e26e4ea85755847f74bf9ca6998c2b47b0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 30 May 2006 10:22:57 +0000 Subject: [PATCH] ZACK: export a top level function for parsing terms, it can't be bypassed due to the Obj.magic trick --- components/content_pres/cicNotationParser.ml | 4 ++++ components/content_pres/cicNotationParser.mli | 2 ++ 2 files changed, 6 insertions(+) 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 *) -- 2.39.2