src/Pure/System/options.ML

   val realT: string
   val stringT: string
   val unknownT: string
   type T
   val empty: T
+  val position: T -> string -> Position.T
   val typ: T -> string -> string
   val bool: T -> string -> bool
   val int: T -> string -> int
   val real: T -> string -> real
   val string: T -> string -> string
   val put_bool: string -> bool -> T -> T
   val put_int: string -> int -> T -> T
   val put_real: string -> real -> T -> T
   val put_string: string -> string -> T -> T
-  val declare: {name: string, typ: string, value: string} -> T -> T
+  val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T
   val update: string -> string -> T -> T
   val decode: XML.body -> T
   val default: unit -> T
+  val default_position: string -> Position.T
   val default_typ: string -> string
   val default_bool: string -> bool
   val default_int: string -> int
   val default_real: string -> real
   val default_string: string -> string

 val intT = "int";
 val realT = "real";
 val stringT = "string";
 val unknownT = "unknown";
 
-datatype T = Options of {typ: string, value: string} Symtab.table;
+datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table;
 
 val empty = Options Symtab.empty;
 
 
 (* check *)

     if #typ opt = typ then opt
     else error ("Ill-typed system option " ^ quote name ^ " : " ^ #typ opt ^ " vs. " ^ typ)
   end;
 
 
-(* typ *)
-
+(* declaration *)
+
+fun position options name = #pos (check_name options name);
 fun typ options name = #typ (check_name options name);
 
 
 (* basic operations *)
 
 fun put T print name x (options as Options tab) =
   let val opt = check_type options name T
-  in Options (Symtab.update (name, {typ = #typ opt, value = print x}) tab) end;
+  in Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = print x}) tab) end;
 
 fun get T parse options name =
   let val opt = check_type options name T in
     (case parse (#value opt) of
       SOME x => x

     else if #typ opt = realT then ignore (real options name)
     else if #typ opt = stringT then ignore (string options name)
     else ()
   end;
 
-fun declare {name, typ, value} (Options tab) =
+fun declare {pos, name, typ, value} (Options tab) =
   let
-    val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
-      handle Symtab.DUP _ => error ("Duplicate declaration of system option " ^ quote name);
+    val options' =
+      (case Symtab.lookup tab name of
+        SOME other =>
+          error ("Duplicate declaration of system option " ^ quote name ^ Position.here pos ^
+            Position.here (#pos other))
+      | NONE => Options (Symtab.update (name, {pos = pos, typ = typ, value = value}) tab));
     val _ =
       typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse
-        error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ);
+        error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ ^
+          Position.here pos);
     val _ = check_value options' name;
   in options' end;
 
 fun update name value (options as Options tab) =
   let
     val opt = check_name options name;
-    val options' = Options (Symtab.update (name, {typ = #typ opt, value = value}) tab);
+    val options' =
+      Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = value}) tab);
     val _ = check_value options' name;
   in options' end;
 
 
 (* decode *)
 
-fun decode body =
-  fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
-    (let open XML.Decode in list (triple string string string) end body) empty;
+fun decode_opt body =
+  let open XML.Decode
+  in list (pair properties (pair string (pair string string))) end body
+  |> map (fn (props, (name, (typ, value))) =>
+      {pos = Position.of_properties props, name = name, typ = typ, value = value});
+
+fun decode body = fold declare (decode_opt body) empty;
 
 
 
 (** global default **)
 

 fun default () =
   (case Synchronized.value global_default of
     SOME options => options
   | NONE => err_no_default ());
 
+fun default_position name = position (default ()) name;
 fun default_typ name = typ (default ()) name;
 fun default_bool name = bool (default ()) name;
 fun default_int name = int (default ()) name;
 fun default_real name = real (default ()) name;
 fun default_string name = string (default ()) name;