From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Dec 2010 22:30:55 +0000 (+0000)
Subject: BIG BUG FIXED (???): in place of using Grammar.Entry.parse we should have
X-Git-Tag: make_still_working~2655
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5e924927db28c0a5bbbaa4e56515d9afe0b1360f;p=helm.git

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 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 ???? *)