From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 27 Oct 2010 15:03:47 +0000 (+0000)
Subject: .moo no longer used: all interesting data is left in either .lexicon or
X-Git-Tag: make_still_working~2759
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=47a9eb47d4215450230840bc66570ce412d0ce79;p=helm.git

.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 22f14db13..1a87934a5 100644
--- 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 a6b9d7b1d..4c7371e09 100644
--- 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 8620f8cd4..1ed016e77 100644
--- 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