Fri, 30 Aug 2013 22:22:07 +0200 |
wenzelm |
more general backup files;
|
file |
diff |
annotate
|
Tue, 16 Jul 2013 12:31:08 +0200 |
wenzelm |
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
|
file |
diff |
annotate
|
Tue, 14 May 2013 14:17:56 +0200 |
wenzelm |
more scalable File.write via separate chunks;
|
file |
diff |
annotate
|
Sun, 24 Mar 2013 16:19:54 +0100 |
wenzelm |
prefer preset = 3 -- much faster and less memory requirement;
|
file |
diff |
annotate
|
Sun, 24 Mar 2013 16:12:45 +0100 |
wenzelm |
basic support for xz files;
|
file |
diff |
annotate
|
Sat, 23 Feb 2013 12:28:18 +0100 |
wenzelm |
more permissive File.read_lines, which is relevant for Managed_Process join/kill;
|
file |
diff |
annotate
|
Sat, 12 Jan 2013 15:00:48 +0100 |
wenzelm |
immediate theory progress for build_dialog;
|
file |
diff |
annotate
|
Wed, 02 Jan 2013 15:08:38 +0100 |
wenzelm |
support File.read_gzip as well, in accordance to File.write_gzip;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 20:17:04 +0100 |
wenzelm |
explicit module UTF8;
|
file |
diff |
annotate
|
Mon, 01 Oct 2012 12:05:05 +0200 |
wenzelm |
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
|
file |
diff |
annotate
|
Thu, 27 Sep 2012 15:04:26 +0200 |
wenzelm |
physical File.eq in conformance to Isabelle/ML;
|
file |
diff |
annotate
|
Thu, 23 Aug 2012 20:34:51 +0200 |
wenzelm |
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
|
file |
diff |
annotate
|
Mon, 30 Jul 2012 20:43:07 +0200 |
wenzelm |
clarified directory content operations (similar to ML version);
|
file |
diff |
annotate
|
Fri, 27 Jul 2012 14:22:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 24 Jul 2012 23:01:55 +0200 |
wenzelm |
read/write dependency information;
|
file |
diff |
annotate
|
Sat, 21 Jul 2012 16:41:55 +0200 |
wenzelm |
some actual build function on ML side;
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 23:16:54 +0200 |
wenzelm |
more abstract file system operations in Scala, corresponding to ML version;
|
file |
diff |
annotate
|