| Sat, 20 Aug 2011 22:46:19 +0200 |
wenzelm |
clarified get_imports -- should not rely on accidental order within graph;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:01:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 22:14:22 +0200 |
wenzelm |
more systematic handling of parallel exceptions;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 22:48:31 +0200 |
wenzelm |
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 21:13:52 +0200 |
wenzelm |
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 20:19:41 +0200 |
wenzelm |
retrieve imports from document state, with fall-back on theory loader for preloaded theories;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:41:29 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special master argument;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2011 20:32:25 +0200 |
wenzelm |
general Graph.schedule;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:05:14 +0200 |
wenzelm |
future_job: explicit indication of interrupts;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 21:44:47 +0200 |
wenzelm |
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 22:39:15 +0200 |
wenzelm |
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 16:27:11 +0200 |
wenzelm |
some support for theory files within Isabelle/Scala session;
|
file |
diff |
annotate
|
| Sat, 02 Jul 2011 19:22:06 +0200 |
wenzelm |
uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;
|
file |
diff |
annotate
|
| Sat, 02 Jul 2011 19:08:51 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 17:40:45 +0100 |
wenzelm |
replaced File.check by specific File.check_file, File.check_dir;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 20:56:00 +0100 |
wenzelm |
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
|
file |
diff |
annotate
|
| Tue, 01 Feb 2011 19:39:26 +0100 |
wenzelm |
simplified trace;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 23:02:53 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 22:57:01 +0100 |
wenzelm |
support named tasks, for improved tracing;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 21:54:49 +0100 |
wenzelm |
more direct Future.bulk, which potentially reduces overhead for Par_List;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 13:58:07 +0100 |
wenzelm |
Thy_Load.begin_theory: maintain source specification of imports;
|
file |
diff |
annotate
|
| Thu, 13 Jan 2011 17:34:45 +0100 |
wenzelm |
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 14:19:04 +0100 |
wenzelm |
moved file identification to thy_load.ML (where it is actually used);
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:51:49 +0200 |
haftmann |
Graph.map, in analogy to Table.map
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 04 Aug 2010 15:50:55 +0200 |
wenzelm |
export use_thys_wrt;
|
file |
diff |
annotate
|