From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 11 Oct 2011 10:43:54 +0000 (+0000)
Subject: WARNING: major experimental change.
X-Git-Tag: make_still_working~2221
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d72aaf7d3c12ecc70208a896e08b120b5031a7cb;p=helm.git

WARNING: major experimental change.

"include" is no longer turned into an "include alias"
when the file to be included is already loaded. This
greatly speeds up inclusion, at the price of having
to manually add some "include alias" here and there.
---

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index 826779401..a7129177e 100644
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -283,32 +283,31 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
    let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_
    ~refresh_uri_in_reference:_ ~alias_only status =
      let baseuri = refresh_uri baseuri in
-     let alias_only =
-      alias_only || List.mem baseuri (get_transitively_included (D.get status))
-     in
-      (*HLog.warn ("include " ^ (if alias_only then "alias " else "") ^ fname);*)
+     if not alias_only && List.mem baseuri (get_transitively_included (D.get status)) then status
+     else
+      (HLog.warn ("include " ^ (if alias_only then "alias " else "") ^ fname);
       let status = require2 ~baseuri ~alias_only status in
-      (*HLog.warn ("done: include " ^ (if alias_only then "alias " else "") ^ fname);*)
-      status
+      HLog.warn ("done: include " ^ (if alias_only then "alias " else "") ^ fname);
+      status)
    in
     register#run "include" aux
 
   let require ~baseuri ~fname ~alias_only status =
-   let alias_only =
-    alias_only || List.mem baseuri (get_transitively_included (D.get status)) in
-   let status =
-    if not alias_only then
-     let s = D.get status in
-      D.set status
-       (s#set_dump {s#dump with dependencies = fname::s#dump.dependencies})
-    else
-     status in
-   let status = require2 ~baseuri ~alias_only status in
-   let s = D.get status in
-    D.set status
-     (s#set_dump
-       {s#dump with
-         objs = record_include (baseuri,fname)::s#dump.objs })
+   if not alias_only && List.mem baseuri (get_transitively_included (D.get status)) then status
+   else
+    (let status =
+     if not alias_only then
+      let s = D.get status in
+       D.set status
+        (s#set_dump {s#dump with dependencies = fname::s#dump.dependencies})
+     else
+      status in
+    let status = require2 ~baseuri ~alias_only status in
+    let s = D.get status in
+     D.set status
+      (s#set_dump
+        {s#dump with
+          objs = record_include (baseuri,fname)::s#dump.objs }))
 end
 
 let fetch_obj status uri =