src/Pure/General/path.scala
2012-07-20 wenzelm 2012-07-20 more explicit java.io.{File => JFile};
2012-07-20 wenzelm 2012-07-20 further imitation of "usedir" shell script; Pure/build observes build_images option, unlike traditional version; tuned signature;
2012-04-22 wenzelm 2012-04-22 USER_HOME settings variable points to cross-platform user home directory;
2012-02-27 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2011-10-22 wenzelm 2011-10-22 class Path as abstract datatype;
2011-07-07 wenzelm 2011-07-07 explicit Document.Node.Header, with master_dir and thy_name; imitate ML path operations more closely;
2011-07-05 wenzelm 2011-07-05 prefer space_explode/split_lines as in Isabelle/ML;
2011-07-05 wenzelm 2011-07-05 Path.split convenience;
2011-07-05 wenzelm 2011-07-05 tuned;
2011-07-04 wenzelm 2011-07-04 pervasive Basic_Library in Scala; tuned;
2011-06-30 wenzelm 2011-06-30 proper fold order;
2011-06-30 wenzelm 2011-06-30 more Path operations; tuned signature;
2011-06-30 wenzelm 2011-06-30 tuned comments;
2011-06-30 wenzelm 2011-06-30 abstract algebra of file paths in Scala (cf. path.ML);