require explicit initialization of options;
more explicit Position operations;

--- 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 = ""
 

--- 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 _ => ""
+    }
 }

--- 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)))
       })
   }
 

--- 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))
+    }
+  }
 }