| Wed, 17 Feb 2016 23:28:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 16:27:12 +0200 |
wenzelm |
explicit debug flag for ML compiler;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 16:03:45 +0100 |
wenzelm |
discontinued Isar TTY loop;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 15:19:22 +0200 |
wenzelm |
clarified ML bootstrap;
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 20:38:16 +0200 |
wenzelm |
tuned error message;
|
file |
diff |
annotate
|
| Sun, 15 May 2011 20:38:08 +0200 |
wenzelm |
timing of Theory_Data operations, with implicit thread positions when functor is applied;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 16:29:53 +0100 |
wenzelm |
removed bash from ML system bootstrap, and past the Secure ML barrier;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 14:14:08 +0200 |
wenzelm |
structure Unsynchronized is never opened and set/reset/toggle have been discontinued;
|
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
|
| Tue, 01 Jun 2010 13:32:05 +0200 |
wenzelm |
uniform ML environment setup for Isar and PG;
|
file |
diff |
annotate
|
| Sat, 06 Feb 2010 14:50:55 +0100 |
wenzelm |
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 14:59:24 +0200 |
wenzelm |
open_unsynchronized for interactive Isar loop;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 19:58:10 +0200 |
wenzelm |
use: tuned error;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 23:28:04 +0200 |
wenzelm |
export secure_mltext;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 21:40:11 +0100 |
wenzelm |
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 19:58:45 +0100 |
wenzelm |
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:24 +0200 |
wenzelm |
use_text/use_file now depend on explicit ML name space;
|
file |
diff |
annotate
|
| Wed, 14 May 2008 11:05:11 +0200 |
wenzelm |
use_text/file: proper position output;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2008 23:34:24 +0100 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 14:25:59 +0100 |
wenzelm |
system: writeln output, if available;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2008 20:17:50 +0100 |
wenzelm |
common setup for system_out/system;
|
file |
diff |
annotate
|
| Sat, 16 Feb 2008 16:43:57 +0100 |
wenzelm |
export deny_secure;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2008 16:09:27 +0100 |
wenzelm |
tuned spaces;
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 22:21:41 +0100 |
wenzelm |
removed obsolete use_noncritical (plain use is already non-critical);
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 19:54:32 +0100 |
wenzelm |
use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:38:41 +0100 |
wenzelm |
commit: non-critical, otherwise session restart will result in deadlock!
|
file |
diff |
annotate
|
| Fri, 26 Oct 2007 19:58:32 +0200 |
wenzelm |
replaced Secure.evaluate by ML_Context.evaluate;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2007 13:52:02 +0200 |
haftmann |
added function for evaluation by compiler invocation
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 20:10:35 +0200 |
wenzelm |
execute/system: non-critical;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 17:48:16 +0200 |
wenzelm |
improved error behaviour of use (bootstrap version);
|
file |
diff |
annotate
|
| Sun, 16 Sep 2007 14:55:48 +0200 |
wenzelm |
use_text/file: tune text (cf. ML_Parse.fix_ints);
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 17:28:55 +0200 |
wenzelm |
NAMED_CRITICAL;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 17:05:45 +0200 |
wenzelm |
added use_noncritical;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 14:06:12 +0200 |
wenzelm |
marked some CRITICAL sections (for multithreading);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:11 +0200 |
wenzelm |
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:43:42 +0100 |
wenzelm |
use_text: added name argument;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2006 19:05:23 +0100 |
wenzelm |
added use_file;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2006 14:14:11 +0200 |
wenzelm |
added execute/system;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 22:55:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 19:37:04 +0200 |
wenzelm |
Secure critical operations.
|
file |
diff |
annotate
|