.moo no longer used: all interesting data is left in either .lexicon or

.ng

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 22f14db13aefed439158fd04be4c3695bc115fd9..1a87934a595cb4c1406d49b39ba81a844f4909f6 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -27,7 +27,7 @@
 
 exception Drop
 (* mo file name, ma file name *)
-exception IncludedFileNotCompiled of string * string 
+(*exception IncludedFileNotCompiled of string * string *)
 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 
 type 'a disambiguator_input = string * int * 'a
@@ -569,6 +569,7 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
  let status,uris =
   match cmd with
   | GrafiteAst.Include (loc, baseuri) ->
+      (*
      let status =
       let moopath_rw, moopath_r = 
        LibraryMisc.obj_file_of_baseuri 
@@ -582,14 +583,14 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
       in
        eval_from_moo status moopath
      in
-      let status =
+      let status = *)
        NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        status in
+        status (*in
       let status =
        GrafiteTypes.add_moo_content
         [GrafiteAst.Include (loc,baseuri)] status
       in
-       status,[]
+      status,[] *), []
   | GrafiteAst.Print (_,_) -> status,[]
   | GrafiteAst.Set (loc, name, value) -> status, []
  in

diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli
index a6b9d7b1da247823c3726f0180c0ad74dd68b79a..4c7371e097da855f5d555403d51fbce89b5795db 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.mli
+++ b/matita/components/grafite_engine/grafiteEngine.mli
@@ -24,7 +24,7 @@
  *)
 
 exception Drop
-exception IncludedFileNotCompiled of string * string
+(*exception IncludedFileNotCompiled of string * string*)
 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 
 type 'a disambiguator_input = string * int * 'a

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index 8620f8cd48eca5908359cd4af95ce3c3bec47c96..1ed016e771035df34cc37920d498e2df468dcaeb 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -12,6 +12,7 @@
 (* $Id$ *)
 
 exception LibraryOutOfSync of string Lazy.t
+exception IncludedFileNotCompiled of string * string 
 
 let magic = 2;;
 
@@ -67,7 +68,9 @@ let require_path path =
    dump
 ;;
 
-let require0 ~baseuri = require_path (path_of_baseuri baseuri);;
+let require0 ~baseuri =
+  require_path (path_of_baseuri baseuri)
+;;
 
 let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
 
@@ -275,10 +278,29 @@ module Serializer =
 
   let serialize = serialize
 
+  let require2 ~baseuri status =
+   try
+    includes := baseuri::!includes;
+    let dump = require0 ~baseuri in
+     List.fold_right !require1#run dump status
+   with
+    Sys_error _ ->
+     raise (IncludedFileNotCompiled(path_of_baseuri baseuri,NUri.string_of_uri baseuri))
+
+  let record_include =
+   let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term =
+     (* memorizzo baseuri in una tabella; *)
+     require2 ~baseuri
+   in
+    register#run "include"
+     object(self : 'a register_type)
+      method run = aux
+     end
+
   let require ~baseuri status =
-   includes := baseuri::!includes;
-   let dump = require0 ~baseuri in
-    List.fold_right !require1#run dump status
+   let status = require2 ~baseuri status in
+   let dump = record_include baseuri :: status#dump in
+    status#set_dump dump
 end