| Thu, 30 Aug 2012 19:18:49 +0200 |
wenzelm |
some support for registering forked proofs within Proof.state, using its bottom context;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 16:39:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 22:10:27 +0200 |
wenzelm |
more accurate defining position of theory;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 12:33:42 +0200 |
wenzelm |
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 21:28:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 21:02:02 +0200 |
wenzelm |
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 21:48:32 +0200 |
wenzelm |
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 20:32:33 +0200 |
wenzelm |
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 17:08:22 +0200 |
wenzelm |
prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 19:53:20 +0200 |
wenzelm |
more standard bootstrapping of Pure.thy;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 13:05:30 +0100 |
wenzelm |
define keywords early when processing the theory header, before running the body commands;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 00:10:45 +0100 |
wenzelm |
some support for outer syntax keyword declarations within theory header;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 18:18:39 +0100 |
wenzelm |
clarified terminology of raw protocol messages;
|
file |
diff |
annotate
|
| Sat, 25 Feb 2012 12:34:56 +0100 |
wenzelm |
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 14:34:18 +0100 |
wenzelm |
prefer raw_message for protocol implementation;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| 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
|
| Wed, 04 Aug 2010 15:45:49 +0200 |
wenzelm |
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 03 Aug 2010 22:28:43 +0200 |
wenzelm |
more precise CRITICAL sections;
|
file |
diff |
annotate
|
| Tue, 03 Aug 2010 21:34:38 +0200 |
wenzelm |
removed unused Update_Time data (cf. ac94ff28e9e1);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 23:25:50 +0200 |
wenzelm |
simplified handling of update_time -- do not store within deps;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 23:15:37 +0200 |
wenzelm |
clarified register_thy: clean slate via kill_thy, more precise CRITICAL section;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 23:01:42 +0200 |
wenzelm |
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 22:42:53 +0200 |
wenzelm |
avoid repeated File.read for theory text (as before);
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 22:23:32 +0200 |
wenzelm |
tuned messages and comments;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 22:15:51 +0200 |
wenzelm |
simplified Thy_Header.read -- include Source.of_string_limited here;
|
file |
diff |
annotate
|