src/Pure/config.ML

   val map_global: 'a T -> ('a -> 'a) -> theory -> theory
   val put_global: 'a T -> 'a -> theory -> theory
   val get_generic: Context.generic -> 'a T -> 'a
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
-  val declare: string -> (Context.generic -> value) -> raw
-  val declare_global: string -> (Context.generic -> value) -> raw
-  val declare_option: string -> raw
-  val declare_option_global: string -> raw
+  val declare: string * Position.T -> (Context.generic -> value) -> raw
+  val declare_global: string * Position.T -> (Context.generic -> value) -> raw
+  val declare_option: string * Position.T -> raw
+  val declare_option_global: string * Position.T -> raw
   val name_of: 'a T -> string
+  val pos_of: 'a T -> Position.T
 end;
 
 structure Config: CONFIG =
 struct
 

   | same_type (Int _) (Int _) = true
   | same_type (Real _) (Real _) = true
   | same_type (String _) (String _) = true
   | same_type _ _ = false;
 
-fun type_check name f value =
+fun type_check (name, pos) f value =
   let
     val value' = f value;
     val _ = same_type value value' orelse
-      error ("Ill-typed configuration option " ^ quote name ^ ": " ^
+      error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^
         print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
   in value' end;
 
 
 (* abstract configuration options *)
 
 datatype 'a T = Config of
  {name: string,
+  pos: Position.T,
   get_value: Context.generic -> 'a,
   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
 
 type raw = value T;
 
-fun coerce make dest (Config {name, get_value, map_value}) = Config
+fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
  {name = name,
+  pos = pos,
   get_value = dest o get_value,
   map_value = fn f => map_value (make o f o dest)};
 
 val bool = coerce Bool (fn Bool b => b);
 val int = coerce Int (fn Int i => i);

   fun merge data = Inttab.merge (K true) data;
 );
 
 local
 
-fun declare_generic global name default =
+fun declare_generic global (name, pos) default =
   let
     val id = serial ();
 
     fun get_value context =
       (case Inttab.lookup (Value.get context) id of
         SOME value => value
       | NONE => default context);
 
     fun update_value f context =
-      Value.map (Inttab.update (id, type_check name f (get_value context))) context;
+      Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
 
     fun map_value f (context as Context.Proof ctxt) =
           let val context' = update_value f context in
             if global andalso
               Context_Position.is_visible ctxt andalso

                 warning ("Ignoring local change of global option " ^ quote name)
               else (); context)
             else context'
           end
       | map_value f context = update_value f context;
-  in Config {name = name, get_value = get_value, map_value = map_value} end;
+  in Config {name = name, pos = pos, get_value = get_value, map_value = map_value} end;
 
-fun declare_option_generic global name =
+fun declare_option_generic global (name, pos) =
   let
     val typ = Options.default_typ name;
     val default =
       if typ = Options.boolT then fn _ => Bool (Options.default_bool name)
       else if typ = Options.intT then fn _ => Int (Options.default_int name)
       else if typ = Options.realT then fn _ => Real (Options.default_real name)
       else if typ = Options.stringT then fn _ => String (Options.default_string name)
-      else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
-  in declare_generic global name default end;
+      else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
+  in declare_generic global (name, pos) default end;
 
 in
 
 val declare = declare_generic false;
 val declare_global = declare_generic true;

 val declare_option_global = declare_option_generic true;
 
 end;
 
 fun name_of (Config {name, ...}) = name;
+fun pos_of (Config {pos, ...}) = pos;
 
 
 (*final declarations of this structure!*)
 val get = get_ctxt;
 val map = map_ctxt;