more source positions;

--- a/src/Pure/General/name_space.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/General/name_space.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -189,13 +189,13 @@
 
 (* extern *)
 
-val names_long_raw = Config.declare_option "names_long";
+val names_long_raw = Config.declare_option ("names_long", @{here});
 val names_long = Config.bool names_long_raw;
 
-val names_short_raw = Config.declare_option "names_short";
+val names_short_raw = Config.declare_option ("names_short", @{here});
 val names_short = Config.bool names_short_raw;
 
-val names_unique_raw = Config.declare_option "names_unique";
+val names_unique_raw = Config.declare_option ("names_unique", @{here});
 val names_unique = Config.bool names_unique_raw;
 
 fun extern ctxt space name =

--- a/src/Pure/Isar/attrib.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -58,14 +58,14 @@
   val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
   val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
   val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
-  val option_bool: string -> bool Config.T * (theory -> theory)
-  val option_int: string -> int Config.T * (theory -> theory)
-  val option_real: string -> real Config.T * (theory -> theory)
-  val option_string: string -> string Config.T * (theory -> theory)
-  val setup_option_bool: string -> bool Config.T
-  val setup_option_int: string -> int Config.T
-  val setup_option_real: string -> real Config.T
-  val setup_option_string: string -> string Config.T
+  val option_bool: string * Position.T -> bool Config.T * (theory -> theory)
+  val option_int: string * Position.T -> int Config.T * (theory -> theory)
+  val option_real: string * Position.T -> real Config.T * (theory -> theory)
+  val option_string: string * Position.T -> string Config.T * (theory -> theory)
+  val setup_option_bool: string * Position.T -> bool Config.T
+  val setup_option_int: string * Position.T -> int Config.T
+  val setup_option_real: string * Position.T -> real Config.T
+  val setup_option_string: string * Position.T -> string Config.T
 end;
 
 structure Attrib: ATTRIB =
@@ -374,13 +374,15 @@
 fun declare make coerce binding default =
   let
     val name = Binding.name_of binding;
-    val config_value = Config.declare name (make o default);
+    val pos = Binding.pos_of binding;
+    val config_value = Config.declare (name, pos) (make o default);
     val config = coerce config_value;
   in (config, register binding config_value) end;
 
 in
 
-fun register_config config = register (Binding.name (Config.name_of config)) config;
+fun register_config config =
+  register (Binding.make (Config.name_of config, Config.pos_of config)) config;
 
 val config_bool = declare Config.Bool Config.bool;
 val config_int = declare Config.Int Config.int;
@@ -414,14 +416,14 @@
 
 local
 
-fun declare_option coerce name =
+fun declare_option coerce (name, pos) =
   let
-    val config = Config.declare_option name;
+    val config = Config.declare_option (name, pos);
   in (coerce config, register_config config) end;
 
-fun setup_option coerce name =
+fun setup_option coerce (name, pos) =
   let
-    val config = Config.declare_option name;
+    val config = Config.declare_option (name, pos);
     val _ = Theory.setup (register_config config);
   in coerce config end;
 

--- a/src/Pure/Isar/proof_context.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -572,7 +572,7 @@
 
 end;
 
-val show_abbrevs_raw = Config.declare "show_abbrevs" (fn _ => Config.Bool true);
+val show_abbrevs_raw = Config.declare ("show_abbrevs", @{here}) (fn _ => Config.Bool true);
 val show_abbrevs = Config.bool show_abbrevs_raw;
 
 fun contract_abbrevs ctxt t =
@@ -605,7 +605,8 @@
 
 local
 
-val dummies = Config.bool (Config.declare "Proof_Context.dummies" (K (Config.Bool false)));
+val dummies =
+  Config.bool (Config.declare ("Proof_Context.dummies", @{here}) (K (Config.Bool false)));
 
 fun check_dummies ctxt t =
   if Config.get ctxt dummies then t
@@ -1338,8 +1339,11 @@
 
 (* core context *)
 
-val debug = Config.bool (Config.declare "Proof_Context.debug" (K (Config.Bool false)));
-val verbose = Config.bool (Config.declare "Proof_Context.verbose" (K (Config.Bool false)));
+val debug =
+  Config.bool (Config.declare ("Proof_Context.debug", @{here}) (K (Config.Bool false)));
+
+val verbose =
+  Config.bool (Config.declare ("Proof_Context.verbose", @{here}) (K (Config.Bool false)));
 
 fun pretty_ctxt ctxt =
   if not (Config.get ctxt debug) then []

--- a/src/Pure/ML/ml_options.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/ML/ml_options.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -21,13 +21,14 @@
 
 (* source trace *)
 
-val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
+val source_trace_raw =
+  Config.declare ("ML_source_trace", @{here}) (fn _ => Config.Bool false);
 val source_trace = Config.bool source_trace_raw;
 
 
 (* exception trace *)
 
-val exception_trace_raw = Config.declare_option "ML_exception_trace";
+val exception_trace_raw = Config.declare_option ("ML_exception_trace", @{here});
 val exception_trace = Config.bool exception_trace_raw;
 
 fun exception_trace_enabled NONE =
@@ -38,7 +39,7 @@
 (* print depth *)
 
 val print_depth_raw =
-  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
+  Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (get_default_print_depth ()));
 val print_depth = Config.int print_depth_raw;
 
 fun get_print_depth () =

--- a/src/Pure/ROOT.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -141,9 +141,6 @@
 use "context_position.ML";
 use "config.ML";
 
-val quick_and_dirty_raw = Config.declare_option "quick_and_dirty";
-val quick_and_dirty = Config.bool quick_and_dirty_raw;
-
 
 (* inner syntax *)
 

--- a/src/Pure/Syntax/ast.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/Syntax/ast.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -164,10 +164,10 @@
 
 (* normalize *)
 
-val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
+val trace_raw = Config.declare ("syntax_ast_trace", @{here}) (fn _ => Config.Bool false);
 val trace = Config.bool trace_raw;
 
-val stats_raw = Config.declare "syntax_ast_stats" (fn _ => Config.Bool false);
+val stats_raw = Config.declare ("syntax_ast_stats", @{here}) (fn _ => Config.Bool false);
 val stats = Config.bool stats_raw;
 
 fun message head body =

--- a/src/Pure/Syntax/parser.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/Syntax/parser.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -626,7 +626,8 @@
 
 
 (*trigger value for warnings*)
-val branching_level = Config.int (Config.declare "syntax_branching_level" (fn _ => Config.Int 600));
+val branching_level =
+  Config.int (Config.declare ("syntax_branching_level", @{here}) (fn _ => Config.Int 600));
 
 (*get all productions of a NT and NTs chained to it which can
   be started by specified token*)

--- a/src/Pure/Syntax/printer.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/Syntax/printer.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -48,27 +48,29 @@
 
 (** options for printing **)
 
-val show_brackets_raw = Config.declare_option "show_brackets";
+val show_brackets_raw = Config.declare_option ("show_brackets", @{here});
 val show_brackets = Config.bool show_brackets_raw;
 
-val show_types_raw = Config.declare_option "show_types";
+val show_types_raw = Config.declare_option ("show_types", @{here});
 val show_types = Config.bool show_types_raw;
 
-val show_sorts_raw = Config.declare_option "show_sorts";
+val show_sorts_raw = Config.declare_option ("show_sorts", @{here});
 val show_sorts = Config.bool show_sorts_raw;
 
 val show_markup_default = Unsynchronized.ref false;
-val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
+val show_markup_raw =
+  Config.declare ("show_markup", @{here}) (fn _ => Config.Bool (! show_markup_default));
 val show_markup = Config.bool show_markup_raw;
 
-val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
+val show_structs_raw =
+  Config.declare ("show_structs", @{here}) (fn _ => Config.Bool false);
 val show_structs = Config.bool show_structs_raw;
 
-val show_question_marks_raw = Config.declare_option "show_question_marks";
+val show_question_marks_raw = Config.declare_option ("show_question_marks", @{here});
 val show_question_marks = Config.bool show_question_marks_raw;
 
 val show_type_emphasis =
-  Config.bool (Config.declare "show_type_emphasis" (fn _ => Config.Bool true));
+  Config.bool (Config.declare ("show_type_emphasis", @{here}) (fn _ => Config.Bool true));
 
 fun type_emphasis ctxt T =
   T <> dummyT andalso
@@ -166,7 +168,8 @@
   | is_chain [Arg _] = true
   | is_chain _  = false;
 
-val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0)));
+val pretty_priority =
+  Config.int (Config.declare ("Syntax.pretty_priority", @{here}) (K (Config.Int 0)));
 
 fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
   let

--- a/src/Pure/Syntax/syntax.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -148,12 +148,14 @@
 
 (* configuration options *)
 
-val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
+val root = Config.string (Config.declare ("syntax_root", @{here}) (K (Config.String "any")));
 
-val ambiguity_warning_raw = Config.declare "syntax_ambiguity_warning" (fn _ => Config.Bool true);
+val ambiguity_warning_raw =
+  Config.declare ("syntax_ambiguity_warning", @{here}) (fn _ => Config.Bool true);
 val ambiguity_warning = Config.bool ambiguity_warning_raw;
 
-val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10);
+val ambiguity_limit_raw =
+  Config.declare ("syntax_ambiguity_limit", @{here}) (fn _ => Config.Int 10);
 val ambiguity_limit = Config.int ambiguity_limit_raw;
 
 
@@ -305,7 +307,8 @@
 
 (* global pretty printing *)
 
-val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false)));
+val pretty_global =
+  Config.bool (Config.declare ("Syntax.pretty_global", @{here}) (K (Config.Bool false)));
 fun is_pretty_global ctxt = Config.get ctxt pretty_global;
 val set_pretty_global = Config.put pretty_global;
 val init_pretty_global = set_pretty_global true o Proof_Context.init_global;

--- a/src/Pure/Syntax/syntax_trans.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -295,7 +295,7 @@
       | t' => Abs (a, T, t'))
   | eta_abs t = t;
 
-val eta_contract_raw = Config.declare_option "eta_contract";
+val eta_contract_raw = Config.declare_option ("eta_contract", @{here});
 val eta_contract = Config.bool eta_contract_raw;
 
 fun eta_contr ctxt tm =

--- a/src/Pure/Thy/thy_output.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -43,12 +43,12 @@
 
 (** options **)
 
-val display = Attrib.setup_option_bool "thy_output_display";
-val break = Attrib.setup_option_bool "thy_output_break";
-val quotes = Attrib.setup_option_bool "thy_output_quotes";
-val indent = Attrib.setup_option_int "thy_output_indent";
-val source = Attrib.setup_option_bool "thy_output_source";
-val modes = Attrib.setup_option_string "thy_output_modes";
+val display = Attrib.setup_option_bool ("thy_output_display", @{here});
+val break = Attrib.setup_option_bool ("thy_output_break", @{here});
+val quotes = Attrib.setup_option_bool ("thy_output_quotes", @{here});
+val indent = Attrib.setup_option_int ("thy_output_indent", @{here});
+val source = Attrib.setup_option_bool ("thy_output_source", @{here});
+val modes = Attrib.setup_option_string ("thy_output_modes", @{here});
 
 
 structure Wrappers = Proof_Data

--- a/src/Pure/config.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/config.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -24,11 +24,12 @@
   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 =
@@ -59,11 +60,11 @@
   | 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;
 
@@ -72,13 +73,15 @@
 
 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)};
 
@@ -112,7 +115,7 @@
 
 local
 
-fun declare_generic global name default =
+fun declare_generic global (name, pos) default =
   let
     val id = serial ();
 
@@ -122,7 +125,7 @@
       | 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
@@ -137,9 +140,9 @@
             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 =
@@ -147,8 +150,8 @@
       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
 
@@ -160,6 +163,7 @@
 end;
 
 fun name_of (Config {name, ...}) = name;
+fun pos_of (Config {pos, ...}) = pos;
 
 
 (*final declarations of this structure!*)

--- a/src/Pure/display.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/display.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -35,10 +35,10 @@
 
 val show_consts = Goal_Display.show_consts;
 
-val show_hyps_raw = Config.declare "show_hyps" (fn _ => Config.Bool false);
+val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
 val show_hyps = Config.bool show_hyps_raw;
 
-val show_tags_raw = Config.declare "show_tags" (fn _ => Config.Bool false);
+val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
 val show_tags = Config.bool show_tags_raw;
 
 

--- a/src/Pure/goal_display.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/goal_display.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -23,13 +23,13 @@
 structure Goal_Display: GOAL_DISPLAY =
 struct
 
-val goals_limit_raw = Config.declare_option "goals_limit";
+val goals_limit_raw = Config.declare_option ("goals_limit", @{here});
 val goals_limit = Config.int goals_limit_raw;
 
-val show_main_goal_raw = Config.declare_option "show_main_goal";
+val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
 val show_main_goal = Config.bool show_main_goal_raw;
 
-val show_consts_raw = Config.declare_option "show_consts";
+val show_consts_raw = Config.declare_option ("show_consts", @{here});
 val show_consts = Config.bool show_consts_raw;
 
 fun pretty_flexpair ctxt (t, u) = Pretty.block

--- a/src/Pure/pattern.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/pattern.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -42,7 +42,8 @@
 
 val unify_trace_failure_default = Unsynchronized.ref false;
 val unify_trace_failure_raw =
-  Config.declare_global "unify_trace_failure" (fn _ => Config.Bool (! unify_trace_failure_default));
+  Config.declare_global ("unify_trace_failure", @{here})
+    (fn _ => Config.Bool (! unify_trace_failure_default));
 val unify_trace_failure = Config.bool unify_trace_failure_raw;
 
 fun string_of_term thy env binders t =

--- a/src/Pure/raw_simplifier.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/raw_simplifier.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -394,12 +394,13 @@
 
 (* simp depth *)
 
-val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
+val simp_depth_limit_raw = Config.declare ("simp_depth_limit", @{here}) (K (Config.Int 100));
 val simp_depth_limit = Config.int simp_depth_limit_raw;
 
 val simp_trace_depth_limit_default = Unsynchronized.ref 1;
-val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
-  (fn _ => Config.Int (! simp_trace_depth_limit_default));
+val simp_trace_depth_limit_raw =
+  Config.declare ("simp_trace_depth_limit", @{here})
+    (fn _ => Config.Int (! simp_trace_depth_limit_default));
 val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
 
 fun inc_simp_depth ctxt =
@@ -418,11 +419,12 @@
 
 exception SIMPLIFIER of string * thm list;
 
-val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
+val simp_debug_raw = Config.declare ("simp_debug", @{here}) (K (Config.Bool false));
 val simp_debug = Config.bool simp_debug_raw;
 
 val simp_trace_default = Unsynchronized.ref false;
-val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
+val simp_trace_raw =
+  Config.declare ("simp_trace", @{here}) (fn _ => Config.Bool (! simp_trace_default));
 val simp_trace = Config.bool simp_trace_raw;
 
 fun cond_warning ctxt msg =

--- a/src/Pure/skip_proof.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/skip_proof.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -4,6 +4,9 @@
 Skip proof via oracle invocation.
 *)
 
+val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
+val quick_and_dirty = Config.bool quick_and_dirty_raw;
+
 signature SKIP_PROOF =
 sig
   val report: Proof.context -> unit

--- a/src/Pure/type_infer_context.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/type_infer_context.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -20,7 +20,8 @@
 
 (* constraints *)
 
-val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true)));
+val const_sorts =
+  Config.bool (Config.declare ("const_sorts", @{here}) (K (Config.Bool true)));
 
 fun const_type ctxt =
   try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o

--- a/src/Pure/unify.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/unify.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -34,19 +34,19 @@
 (*Unification options*)
 
 (*tracing starts above this depth, 0 for full*)
-val trace_bound_raw = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
+val trace_bound_raw = Config.declare_global ("unify_trace_bound", @{here}) (K (Config.Int 50));
 val trace_bound = Config.int trace_bound_raw;
 
 (*unification quits above this depth*)
-val search_bound_raw = Config.declare_global "unify_search_bound" (K (Config.Int 60));
+val search_bound_raw = Config.declare_global ("unify_search_bound", @{here}) (K (Config.Int 60));
 val search_bound = Config.int search_bound_raw;
 
 (*print dpairs before calling SIMPL*)
-val trace_simp_raw = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
+val trace_simp_raw = Config.declare_global ("unify_trace_simp", @{here}) (K (Config.Bool false));
 val trace_simp = Config.bool trace_simp_raw;
 
 (*announce potential incompleteness of type unification*)
-val trace_types_raw = Config.declare_global "unify_trace_types" (K (Config.Bool false));
+val trace_types_raw = Config.declare_global ("unify_trace_types", @{here}) (K (Config.Bool false));
 val trace_types = Config.bool trace_types_raw;