diff -r a509f19d4cc6 -r d8ff14f44a40 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Jul 23 21:01:16 2012 +0200
+++ b/src/Pure/System/options.scala	Mon Jul 23 22:35:10 2012 +0200
@@ -177,7 +177,7 @@
             case "int" => Options.Int
             case "real" => Options.Real
             case "string" => Options.String
-            case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name))
+            case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
           }
         (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name)
     }
@@ -209,4 +209,14 @@
       case i => define(str.substring(0, i), str.substring(i + 1))
     }
   }
+
+
+  /* encode */
+
+  def encode: XML.Body =
+  {
+    import XML.Encode.{string => str, _}
+    list(triple(str, str, str))(
+      options.toList.map({ case (name, opt) => (name, opt.typ.print, opt.value) }))
+  }
 }