| 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
|
| Mon, 24 Sep 2007 21:07:41 +0200 |
wenzelm |
added @{theory_ref};
|
file |
diff |
annotate
|
| Sat, 08 Sep 2007 19:58:39 +0200 |
wenzelm |
export is_finished;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 23:10:46 +0200 |
wenzelm |
removed obsolete touch_all_thys;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 17:49:33 +0200 |
wenzelm |
check_deps: ensure that theory is actually present, not just update_time > 1;
|
file |
diff |
annotate
|
| Sun, 12 Aug 2007 14:14:24 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2007 17:50:23 +0200 |
wenzelm |
schedule_tasks: alphabetical order for equivalent tasks;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 23:53:51 +0200 |
wenzelm |
schedule: misc cleanup, more precise task model;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 23:07:50 +0200 |
wenzelm |
discontinued attached ML files;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 20:48:08 +0200 |
wenzelm |
check_deps: really do reload the master text if required;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 20:19:51 +0200 |
wenzelm |
theory loader: removed obsolete update_thy (coincides with use_thy);
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 22:33:10 +0200 |
wenzelm |
replaced outdated flag by update_time (multithreading-safe presentation order);
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 21:45:07 +0200 |
wenzelm |
added int type constraints to accomodate hacked SML/NJ;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 19:40:28 +0200 |
wenzelm |
register_thy: more sanity checks;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:34 +0200 |
wenzelm |
added register_thy (replaces pretend_use_thy_only and really flag);
|
file |
diff |
annotate
|
| Mon, 30 Jul 2007 11:12:28 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 22:42:02 +0200 |
wenzelm |
deps: keep thy source text, avoid reloading;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 16:00:06 +0200 |
wenzelm |
removed obsolete Output.ML_errors/toplevel_errors;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 17:05:50 +0200 |
wenzelm |
require_thy/schedule: improved task graph, actually observe dependencies on running tasks;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 22:53:49 +0200 |
wenzelm |
require_thy: tuned tasks graph, removed visited;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 19:44:39 +0200 |
wenzelm |
require_thy: explicit tasks graph;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 19:45:46 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 21:20:55 +0200 |
wenzelm |
added simultaneous use_thys;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 13:53:52 +0200 |
wenzelm |
begin_theory: simplified interface, keep thy info empty until end_theory;
|
file |
diff |
annotate
|
| Sat, 21 Jul 2007 17:40:40 +0200 |
wenzelm |
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 17:54:17 +0200 |
wenzelm |
simplified ThyLoad interfaces: only one additional directory;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 23:18:58 +0200 |
wenzelm |
removed obsolete use/update_thy_only;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2007 13:16:58 +0100 |
aspinall |
Add get_succs
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:46:40 +0100 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:43:47 +0100 |
wenzelm |
tuned comments
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:22 +0100 |
wenzelm |
added @{theory};
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 13:09:33 +0100 |
wenzelm |
adapted ML context operations;
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Tue, 02 May 2006 20:42:43 +0200 |
wenzelm |
added the_theory;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:15 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:26 +0100 |
wenzelm |
use/use_thy: Output.toplevel_errors;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:50 +0200 |
wenzelm |
begin_theory: tuned interface, check uses;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 09:37:12 +0200 |
haftmann |
introduced AList.*
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:19 +0200 |
wenzelm |
Theory.begin/end_theory;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:39 +0200 |
wenzelm |
removed obsolete theory_of_sign, theory_of_thm;
|
file |
diff |
annotate
|
| Mon, 23 May 2005 14:56:37 +0200 |
wenzelm |
tuned pretty_sg;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2005 18:20:29 +0100 |
paulson |
new display of theory stamps
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 23 Aug 2004 18:33:55 +0200 |
berghofe |
Fixed several bugs related to path specifications in theory names.
|
file |
diff |
annotate
|
| Mon, 19 Jul 2004 18:21:26 +0200 |
berghofe |
Some changes to allow qualified theory import.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:01:36 +0200 |
wenzelm |
Output.timing;
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:18:48 +0200 |
wenzelm |
Graph.minimals;
|
file |
diff |
annotate
|
| Sun, 17 Sep 2000 22:22:11 +0200 |
wenzelm |
begin_theory: removed message;
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 22:32:15 +0200 |
wenzelm |
begin_theory: priority message to gain some robustness in sync communication;
|
file |
diff |
annotate
|
| Sun, 03 Sep 2000 20:04:43 +0200 |
wenzelm |
added pretend_use_thy_only;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2000 00:34:07 +0200 |
wenzelm |
replaced writeln by priority;
|
file |
diff |
annotate
|
| Tue, 01 Aug 2000 13:43:22 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2000 18:25:01 +0200 |
wenzelm |
begin_theory: store *copy* of initial theory;
|
file |
diff |
annotate
|
| Sun, 23 Jul 2000 12:10:41 +0200 |
wenzelm |
get_names: topologically sorted;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 23:26:08 +0200 |
wenzelm |
tuned cycle_msg;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 23:20:14 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 25 Jun 2000 23:56:16 +0200 |
wenzelm |
use Library.change;
|
file |
diff |
annotate
|
| Sun, 04 Jun 2000 21:54:58 +0200 |
wenzelm |
do not setmp Library.timing;
|
file |
diff |
annotate
|
| Tue, 30 May 2000 16:03:09 +0200 |
wenzelm |
global timing flag;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:00:17 +0200 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Wed, 27 Oct 1999 17:25:36 +0200 |
wenzelm |
quiet_update_thy: ml flag;
|
file |
diff |
annotate
|
| Tue, 26 Oct 1999 22:37:34 +0200 |
wenzelm |
improved ml handling;
|
file |
diff |
annotate
|
| Tue, 26 Oct 1999 19:04:55 +0200 |
wenzelm |
added check_known_thy, if_known_thy;
|
file |
diff |
annotate
|
| Thu, 21 Oct 1999 19:00:01 +0200 |
wenzelm |
added known_thy;
|
file |
diff |
annotate
|
| Wed, 20 Oct 1999 15:50:51 +0200 |
wenzelm |
remove_thy: warn unknown theory (rather than error);
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 12:22:14 +0200 |
wenzelm |
fixed lookup_theory;
|
file |
diff |
annotate
|
| Thu, 23 Sep 1999 18:42:28 +0200 |
wenzelm |
improved cycle error;
|
file |
diff |
annotate
|
| Thu, 19 Aug 1999 16:33:36 +0200 |
wenzelm |
lookup_theory;
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 20:42:09 +0200 |
wenzelm |
deps: include 'really' flag;
|
file |
diff |
annotate
|
| Tue, 17 Aug 1999 22:22:36 +0200 |
wenzelm |
may_load_file;
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 22:04:07 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 16:44:24 +0200 |
wenzelm |
fixed thy_only;
|
file |
diff |
annotate
|
| Fri, 06 Aug 1999 22:32:27 +0200 |
wenzelm |
added pretend_use;
|
file |
diff |
annotate
|
| Tue, 27 Jul 1999 21:55:19 +0200 |
wenzelm |
added update_thy_only;
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 16:50:20 +0200 |
wenzelm |
require_thy: fixed performance leak;
|
file |
diff |
annotate
|
| Tue, 06 Jul 1999 21:03:34 +0200 |
wenzelm |
begin_theory: disallow finished;
|
file |
diff |
annotate
|
| Mon, 17 May 1999 21:36:11 +0200 |
wenzelm |
cleaned comments;
|
file |
diff |
annotate
|
| Mon, 17 May 1999 17:07:54 +0200 |
berghofe |
Added function get_preds.
|
file |
diff |
annotate
|
| Tue, 27 Apr 1999 15:12:34 +0200 |
wenzelm |
use_thy_only made pervasive;
|
file |
diff |
annotate
|
| Thu, 22 Apr 1999 18:18:47 +0200 |
wenzelm |
improved auto dir handling;
|
file |
diff |
annotate
|
| Thu, 22 Apr 1999 13:28:11 +0200 |
wenzelm |
use_thy etc.: may specify path prefix, which is temporarily used as load path;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:32:38 +0100 |
wenzelm |
fixed msg;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 13:41:50 +0100 |
wenzelm |
tuned msgs;
|
file |
diff |
annotate
|
| Fri, 12 Mar 1999 18:48:51 +0100 |
wenzelm |
removed obsolete user data stuff;
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 12:18:46 +0100 |
wenzelm |
added use_path;
|
file |
diff |
annotate
|
| Mon, 08 Feb 1999 17:32:24 +0100 |
wenzelm |
tuned msgs;
|
file |
diff |
annotate
|
| Fri, 05 Feb 1999 21:01:53 +0100 |
wenzelm |
time_use made pervasive;
|
file |
diff |
annotate
|
| Thu, 04 Feb 1999 18:18:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 20:25:53 +0100 |
wenzelm |
check_thy: include ML stamp;
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 17:29:48 +0100 |
wenzelm |
Theory loader database: theory and file dependencies, theory values
|
file |
diff |
annotate
|
| Wed, 29 Jul 1998 15:38:08 +0200 |
wenzelm |
late setup of Pure and CPure;
|
file |
diff |
annotate
|
| Tue, 28 Jul 1998 17:03:12 +0200 |
wenzelm |
theory_of renamed to theory (and made public);
|
file |
diff |
annotate
|
| Thu, 28 May 1998 11:09:07 +0200 |
wenzelm |
tuned error msg;
|
file |
diff |
annotate
|
| Mon, 25 May 1998 21:25:04 +0200 |
wenzelm |
tuned store_theory: theory -> unit;
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 12:03:48 +0100 |
wenzelm |
removed old thy data stuff;
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:18:25 +0200 |
wenzelm |
ProtoPure.thy etc.;
|
file |
diff |
annotate
|