# HG changeset patch
# User wenzelm
# Date 1342795663 -7200
# Node ID dc538eef2cf20af89c8a70c4e77d802121c3769d
# Parent  680d297ec71bdfdaf708490117d2abc251a48cb5
define build_options from command line;

diff -r 680d297ec71b -r dc538eef2cf2 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Jul 20 16:47:17 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 20 16:47:43 2012 +0200
@@ -257,6 +257,8 @@
   {
     val full_queue = find_sessions(more_dirs)
 
+    val build_options = (Options.init() /: options)(_.define_simple(_))
+
     sessions.filter(name => !full_queue.defined(name)) match {
       case Nil =>
       case bad => error("Undefined session(s): " + commas_quote(bad))
diff -r 680d297ec71b -r dc538eef2cf2 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Fri Jul 20 16:47:17 2012 +0200
+++ b/src/Pure/System/options.scala	Fri Jul 20 16:47:43 2012 +0200
@@ -89,7 +89,7 @@
   private def check_name(name: String): Options.Opt =
     options.get(name) match {
       case Some(opt) => opt
-      case None => error("Undeclared option " + quote(name))
+      case None => error("Unknown option " + quote(name))
     }
 
   private def check_type(name: String, typ: Options.Type): Options.Opt =
@@ -117,8 +117,6 @@
   }
 
 
-
-
   /* external declare and define */
 
   def declare(name: String, typ_name: String, description: String = ""): Options =
@@ -151,6 +149,17 @@
     result
   }
 
+  def define_simple(str: String): Options =
+  {
+    str.indexOf('=') match {
+      case -1 =>
+        val opt = check_name(str)
+        if (opt.typ == Options.Bool) define(str, "true")
+        else error("Missing value for option " + quote(str) + " : " + opt.typ.print)
+      case i => define(str.substring(0, i), str.substring(i + 1))
+    }
+  }
+
 
   /* internal lookup and update */