Fri, 03 Aug 2012 13:06:25 +0200 |
wenzelm |
reject path variable nesting explicitly;
|
file |
diff |
annotate
|
Fri, 27 Jul 2012 14:09:59 +0200 |
wenzelm |
simplified Path vs. JVM File operations;
|
file |
diff |
annotate
|
Tue, 24 Jul 2012 20:56:18 +0200 |
wenzelm |
more explicit checks during parsing;
|
file |
diff |
annotate
|
Tue, 24 Jul 2012 00:29:36 +0200 |
wenzelm |
pass build options to ML;
|
file |
diff |
annotate
|
Sat, 21 Jul 2012 21:16:08 +0200 |
wenzelm |
disallow quotes in path specifications -- extra paranoia;
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:29:25 +0200 |
wenzelm |
more explicit java.io.{File => JFile};
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 21:04:03 +0200 |
wenzelm |
further imitation of "usedir" shell script;
|
file |
diff |
annotate
|
Sun, 22 Apr 2012 14:30:18 +0200 |
wenzelm |
USER_HOME settings variable points to cross-platform user home directory;
|
file |
diff |
annotate
|
Mon, 27 Feb 2012 17:13:25 +0100 |
wenzelm |
prefer final ADTs -- prevent ooddities;
|
file |
diff |
annotate
|
Sat, 22 Oct 2011 19:15:32 +0200 |
wenzelm |
class Path as abstract datatype;
|
file |
diff |
annotate
|
Thu, 07 Jul 2011 22:04:30 +0200 |
wenzelm |
explicit Document.Node.Header, with master_dir and thy_name;
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 21:32:48 +0200 |
wenzelm |
prefer space_explode/split_lines as in Isabelle/ML;
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 21:20:24 +0200 |
wenzelm |
Path.split convenience;
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 10:54:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 04 Jul 2011 16:51:45 +0200 |
wenzelm |
pervasive Basic_Library in Scala;
|
file |
diff |
annotate
|
Thu, 30 Jun 2011 14:51:32 +0200 |
wenzelm |
proper fold order;
|
file |
diff |
annotate
|
Thu, 30 Jun 2011 14:03:31 +0200 |
wenzelm |
more Path operations;
|
file |
diff |
annotate
|
Thu, 30 Jun 2011 11:15:36 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
Thu, 30 Jun 2011 00:09:57 +0200 |
wenzelm |
abstract algebra of file paths in Scala (cf. path.ML);
|
file |
diff |
annotate
|