src/Pure/System/options.ML
2012-07-23 wenzelm 2012-07-23 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);