BIG BUG FIXED (???): in place of using Grammar.Entry.parse we should have

[helm.git] / matita / matita / matitaEngine.ml

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 1efaeff24834ce7b09cdbd3f1eb619d0ece0a270..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
@@ -288,7 +292,7 @@ and compile ~compiling ~include_paths fname =
 (* BIG BUG: if a file recursively includes itself, anything can happen,
  * from divergence to inclusion of an old copy of itself *)
 and assert_ng ~compiling ~include_paths ~root mapath =
- let root',baseuri,_,_ = Librarian.baseuri_of_script ~include_paths mapath in
+ let root',baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
  assert (root=root');
  let baseuri = NUri.uri_of_string baseuri in
  let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
@@ -297,8 +301,8 @@ and assert_ng ~compiling ~include_paths ~root mapath =
    Some (Unix.stat ngpath).Unix.st_mtime
   with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
  let matime =
-  try (Unix.stat mapath).Unix.st_mtime
-  with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = mapath -> assert false
+  try (Unix.stat fullmapath).Unix.st_mtime
+  with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
  in
  let to_be_compiled =
   match ngtime with
@@ -317,7 +321,7 @@ and assert_ng ~compiling ~include_paths ~root mapath =
      (* maybe recompiling it I would get the same... *)
      raise (AlreadyLoaded (lazy mapath))
    else
-    (compile ~compiling ~include_paths mapath; true)
+    (compile ~compiling ~include_paths fullmapath; true)
 ;;
 
 let assert_ng = assert_ng ~compiling:[]