src/Pure/General/secure.ML
Wed, 17 Sep 2008 21:27:24 +0200 wenzelm use_text/use_file now depend on explicit ML name space;
Wed, 14 May 2008 11:05:11 +0200 wenzelm use_text/file: proper position output;
Mon, 24 Mar 2008 23:34:24 +0100 wenzelm ML runtime compilation: pass position, tuned signature;
Wed, 19 Mar 2008 14:25:59 +0100 wenzelm system: writeln output, if available;
Thu, 06 Mar 2008 20:17:50 +0100 wenzelm common setup for system_out/system;
Sat, 16 Feb 2008 16:43:57 +0100 wenzelm export deny_secure;
Tue, 01 Jan 2008 16:09:27 +0100 wenzelm tuned spaces;
Tue, 18 Dec 2007 22:21:41 +0100 wenzelm removed obsolete use_noncritical (plain use is already non-critical);
Tue, 18 Dec 2007 19:54:32 +0100 wenzelm use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
Thu, 29 Nov 2007 17:38:41 +0100 wenzelm commit: non-critical, otherwise session restart will result in deadlock!
Fri, 26 Oct 2007 19:58:32 +0200 wenzelm replaced Secure.evaluate by ML_Context.evaluate;
Thu, 25 Oct 2007 13:52:02 +0200 haftmann added function for evaluation by compiler invocation
Fri, 05 Oct 2007 20:10:35 +0200 wenzelm execute/system: non-critical;
Thu, 20 Sep 2007 17:48:16 +0200 wenzelm improved error behaviour of use (bootstrap version);
Sun, 16 Sep 2007 14:55:48 +0200 wenzelm use_text/file: tune text (cf. ML_Parse.fix_ints);
Sun, 29 Jul 2007 17:28:55 +0200 wenzelm NAMED_CRITICAL;
Wed, 25 Jul 2007 17:05:45 +0200 wenzelm added use_noncritical;
Mon, 23 Jul 2007 14:06:12 +0200 wenzelm marked some CRITICAL sections (for multithreading);
Tue, 03 Apr 2007 19:24:11 +0200 wenzelm removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
Sun, 21 Jan 2007 16:43:42 +0100 wenzelm use_text: added name argument;
Mon, 11 Dec 2006 19:05:23 +0100 wenzelm added use_file;
Thu, 12 Oct 2006 14:14:11 +0200 wenzelm added execute/system;
Wed, 11 Oct 2006 22:55:14 +0200 wenzelm tuned signature;
Mon, 09 Oct 2006 19:37:04 +0200 wenzelm Secure critical operations.
less more (0) tip