From d72aaf7d3c12ecc70208a896e08b120b5031a7cb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 11 Oct 2011 10:43:54 +0000 Subject: [PATCH] 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. --- matita/components/ng_library/nCicLibrary.ml | 41 ++++++++++----------- 1 file changed, 20 insertions(+), 21 deletions(-) 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 = -- 2.39.2