From 5e924927db28c0a5bbbaa4e56515d9afe0b1360f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 10 Dec 2010 22:30:55 +0000 Subject: [PATCH] BIG BUG FIXED (???): in place of using Grammar.Entry.parse we should have used from the beginning Grammar.Entry.parse_parsable in order to avoid token loss (because of backtracking) between consecutive reads. I have fixed the issue for statements only (since they are the one that show the problem). Should I do the same everywhere? --- matita/components/grafite_parser/grafiteParser.ml | 4 ++-- matita/components/grafite_parser/grafiteParser.mli | 2 +- matita/matita/matitaEngine.ml | 6 +++++- matita/matita/matitaEngine.mli | 2 +- matita/matita/matitaScript.ml | 11 +++++++---- 5 files changed, 16 insertions(+), 9 deletions(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index dd4075a8a..8c2cbf909 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -42,9 +42,9 @@ let exc_located_wrapper f = raise (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn))) -let parse_statement grafite_parser lexbuf = +let parse_statement grafite_parser parsable = exc_located_wrapper - (fun () -> (Grammar.Entry.parse (Obj.magic grafite_parser) (Obj.magic lexbuf))) + (fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) parsable)) let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t) diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli index 2b458fdf8..ea4d43a62 100644 --- a/matita/components/grafite_parser/grafiteParser.mli +++ b/matita/components/grafite_parser/grafiteParser.mli @@ -47,4 +47,4 @@ val extend : #status as 'status -> (* never_include: do not call LexiconEngine to do includes, * always raise NoInclusionPerformed *) (** @raise End_of_file *) -val parse_statement: #status -> Ulexing.lexbuf -> GrafiteAst.statement +val parse_statement: #status -> Grammar.parsable -> GrafiteAst.statement diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index cd5c83441..4429f9636 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -249,7 +249,11 @@ and compile ~compiling ~include_paths fname = (Filename.dirname (Http_getter.filename ~local:true ~writable:true (baseuri ^ "foo.con"))); - let buf = Ulexing.from_utf8_channel (open_in fname) in + let grammar = CicNotationParser.level2_ast_grammar grafite_status in + let buf = + Grammar.parsable grammar + (Obj.magic (Ulexing.from_utf8_channel (open_in fname))) + in let print_cb = if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ()) else pp_ast_statement diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli index 768ff7080..856805db8 100644 --- a/matita/matita/matitaEngine.mli +++ b/matita/matita/matitaEngine.mli @@ -30,7 +30,7 @@ exception FailureCompiling of string * exn exception CircularDependency of string val get_ast: - GrafiteTypes.status -> include_paths:string list -> Ulexing.lexbuf -> + GrafiteTypes.status -> include_paths:string list -> Grammar.parsable -> GrafiteAst.statement (* heavy checks slow down the compilation process but give you some interesting diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 22eee2f00..3a73d6ce6 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -193,7 +193,9 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - let strm = Ulexing.from_utf8_string text in + let grammar = CicNotationParser.level2_ast_grammar grafite_status in + let strm = + Grammar.parsable grammar (Obj.magic(Ulexing.from_utf8_string text)) in let ast = MatitaEngine.get_ast grafite_status include_paths strm in ast, text | `Ast (st, text) -> st, text @@ -663,9 +665,10 @@ object (self) method eos = let rec is_there_only_comments lexicon_status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - match - GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s) - with + let grammar = CicNotationParser.level2_ast_grammar lexicon_status in + let strm = + Grammar.parsable grammar (Obj.magic(Ulexing.from_utf8_string s)) in + match GrafiteParser.parse_statement lexicon_status strm with | GrafiteAst.Comment (loc,_) -> let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in (* CSC: why +1 in the following lines ???? *) -- 2.39.2