src/Pure/System/options.scala

--- a/src/Pure/System/options.scala	Mon Aug 06 14:33:23 2012 +0200
+++ b/src/Pure/System/options.scala	Mon Aug 06 16:05:29 2012 +0200
@@ -83,6 +83,25 @@
   /* encode */
 
   val encode: XML.Encode.T[Options] = (options => options.encode)
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool {
+      args.toList match {
+        case export_file :: more_options =>
+          val options = (Options.init() /: more_options)(_.define_simple(_))
+
+          if (export_file == "") java.lang.System.out.println(options.print)
+          else File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
+
+          0
+        case _ => error("Bad arguments:\n" + cat_lines(args))
+      }
+    }
+  }
 }
 
 
@@ -90,6 +109,12 @@
 {
   override def toString: String = options.iterator.mkString("Options (", ",", ")")
 
+  def print: String =
+    cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
+      name + " : " + opt.typ.print + " = " +
+        (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
+      "\n  -- " + quote(opt.description) }))
+
 
   /* check */