src/Pure/System/options.scala
2012-07-30 wenzelm 2012-07-30 allow negative int values as well, according to real = int | float;
2012-07-28 wenzelm 2012-07-28 some description of main build options;
2012-07-27 wenzelm 2012-07-27 simplified Path vs. JVM File operations;
2012-07-24 wenzelm 2012-07-24 pass build options to ML; some imitation of usedir Session.init;
2012-07-23 wenzelm 2012-07-23 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
2012-07-21 wenzelm 2012-07-21 propagate defined options; misc tuning;
2012-07-20 wenzelm 2012-07-20 more abstract file system operations in Scala, corresponding to ML version;
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-07-20 wenzelm 2012-07-20 require explicit initialization of options; more explicit Position operations;
2012-07-20 wenzelm 2012-07-20 tuned signature;
2012-07-20 wenzelm 2012-07-20 define build_options from command line;
2012-07-20 wenzelm 2012-07-20 basic support for stand-alone options with external string representation;