# HG changeset patch # User wenzelm # Date 1342803033 -7200 # Node ID d0fa3efec93b51be4d6aa093cb233bcaf4cad5a9 # Parent 10b534e6420954f40ab7abf7332a13272b364e9f require explicit initialization of options; more explicit Position operations; diff -r 10b534e64209 -r d0fa3efec93b etc/options --- a/etc/options Fri Jul 20 17:43:55 2012 +0200 +++ b/etc/options Fri Jul 20 18:50:33 2012 +0200 @@ -1,24 +1,24 @@ (* :mode=isabelle-options: *) -declare browser_info : bool +declare browser_info : bool = false -declare document : bool define document = true -declare document_format : string define document_format = pdf -declare document_variants : string define document_variants = document -declare document_graph : bool +declare document : bool = true +declare document_format : string = pdf +declare document_variants : string = document +declare document_graph : bool = false -declare threads_limit : int -declare threads_trace : bool -declare parallel_proofs : bool define parallel_proofs = true -declare parallel_proofs_threshold : int +declare threads_limit : int = 1 +declare threads_trace : int = 0 +declare parallel_proofs : int = 1 +declare parallel_proofs_threshold : int = 100 -declare print_mode : string +declare print_mode : string = "" -declare proofs : bool -declare quick_and_dirty : bool +declare proofs : int = 0 +declare quick_and_dirty : bool = false -declare timing : bool -declare verbose : bool +declare timing : bool = false +declare verbose : bool = false -declare condition : string +declare condition : string = "" diff -r 10b534e64209 -r d0fa3efec93b src/Pure/General/position.scala --- a/src/Pure/General/position.scala Fri Jul 20 17:43:55 2012 +0200 +++ b/src/Pure/General/position.scala Fri Jul 20 18:50:33 2012 +0200 @@ -17,6 +17,9 @@ val File = new Properties.String(Isabelle_Markup.FILE) val Id = new Properties.Long(Isabelle_Markup.ID) + def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString)) + def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f) + object Range { def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop) @@ -47,4 +50,13 @@ def purge(props: T): T = for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x)) yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y)) + + + def str_of(props: T): String = + (Line.unapply(props), File.unapply(props)) match { + case (Some(i), None) => " (line " + i.toString + ")" + case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")" + case (None, Some(name)) => " (file " + quote(name) + ")" + case _ => "" + } } diff -r 10b534e64209 -r d0fa3efec93b src/Pure/System/build.scala --- a/src/Pure/System/build.scala Fri Jul 20 17:43:55 2012 +0200 +++ b/src/Pure/System/build.scala Fri Jul 20 18:50:33 2012 +0200 @@ -192,7 +192,7 @@ catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session entry " + - quote(entry.name) + " (file " + quote(root.toString) + ")") + quote(entry.name) + Position.str_of(Position.file(root))) }) } diff -r 10b534e64209 -r d0fa3efec93b src/Pure/System/options.scala --- a/src/Pure/System/options.scala Fri Jul 20 17:43:55 2012 +0200 +++ b/src/Pure/System/options.scala Fri Jul 20 18:50:33 2012 +0200 @@ -15,14 +15,13 @@ abstract class Type { def print: String = toString.toLowerCase - def init: String } - case object Bool extends Type { def init = "false" } - case object Int extends Type { def init = "0" } - case object Real extends Type { def init = "0.0" } - case object String extends Type { def init = "" } + case object Bool extends Type + case object Int extends Type + case object Real extends Type + case object String extends Type - case class Opt(typ: Type, description: String, value: String) + case class Opt(typ: Type, value: String, description: String) val empty: Options = new Options() @@ -42,12 +41,12 @@ val option_type = atom("option type", _.is_ident) val option_value = atom("option value", tok => tok.is_name || tok.is_float) - keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~ opt(text)) ^^ - { case _ ~ (x ~ _ ~ y ~ z) => (options: Options) => - options.declare(x, y, z.getOrElse("")) } | + keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~ + keyword("=") ~ option_value ~ opt(text)) ^^ + { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => + (options: Options) => options.declare(a, b, c, d.getOrElse("")) } | keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^ - { case _ ~ (x ~ _ ~ y) => (options: Options) => - options.define(x, y) } + { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) } } def parse_entries(file: File): List[Options => Options] = @@ -72,7 +71,7 @@ entry <- Parser.parse_entries(file) } { try { options = entry(options) } - catch { case ERROR(msg) => error(msg + " (file " + quote(file.toString) + ")") } + catch { case ERROR(msg) => error(msg + Position.str_of(Position.file(file))) } } options } @@ -84,7 +83,7 @@ override def toString: String = options.iterator.mkString("Options (", ",", ")") - /* basic operations */ + /* check */ private def check_name(name: String): Options.Opt = options.get(name) match { @@ -99,6 +98,15 @@ else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print) } + + /* basic operations */ + + private def put[A](name: String, typ: Options.Type, value: String): Options = + { + val opt = check_type(name, typ) + new Options(options + (name -> opt.copy(value = value))) + } + private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A = { val opt = check_type(name, typ) @@ -110,63 +118,6 @@ } } - private def put[A](name: String, typ: Options.Type, value: String): Options = - { - val opt = check_type(name, typ) - new Options(options + (name -> opt.copy(value = value))) - } - - - /* external declare and define */ - - def declare(name: String, typ_name: String, description: String = ""): Options = - { - options.get(name) match { - case Some(_) => error("Duplicate declaration of option " + quote(name)) - case None => - val typ = - typ_name match { - case "bool" => Options.Bool - case "int" => Options.Int - case "real" => Options.Real - case "string" => Options.String - case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name)) - } - new Options(options + (name -> Options.Opt(typ, description, typ.init))) - } - } - - def define(name: String, value: String): Options = - { - val opt = check_name(name) - val result = new Options(options + (name -> opt.copy(value = value))) - opt.typ match { - case Options.Bool => result.bool(name); () - case Options.Int => result.int(name); () - case Options.Real => result.real(name); () - case Options.String => result.string(name); () - } - result - } - - def define(name: String, opt_value: Option[String]): Options = - { - val opt = check_name(name) - opt_value match { - case Some(value) => define(name, value) - case None if opt.typ == Options.Bool => define(name, "true") - case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print) - } - } - - def define_simple(str: String): Options = - { - str.indexOf('=') match { - case -1 => define(str, None) - case i => define(str.substring(0, i), str.substring(i + 1)) - } - } - /* internal lookup and update */ @@ -196,4 +147,59 @@ def apply(name: String): String = get(name, Options.String, s => Some(s)) def update(name: String, x: String): Options = put(name, Options.String, x) } + + + /* external declare and define */ + + private def check_value(name: String): Options = + { + val opt = check_name(name) + opt.typ match { + case Options.Bool => bool(name); this + case Options.Int => int(name); this + case Options.Real => real(name); this + case Options.String => string(name); this + } + } + + def declare(name: String, typ_name: String, value: String, description: String = ""): Options = + { + options.get(name) match { + case Some(_) => error("Duplicate declaration of option " + quote(name)) + case None => + val typ = + typ_name match { + case "bool" => Options.Bool + case "int" => Options.Int + case "real" => Options.Real + case "string" => Options.String + case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name)) + } + (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name) + } + } + + def define(name: String, value: String): Options = + { + val opt = check_name(name) + (new Options(options + (name -> opt.copy(value = value)))).check_value(name) + } + + def define(name: String, opt_value: Option[String]): Options = + { + val opt = check_name(name) + opt_value match { + case Some(value) => define(name, value) + case None if opt.typ == Options.Bool => define(name, "true") + case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print) + } + } + + def define_simple(str: String): Options = + { + str.indexOf('=') match { + case -1 => define(str, None) + case i => define(str.substring(0, i), str.substring(i + 1)) + } + } }