require explicit initialization of options;
authorwenzelm
Fri Jul 20 18:50:33 2012 +0200 (2012-07-20)
changeset 48370d0fa3efec93b
parent 48369 10b534e64209
child 48373 527e2bad7cca
require explicit initialization of options;
more explicit Position operations;
etc/options
src/Pure/General/position.scala
src/Pure/System/build.scala
src/Pure/System/options.scala
     1.1 --- a/etc/options	Fri Jul 20 17:43:55 2012 +0200
     1.2 +++ b/etc/options	Fri Jul 20 18:50:33 2012 +0200
     1.3 @@ -1,24 +1,24 @@
     1.4  (* :mode=isabelle-options: *)
     1.5  
     1.6 -declare browser_info : bool
     1.7 +declare browser_info : bool = false
     1.8  
     1.9 -declare document : bool               define document = true
    1.10 -declare document_format : string      define document_format = pdf
    1.11 -declare document_variants : string    define document_variants = document
    1.12 -declare document_graph : bool
    1.13 +declare document : bool = true
    1.14 +declare document_format : string = pdf
    1.15 +declare document_variants : string = document
    1.16 +declare document_graph : bool = false
    1.17  
    1.18 -declare threads_limit : int
    1.19 -declare threads_trace : bool
    1.20 -declare parallel_proofs : bool        define parallel_proofs = true
    1.21 -declare parallel_proofs_threshold : int
    1.22 +declare threads_limit : int = 1
    1.23 +declare threads_trace : int = 0
    1.24 +declare parallel_proofs : int = 1
    1.25 +declare parallel_proofs_threshold : int = 100
    1.26  
    1.27 -declare print_mode : string
    1.28 +declare print_mode : string = ""
    1.29  
    1.30 -declare proofs : bool
    1.31 -declare quick_and_dirty : bool
    1.32 +declare proofs : int = 0
    1.33 +declare quick_and_dirty : bool = false
    1.34  
    1.35 -declare timing : bool
    1.36 -declare verbose : bool
    1.37 +declare timing : bool = false
    1.38 +declare verbose : bool = false
    1.39  
    1.40 -declare condition : string
    1.41 +declare condition : string = ""
    1.42  
     2.1 --- a/src/Pure/General/position.scala	Fri Jul 20 17:43:55 2012 +0200
     2.2 +++ b/src/Pure/General/position.scala	Fri Jul 20 18:50:33 2012 +0200
     2.3 @@ -17,6 +17,9 @@
     2.4    val File = new Properties.String(Isabelle_Markup.FILE)
     2.5    val Id = new Properties.Long(Isabelle_Markup.ID)
     2.6  
     2.7 +  def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString))
     2.8 +  def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f)
     2.9 +
    2.10    object Range
    2.11    {
    2.12      def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
    2.13 @@ -47,4 +50,13 @@
    2.14    def purge(props: T): T =
    2.15      for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
    2.16        yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
    2.17 +
    2.18 +
    2.19 +  def str_of(props: T): String =
    2.20 +    (Line.unapply(props), File.unapply(props)) match {
    2.21 +      case (Some(i), None) => " (line " + i.toString + ")"
    2.22 +      case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
    2.23 +      case (None, Some(name)) => " (file " + quote(name) + ")"
    2.24 +      case _ => ""
    2.25 +    }
    2.26  }
     3.1 --- a/src/Pure/System/build.scala	Fri Jul 20 17:43:55 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Fri Jul 20 18:50:33 2012 +0200
     3.3 @@ -192,7 +192,7 @@
     3.4        catch {
     3.5          case ERROR(msg) =>
     3.6            error(msg + "\nThe error(s) above occurred in session entry " +
     3.7 -            quote(entry.name) + " (file " + quote(root.toString) + ")")
     3.8 +            quote(entry.name) + Position.str_of(Position.file(root)))
     3.9        })
    3.10    }
    3.11  
     4.1 --- a/src/Pure/System/options.scala	Fri Jul 20 17:43:55 2012 +0200
     4.2 +++ b/src/Pure/System/options.scala	Fri Jul 20 18:50:33 2012 +0200
     4.3 @@ -15,14 +15,13 @@
     4.4    abstract class Type
     4.5    {
     4.6      def print: String = toString.toLowerCase
     4.7 -    def init: String
     4.8    }
     4.9 -  case object Bool extends Type { def init = "false" }
    4.10 -  case object Int extends Type { def init = "0" }
    4.11 -  case object Real extends Type { def init = "0.0" }
    4.12 -  case object String extends Type { def init = "" }
    4.13 +  case object Bool extends Type
    4.14 +  case object Int extends Type
    4.15 +  case object Real extends Type
    4.16 +  case object String extends Type
    4.17  
    4.18 -  case class Opt(typ: Type, description: String, value: String)
    4.19 +  case class Opt(typ: Type, value: String, description: String)
    4.20  
    4.21    val empty: Options = new Options()
    4.22  
    4.23 @@ -42,12 +41,12 @@
    4.24        val option_type = atom("option type", _.is_ident)
    4.25        val option_value = atom("option value", tok => tok.is_name || tok.is_float)
    4.26  
    4.27 -      keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~ opt(text)) ^^
    4.28 -        { case _ ~ (x ~ _ ~ y ~ z) => (options: Options) =>
    4.29 -            options.declare(x, y, z.getOrElse("")) } |
    4.30 +      keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
    4.31 +      keyword("=") ~ option_value ~ opt(text)) ^^
    4.32 +        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) =>
    4.33 +            (options: Options) => options.declare(a, b, c, d.getOrElse("")) } |
    4.34        keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
    4.35 -        { case _ ~ (x ~ _ ~ y) => (options: Options) =>
    4.36 -            options.define(x, y) }
    4.37 +        { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
    4.38      }
    4.39  
    4.40      def parse_entries(file: File): List[Options => Options] =
    4.41 @@ -72,7 +71,7 @@
    4.42        entry <- Parser.parse_entries(file)
    4.43      } {
    4.44        try { options = entry(options) }
    4.45 -      catch { case ERROR(msg) => error(msg + " (file " + quote(file.toString) + ")") }
    4.46 +      catch { case ERROR(msg) => error(msg + Position.str_of(Position.file(file))) }
    4.47      }
    4.48      options
    4.49    }
    4.50 @@ -84,7 +83,7 @@
    4.51    override def toString: String = options.iterator.mkString("Options (", ",", ")")
    4.52  
    4.53  
    4.54 -  /* basic operations */
    4.55 +  /* check */
    4.56  
    4.57    private def check_name(name: String): Options.Opt =
    4.58      options.get(name) match {
    4.59 @@ -99,6 +98,15 @@
    4.60      else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
    4.61    }
    4.62  
    4.63 +
    4.64 +  /* basic operations */
    4.65 +
    4.66 +  private def put[A](name: String, typ: Options.Type, value: String): Options =
    4.67 +  {
    4.68 +    val opt = check_type(name, typ)
    4.69 +    new Options(options + (name -> opt.copy(value = value)))
    4.70 +  }
    4.71 +
    4.72    private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
    4.73    {
    4.74      val opt = check_type(name, typ)
    4.75 @@ -110,63 +118,6 @@
    4.76      }
    4.77    }
    4.78  
    4.79 -  private def put[A](name: String, typ: Options.Type, value: String): Options =
    4.80 -  {
    4.81 -    val opt = check_type(name, typ)
    4.82 -    new Options(options + (name -> opt.copy(value = value)))
    4.83 -  }
    4.84 -
    4.85 -
    4.86 -  /* external declare and define */
    4.87 -
    4.88 -  def declare(name: String, typ_name: String, description: String = ""): Options =
    4.89 -  {
    4.90 -    options.get(name) match {
    4.91 -      case Some(_) => error("Duplicate declaration of option " + quote(name))
    4.92 -      case None =>
    4.93 -        val typ =
    4.94 -          typ_name match {
    4.95 -            case "bool" => Options.Bool
    4.96 -            case "int" => Options.Int
    4.97 -            case "real" => Options.Real
    4.98 -            case "string" => Options.String
    4.99 -            case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name))
   4.100 -          }
   4.101 -        new Options(options + (name -> Options.Opt(typ, description, typ.init)))
   4.102 -    }
   4.103 -  }
   4.104 -
   4.105 -  def define(name: String, value: String): Options =
   4.106 -  {
   4.107 -    val opt = check_name(name)
   4.108 -    val result = new Options(options + (name -> opt.copy(value = value)))
   4.109 -    opt.typ match {
   4.110 -      case Options.Bool => result.bool(name); ()
   4.111 -      case Options.Int => result.int(name); ()
   4.112 -      case Options.Real => result.real(name); ()
   4.113 -      case Options.String => result.string(name); ()
   4.114 -    }
   4.115 -    result
   4.116 -  }
   4.117 -
   4.118 -  def define(name: String, opt_value: Option[String]): Options =
   4.119 -  {
   4.120 -    val opt = check_name(name)
   4.121 -    opt_value match {
   4.122 -      case Some(value) => define(name, value)
   4.123 -      case None if opt.typ == Options.Bool => define(name, "true")
   4.124 -      case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
   4.125 -    }
   4.126 -  }
   4.127 -
   4.128 -  def define_simple(str: String): Options =
   4.129 -  {
   4.130 -    str.indexOf('=') match {
   4.131 -      case -1 => define(str, None)
   4.132 -      case i => define(str.substring(0, i), str.substring(i + 1))
   4.133 -    }
   4.134 -  }
   4.135 -
   4.136  
   4.137    /* internal lookup and update */
   4.138  
   4.139 @@ -196,4 +147,59 @@
   4.140      def apply(name: String): String = get(name, Options.String, s => Some(s))
   4.141      def update(name: String, x: String): Options = put(name, Options.String, x)
   4.142    }
   4.143 +
   4.144 +
   4.145 +  /* external declare and define */
   4.146 +
   4.147 +  private def check_value(name: String): Options =
   4.148 +  {
   4.149 +    val opt = check_name(name)
   4.150 +    opt.typ match {
   4.151 +      case Options.Bool => bool(name); this
   4.152 +      case Options.Int => int(name); this
   4.153 +      case Options.Real => real(name); this
   4.154 +      case Options.String => string(name); this
   4.155 +    }
   4.156 +  }
   4.157 +
   4.158 +  def declare(name: String, typ_name: String, value: String, description: String = ""): Options =
   4.159 +  {
   4.160 +    options.get(name) match {
   4.161 +      case Some(_) => error("Duplicate declaration of option " + quote(name))
   4.162 +      case None =>
   4.163 +        val typ =
   4.164 +          typ_name match {
   4.165 +            case "bool" => Options.Bool
   4.166 +            case "int" => Options.Int
   4.167 +            case "real" => Options.Real
   4.168 +            case "string" => Options.String
   4.169 +            case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name))
   4.170 +          }
   4.171 +        (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name)
   4.172 +    }
   4.173 +  }
   4.174 +
   4.175 +  def define(name: String, value: String): Options =
   4.176 +  {
   4.177 +    val opt = check_name(name)
   4.178 +    (new Options(options + (name -> opt.copy(value = value)))).check_value(name)
   4.179 +  }
   4.180 +
   4.181 +  def define(name: String, opt_value: Option[String]): Options =
   4.182 +  {
   4.183 +    val opt = check_name(name)
   4.184 +    opt_value match {
   4.185 +      case Some(value) => define(name, value)
   4.186 +      case None if opt.typ == Options.Bool => define(name, "true")
   4.187 +      case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
   4.188 +    }
   4.189 +  }
   4.190 +
   4.191 +  def define_simple(str: String): Options =
   4.192 +  {
   4.193 +    str.indexOf('=') match {
   4.194 +      case -1 => define(str, None)
   4.195 +      case i => define(str.substring(0, i), str.substring(i + 1))
   4.196 +    }
   4.197 +  }
   4.198  }