1.1 --- a/src/Pure/General/position.ML	Sun May 15 19:19:26 2011 +0200
     1.2 +++ b/src/Pure/General/position.ML	Sun May 15 20:38:08 2011 +0200
     1.3 @@ -177,6 +177,7 @@
     1.4        (case (line_of pos, file_of pos) of
     1.5          (SOME i, NONE) => "(line " ^ string_of_int i ^ ")"
     1.6        | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")"
     1.7 +      | (NONE, SOME name) => "(" ^ quote name ^ ")"
     1.8        | _ => "");
     1.9    in
    1.10      if null props then ""

     2.1 --- a/src/Pure/General/secure.ML	Sun May 15 19:19:26 2011 +0200
     2.2 +++ b/src/Pure/General/secure.ML	Sun May 15 20:38:08 2011 +0200
     2.3 @@ -61,7 +61,12 @@
     2.4  (*override previous toplevel bindings!*)
     2.5  val use_text = Secure.use_text;
     2.6  val use_file = Secure.use_file;
     2.7 -fun use s = Secure.use_file ML_Parse.global_context true s
     2.8 -  handle ERROR msg => (writeln msg; error "ML error");
     2.9 +
    2.10 +fun use s =
    2.11 +  Position.setmp_thread_data (Position.of_properties (Position.file_name s))
    2.12 +    (fn () =>
    2.13 +      Secure.use_file ML_Parse.global_context true s
    2.14 +        handle ERROR msg => (writeln msg; error "ML error")) ();
    2.15 +
    2.16  val toplevel_pp = Secure.toplevel_pp;
    2.17  

     3.1 --- a/src/Pure/context.ML	Sun May 15 19:19:26 2011 +0200
     3.2 +++ b/src/Pure/context.ML	Sun May 15 20:38:08 2011 +0200
     3.3 @@ -28,6 +28,7 @@
     3.4  sig
     3.5    include BASIC_CONTEXT
     3.6    (*theory context*)
     3.7 +  val timing: bool Unsynchronized.ref
     3.8    type pretty
     3.9    val parents_of: theory -> theory list
    3.10    val ancestors_of: theory -> theory list
    3.11 @@ -90,7 +91,7 @@
    3.12    include CONTEXT
    3.13    structure Theory_Data:
    3.14    sig
    3.15 -    val declare: Object.T -> (Object.T -> Object.T) ->
    3.16 +    val declare: Position.T -> Object.T -> (Object.T -> Object.T) ->
    3.17        (pretty -> Object.T * Object.T -> Object.T) -> serial
    3.18      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    3.19      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    3.20 @@ -112,6 +113,8 @@
    3.21  
    3.22  (* data kinds and access methods *)
    3.23  
    3.24 +val timing = Unsynchronized.ref false;
    3.25 +
    3.26  (*private copy avoids potential conflict of table exceptions*)
    3.27  structure Datatab = Table(type key = int val ord = int_ord);
    3.28  
    3.29 @@ -120,27 +123,32 @@
    3.30  local
    3.31  
    3.32  type kind =
    3.33 - {empty: Object.T,
    3.34 + {pos: Position.T,
    3.35 +  empty: Object.T,
    3.36    extend: Object.T -> Object.T,
    3.37    merge: pretty -> Object.T * Object.T -> Object.T};
    3.38  
    3.39  val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
    3.40  
    3.41 -fun invoke f k =
    3.42 +fun invoke name f k x =
    3.43    (case Datatab.lookup (! kinds) k of
    3.44 -    SOME kind => f kind
    3.45 +    SOME kind =>
    3.46 +      if ! timing andalso name <> "" then
    3.47 +        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind))
    3.48 +          (fn () => f kind x)
    3.49 +      else f kind x
    3.50    | NONE => raise Fail "Invalid theory data identifier");
    3.51  
    3.52  in
    3.53  
    3.54 -fun invoke_empty k = invoke (K o #empty) k ();
    3.55 -val invoke_extend = invoke #extend;
    3.56 -fun invoke_merge pp = invoke (fn kind => #merge kind pp);
    3.57 +fun invoke_empty k = invoke "" (K o #empty) k ();
    3.58 +val invoke_extend = invoke "extend" #extend;
    3.59 +fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
    3.60  
    3.61 -fun declare_theory_data empty extend merge =
    3.62 +fun declare_theory_data pos empty extend merge =
    3.63    let
    3.64      val k = serial ();
    3.65 -    val kind = {empty = empty, extend = extend, merge = merge};
    3.66 +    val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
    3.67      val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    3.68    in k end;
    3.69  
    3.70 @@ -635,10 +643,12 @@
    3.71  type T = Data.T;
    3.72  exception Data of T;
    3.73  
    3.74 -val kind = Context.Theory_Data.declare
    3.75 -  (Data Data.empty)
    3.76 -  (fn Data x => Data (Data.extend x))
    3.77 -  (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
    3.78 +val kind =
    3.79 +  Context.Theory_Data.declare
    3.80 +    (Position.thread_data ())
    3.81 +    (Data Data.empty)
    3.82 +    (fn Data x => Data (Data.extend x))
    3.83 +    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
    3.84  
    3.85  val get = Context.Theory_Data.get kind (fn Data x => x);
    3.86  val put = Context.Theory_Data.put kind Data;