From 8d55798c22b29c00febc623234db5f57483c0401 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 --- helm/software/components/content_pres/cicNotationParser.ml | 4 ++++ helm/software/components/content_pres/cicNotationParser.mli | 2 ++ 2 files changed, 6 insertions(+) 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 *) -- 2.39.2