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?

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index dd4075a8a5f70fb5b87ccdc364dac0c7f58ad1a1..8c2cbf9093554893d28cb6f9601854755e28aceb 100644 (file)
--- 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 2b458fdf80f7501a6833ba0c9d7c304db74d9533..ea4d43a621a676651929d2e5214712b75426ce66 100644 (file)
--- 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 cd5c8344198288c08dbfd1cd471686fc1c6fad42..4429f963651f7e8fa9839626fb8aa955b119d0ec 100644 (file)
--- 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 768ff7080ee323f50a5f8cdb977fe92579e9995e..856805db8a29851523b0fe1f16d76726d526f420 100644 (file)
--- 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 22eee2f00ebf0d3c00e601a2dc8e6d04b75cba7d..3a73d6ce6d2d38cbb2425e04c9ad670ea8f59112 100644 (file)
--- 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 ???? *)