define build_options from command line;
authorwenzelm
Fri Jul 20 16:47:43 2012 +0200 (2012-07-20)
changeset 48368dc538eef2cf2
parent 48367 680d297ec71b
child 48369 10b534e64209
define build_options from command line;
src/Pure/System/build.scala
src/Pure/System/options.scala
     1.1 --- a/src/Pure/System/build.scala	Fri Jul 20 16:47:17 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Fri Jul 20 16:47:43 2012 +0200
     1.3 @@ -257,6 +257,8 @@
     1.4    {
     1.5      val full_queue = find_sessions(more_dirs)
     1.6  
     1.7 +    val build_options = (Options.init() /: options)(_.define_simple(_))
     1.8 +
     1.9      sessions.filter(name => !full_queue.defined(name)) match {
    1.10        case Nil =>
    1.11        case bad => error("Undefined session(s): " + commas_quote(bad))
     2.1 --- a/src/Pure/System/options.scala	Fri Jul 20 16:47:17 2012 +0200
     2.2 +++ b/src/Pure/System/options.scala	Fri Jul 20 16:47:43 2012 +0200
     2.3 @@ -89,7 +89,7 @@
     2.4    private def check_name(name: String): Options.Opt =
     2.5      options.get(name) match {
     2.6        case Some(opt) => opt
     2.7 -      case None => error("Undeclared option " + quote(name))
     2.8 +      case None => error("Unknown option " + quote(name))
     2.9      }
    2.10  
    2.11    private def check_type(name: String, typ: Options.Type): Options.Opt =
    2.12 @@ -117,8 +117,6 @@
    2.13    }
    2.14  
    2.15  
    2.16 -
    2.17 -
    2.18    /* external declare and define */
    2.19  
    2.20    def declare(name: String, typ_name: String, description: String = ""): Options =
    2.21 @@ -151,6 +149,17 @@
    2.22      result
    2.23    }
    2.24  
    2.25 +  def define_simple(str: String): Options =
    2.26 +  {
    2.27 +    str.indexOf('=') match {
    2.28 +      case -1 =>
    2.29 +        val opt = check_name(str)
    2.30 +        if (opt.typ == Options.Bool) define(str, "true")
    2.31 +        else error("Missing value for option " + quote(str) + " : " + opt.typ.print)
    2.32 +      case i => define(str.substring(0, i), str.substring(i + 1))
    2.33 +    }
    2.34 +  }
    2.35 +
    2.36  
    2.37    /* internal lookup and update */
    2.38