src/Pure/Thy/thy_info.ML
Tue, 05 Jul 2011 22:39:15 +0200 wenzelm Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
Mon, 04 Jul 2011 16:27:11 +0200 wenzelm some support for theory files within Isabelle/Scala session;
Sat, 02 Jul 2011 19:22:06 +0200 wenzelm uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;
Sat, 02 Jul 2011 19:08:51 +0200 wenzelm misc tuning;
Sat, 26 Mar 2011 21:45:29 +0100 wenzelm present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
Sun, 20 Mar 2011 17:40:45 +0100 wenzelm replaced File.check by specific File.check_file, File.check_dir;
Sun, 13 Mar 2011 20:56:00 +0100 wenzelm files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
Tue, 01 Feb 2011 19:39:26 +0100 wenzelm simplified trace;
Mon, 31 Jan 2011 23:02:53 +0100 wenzelm tuned signature;
Mon, 31 Jan 2011 22:57:01 +0100 wenzelm support named tasks, for improved tracing;
Mon, 31 Jan 2011 21:54:49 +0100 wenzelm more direct Future.bulk, which potentially reduces overhead for Par_List;
Fri, 14 Jan 2011 13:58:07 +0100 wenzelm Thy_Load.begin_theory: maintain source specification of imports;
Thu, 13 Jan 2011 17:34:45 +0100 wenzelm Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
Sat, 27 Nov 2010 14:19:04 +0100 wenzelm moved file identification to thy_load.ML (where it is actually used);
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Wed, 01 Sep 2010 15:51:49 +0200 haftmann Graph.map, in analogy to Table.map
Wed, 04 Aug 2010 16:28:45 +0200 wenzelm uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
Wed, 04 Aug 2010 16:11:51 +0200 wenzelm load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;
Wed, 04 Aug 2010 15:50:55 +0200 wenzelm export use_thys_wrt;
Wed, 04 Aug 2010 15:45:49 +0200 wenzelm more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
Wed, 04 Aug 2010 14:46:17 +0200 wenzelm schedule_futures: discontinued special treatment of non-parallel proofs, which might have affected memory usage at some point, but does not seem to make a difference with as little as 2GB RAM;
Tue, 03 Aug 2010 22:28:43 +0200 wenzelm more precise CRITICAL sections;
Tue, 03 Aug 2010 21:34:38 +0200 wenzelm removed unused Update_Time data (cf. ac94ff28e9e1);
Tue, 03 Aug 2010 18:13:57 +0200 wenzelm eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;
Tue, 03 Aug 2010 16:21:33 +0200 wenzelm load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;
Tue, 27 Jul 2010 23:25:50 +0200 wenzelm simplified handling of update_time -- do not store within deps;
Tue, 27 Jul 2010 23:15:37 +0200 wenzelm clarified register_thy: clean slate via kill_thy, more precise CRITICAL section;
Tue, 27 Jul 2010 23:01:42 +0200 wenzelm theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
Tue, 27 Jul 2010 22:42:53 +0200 wenzelm avoid repeated File.read for theory text (as before);
Tue, 27 Jul 2010 22:23:32 +0200 wenzelm tuned messages and comments;
Tue, 27 Jul 2010 22:15:51 +0200 wenzelm simplified Thy_Header.read -- include Source.of_string_limited here;
Tue, 27 Jul 2010 22:00:26 +0200 wenzelm simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
Mon, 26 Jul 2010 13:50:52 +0200 wenzelm Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;
Sun, 25 Jul 2010 21:42:39 +0200 wenzelm simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
Sun, 25 Jul 2010 14:41:48 +0200 wenzelm simplified handling of theory begin/end wrt. toplevel and theory loader;
Sat, 24 Jul 2010 12:14:53 +0200 wenzelm moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
Thu, 22 Jul 2010 22:58:18 +0200 wenzelm eliminated some unused Thy_Info operations;
Thu, 22 Jul 2010 22:31:20 +0200 wenzelm discontinued special treatment of ML files -- no longer complete extensions on demand;
Thu, 22 Jul 2010 14:01:43 +0200 wenzelm tuned;
Wed, 21 Jul 2010 20:32:08 +0200 wenzelm deps_thy/load_thy: store compact text to reduce space by factor 12;
Wed, 21 Jul 2010 16:14:16 +0200 wenzelm eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
Wed, 21 Jul 2010 15:31:38 +0200 wenzelm replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Sat, 15 May 2010 23:40:00 +0200 wenzelm renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
Tue, 05 Jan 2010 00:04:29 +0100 wenzelm kill failed theories in reverse order -- avoids cascaded warnings;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Thu, 01 Oct 2009 16:27:13 +0200 wenzelm added Task_Queue.depend (again) -- light-weight version for transitive graph;
Wed, 30 Sep 2009 23:28:54 +0200 wenzelm eliminated redundant bindings;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Tue, 21 Jul 2009 20:37:32 +0200 wenzelm maintain Future.worker_group as management data;
Sun, 19 Jul 2009 19:24:04 +0200 wenzelm parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
Wed, 10 Jun 2009 11:12:06 +0200 wenzelm reraise exceptions to preserve position information;
Tue, 31 Mar 2009 12:59:16 +0200 wenzelm schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;
Fri, 06 Mar 2009 22:47:32 +0100 wenzelm schedule_seq: handle after_load errors as in schedule_futures;
Sat, 10 Jan 2009 23:56:11 +0100 wenzelm schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
Sat, 10 Jan 2009 16:58:56 +0100 wenzelm remove_thy: perform PureThy.cancel_proofs;
Sat, 10 Jan 2009 13:11:56 +0100 wenzelm schedule_futures: tuned final consolidation, explicit after_load phase;
Sat, 10 Jan 2009 00:25:31 +0100 wenzelm use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
Tue, 16 Dec 2008 12:13:53 +0100 wenzelm removed old scheduler;
less more (0) -100 -60 tip