src/Pure/General/path.scala
Fri, 20 Jul 2012 21:04:03 +0200 wenzelm further imitation of "usedir" shell script;
Sun, 22 Apr 2012 14:30:18 +0200 wenzelm USER_HOME settings variable points to cross-platform user home directory;
Mon, 27 Feb 2012 17:13:25 +0100 wenzelm prefer final ADTs -- prevent ooddities;
Sat, 22 Oct 2011 19:15:32 +0200 wenzelm class Path as abstract datatype;
Thu, 07 Jul 2011 22:04:30 +0200 wenzelm explicit Document.Node.Header, with master_dir and thy_name;
Tue, 05 Jul 2011 21:32:48 +0200 wenzelm prefer space_explode/split_lines as in Isabelle/ML;
Tue, 05 Jul 2011 21:20:24 +0200 wenzelm Path.split convenience;
Tue, 05 Jul 2011 10:54:05 +0200 wenzelm tuned;
Mon, 04 Jul 2011 16:51:45 +0200 wenzelm pervasive Basic_Library in Scala;
Thu, 30 Jun 2011 14:51:32 +0200 wenzelm proper fold order;
Thu, 30 Jun 2011 14:03:31 +0200 wenzelm more Path operations;
Thu, 30 Jun 2011 11:15:36 +0200 wenzelm tuned comments;
Thu, 30 Jun 2011 00:09:57 +0200 wenzelm abstract algebra of file paths in Scala (cf. path.ML);
less more (0) tip