| 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
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 25 Jul 2010 21:42:39 +0200 |
wenzelm |
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
|
file |
diff |
annotate
|
| Sun, 25 Jul 2010 14:41:48 +0200 |
wenzelm |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 22:58:18 +0200 |
wenzelm |
eliminated some unused Thy_Info operations;
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 22:31:20 +0200 |
wenzelm |
discontinued special treatment of ML files -- no longer complete extensions on demand;
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 14:01:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 20:32:08 +0200 |
wenzelm |
deps_thy/load_thy: store compact text to reduce space by factor 12;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 16:14:16 +0200 |
wenzelm |
eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
| Tue, 05 Jan 2010 00:04:29 +0100 |
wenzelm |
kill failed theories in reverse order -- avoids cascaded warnings;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 16:27:13 +0200 |
wenzelm |
added Task_Queue.depend (again) -- light-weight version for transitive graph;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 23:28:54 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 20:37:32 +0200 |
wenzelm |
maintain Future.worker_group as management data;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2009 19:24:04 +0200 |
wenzelm |
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 11:12:06 +0200 |
wenzelm |
reraise exceptions to preserve position information;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 12:59:16 +0200 |
wenzelm |
schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 22:47:32 +0100 |
wenzelm |
schedule_seq: handle after_load errors as in schedule_futures;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 16:58:56 +0100 |
wenzelm |
remove_thy: perform PureThy.cancel_proofs;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 13:11:56 +0100 |
wenzelm |
schedule_futures: tuned final consolidation, explicit after_load phase;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 12:13:53 +0100 |
wenzelm |
removed old scheduler;
|
file |
diff |
annotate
|
| Fri, 12 Dec 2008 12:14:02 +0100 |
wenzelm |
future proofs: more robust check via Future.enabled;
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 00:04:44 +0100 |
wenzelm |
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:46:20 +0100 |
wenzelm |
refined Future.fork interfaces, no longer export Future.future;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:02:46 +0100 |
wenzelm |
future_scheduler: no global task group, exceptions via collective join;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 18:25:59 +0100 |
wenzelm |
force_proofs after cumulative use_thys;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 00:11:06 +0100 |
wenzelm |
finish: force proofs;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2008 20:21:35 +0200 |
wenzelm |
Future.joint_results is already uninterruptible;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 18:16:10 +0200 |
wenzelm |
future_schedule: back to one group for all loader tasks;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:00:05 +0200 |
wenzelm |
more robust treatment of Interrupt (cf. exn.ML);
|
file |
diff |
annotate
|
| Tue, 30 Sep 2008 22:02:55 +0200 |
wenzelm |
schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 20:34:21 +0200 |
wenzelm |
moved future_scheduler flag to skip_proof.ML;
|
file |
diff |
annotate
|
| Fri, 19 Sep 2008 21:22:31 +0200 |
wenzelm |
future tasks: support boolean priorities (true = high, false = low/irrelevant);
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:49 +0200 |
wenzelm |
begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};
|
file |
diff |
annotate
|
| Wed, 10 Sep 2008 22:29:36 +0200 |
wenzelm |
future_schedule: uninterruptible join;
|
file |
diff |
annotate
|
| Wed, 10 Sep 2008 21:50:32 +0200 |
wenzelm |
added future_scheduler (default false);
|
file |
diff |
annotate
|
| Thu, 04 Sep 2008 16:03:49 +0200 |
wenzelm |
moved Multithreading.task/schedule to Concurrent/schedule.ML
|
file |
diff |
annotate
|
| Tue, 12 Aug 2008 21:28:05 +0200 |
wenzelm |
load_thy: removed obsolete dir argument;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 17:51:48 +0200 |
wenzelm |
end_theory: no result;
|
file |
diff |
annotate
|
| Tue, 08 Jul 2008 17:52:28 +0200 |
wenzelm |
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:21 +0200 |
wenzelm |
moved concrete antiquotations to ml_antiquote.ML;
|
file |
diff |
annotate
|
| Sat, 24 May 2008 20:12:17 +0200 |
wenzelm |
exported master_directory;
|
file |
diff |
annotate
|
| Wed, 14 May 2008 11:05:08 +0200 |
wenzelm |
renamed Position.path to Path.position;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2008 14:53:30 +0200 |
wenzelm |
export get_names (formerly names);
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:16 +0100 |
wenzelm |
added exec_file;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 00:02:54 +0100 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:10 +0100 |
wenzelm |
renamed ML_Context.the_context to ML_Context.the_global_context;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:07 +0100 |
wenzelm |
adapted to Context.thread_data interface;
|
file |
diff |
annotate
|
| Sun, 27 Jan 2008 22:21:37 +0100 |
wenzelm |
use_thy: do not set implicit ML context anymore;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 16:32:53 +0100 |
wenzelm |
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 21:12:03 +0100 |
wenzelm |
scheduling/next_task: PrintMode.closure;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2007 16:13:46 +0200 |
wenzelm |
require_thy: read_text *after* checking parents
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 21:37:00 +0200 |
wenzelm |
added generic provide_file;
|
file |
diff |
annotate
|