src/Pure/context.ML
changeset 42818 128cc195ced3
parent 42383 0ae4ad40d7b5
child 43610 16482dc641d4
     1.1 --- a/src/Pure/context.ML	Sun May 15 19:19:26 2011 +0200
     1.2 +++ b/src/Pure/context.ML	Sun May 15 20:38:08 2011 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4  sig
     1.5    include BASIC_CONTEXT
     1.6    (*theory context*)
     1.7 +  val timing: bool Unsynchronized.ref
     1.8    type pretty
     1.9    val parents_of: theory -> theory list
    1.10    val ancestors_of: theory -> theory list
    1.11 @@ -90,7 +91,7 @@
    1.12    include CONTEXT
    1.13    structure Theory_Data:
    1.14    sig
    1.15 -    val declare: Object.T -> (Object.T -> Object.T) ->
    1.16 +    val declare: Position.T -> Object.T -> (Object.T -> Object.T) ->
    1.17        (pretty -> Object.T * Object.T -> Object.T) -> serial
    1.18      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    1.19      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    1.20 @@ -112,6 +113,8 @@
    1.21  
    1.22  (* data kinds and access methods *)
    1.23  
    1.24 +val timing = Unsynchronized.ref false;
    1.25 +
    1.26  (*private copy avoids potential conflict of table exceptions*)
    1.27  structure Datatab = Table(type key = int val ord = int_ord);
    1.28  
    1.29 @@ -120,27 +123,32 @@
    1.30  local
    1.31  
    1.32  type kind =
    1.33 - {empty: Object.T,
    1.34 + {pos: Position.T,
    1.35 +  empty: Object.T,
    1.36    extend: Object.T -> Object.T,
    1.37    merge: pretty -> Object.T * Object.T -> Object.T};
    1.38  
    1.39  val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
    1.40  
    1.41 -fun invoke f k =
    1.42 +fun invoke name f k x =
    1.43    (case Datatab.lookup (! kinds) k of
    1.44 -    SOME kind => f kind
    1.45 +    SOME kind =>
    1.46 +      if ! timing andalso name <> "" then
    1.47 +        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind))
    1.48 +          (fn () => f kind x)
    1.49 +      else f kind x
    1.50    | NONE => raise Fail "Invalid theory data identifier");
    1.51  
    1.52  in
    1.53  
    1.54 -fun invoke_empty k = invoke (K o #empty) k ();
    1.55 -val invoke_extend = invoke #extend;
    1.56 -fun invoke_merge pp = invoke (fn kind => #merge kind pp);
    1.57 +fun invoke_empty k = invoke "" (K o #empty) k ();
    1.58 +val invoke_extend = invoke "extend" #extend;
    1.59 +fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
    1.60  
    1.61 -fun declare_theory_data empty extend merge =
    1.62 +fun declare_theory_data pos empty extend merge =
    1.63    let
    1.64      val k = serial ();
    1.65 -    val kind = {empty = empty, extend = extend, merge = merge};
    1.66 +    val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
    1.67      val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    1.68    in k end;
    1.69  
    1.70 @@ -635,10 +643,12 @@
    1.71  type T = Data.T;
    1.72  exception Data of T;
    1.73  
    1.74 -val kind = Context.Theory_Data.declare
    1.75 -  (Data Data.empty)
    1.76 -  (fn Data x => Data (Data.extend x))
    1.77 -  (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
    1.78 +val kind =
    1.79 +  Context.Theory_Data.declare
    1.80 +    (Position.thread_data ())
    1.81 +    (Data Data.empty)
    1.82 +    (fn Data x => Data (Data.extend x))
    1.83 +    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
    1.84  
    1.85  val get = Context.Theory_Data.get kind (fn Data x => x);
    1.86  val put = Context.Theory_Data.put kind Data;