structure Datatab: private copy avoids potential conflict of table exceptions;
authorwenzelm
Sun Feb 12 21:34:22 2006 +0100 (2006-02-12)
changeset 190286c238953f66c
parent 19027 adf6fb0db28a
child 19029 8635700e2c9c
structure Datatab: private copy avoids potential conflict of table exceptions;
simplified TableFun.join;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Sun Feb 12 21:34:21 2006 +0100
     1.2 +++ b/src/Pure/context.ML	Sun Feb 12 21:34:22 2006 +0100
     1.3 @@ -112,6 +112,9 @@
     1.4  
     1.5  (* data kinds and access methods *)
     1.6  
     1.7 +(*private copy avoids potential conflict of table exceptions*)
     1.8 +structure Datatab = TableFun(type key = int val ord = int_ord);
     1.9 +
    1.10  local
    1.11  
    1.12  type kind =
    1.13 @@ -121,10 +124,10 @@
    1.14    extend: Object.T -> Object.T,
    1.15    merge: Pretty.pp -> Object.T * Object.T -> Object.T};
    1.16  
    1.17 -val kinds = ref (Inttab.empty: kind Inttab.table);
    1.18 +val kinds = ref (Datatab.empty: kind Datatab.table);
    1.19  
    1.20  fun invoke meth_name meth_fn k =
    1.21 -  (case Inttab.lookup (! kinds) k of
    1.22 +  (case Datatab.lookup (! kinds) k of
    1.23      SOME kind => meth_fn kind |> transform_failure (fn exn =>
    1.24        EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
    1.25    | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
    1.26 @@ -141,14 +144,14 @@
    1.27    let
    1.28      val k = serial ();
    1.29      val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
    1.30 -    val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
    1.31 +    val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
    1.32        warning ("Duplicate declaration of theory data " ^ quote name));
    1.33 -    val _ = change kinds (Inttab.update (k, kind));
    1.34 +    val _ = change kinds (Datatab.update (k, kind));
    1.35    in k end;
    1.36  
    1.37 -val copy_data = Inttab.map' invoke_copy;
    1.38 -val extend_data = Inttab.map' invoke_extend;
    1.39 -fun merge_data pp = Inttab.join (SOME oo invoke_merge pp) o pairself extend_data;
    1.40 +val copy_data = Datatab.map' invoke_copy;
    1.41 +val extend_data = Datatab.map' invoke_extend;
    1.42 +fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
    1.43  
    1.44  end;
    1.45  
    1.46 @@ -164,8 +167,8 @@
    1.47      ids: string Inttab.table,           (*identifiers of ancestors*)
    1.48      iids: string Inttab.table} *        (*identifiers of intermediate checkpoints*)
    1.49     (*data*)
    1.50 -   {theory: Object.T Inttab.table,      (*theory data record*)
    1.51 -    proof: unit Inttab.table} *         (*proof data kinds*)
    1.52 +   {theory: Object.T Datatab.table,     (*theory data record*)
    1.53 +    proof: unit Datatab.table} *        (*proof data kinds*)
    1.54     (*ancestry*)
    1.55     {parents: theory list,               (*immediate predecessors*)
    1.56      ancestors: theory list} *           (*all predecessors*)
    1.57 @@ -349,7 +352,7 @@
    1.58      create_thy draftN NONE id ids iids (map_theory_data copy_data data) ancestry history);
    1.59  
    1.60  val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
    1.61 -  (make_data Inttab.empty Inttab.empty) (make_ancestry [] []) (make_history ProtoPureN 0 []);
    1.62 +  (make_data Datatab.empty Datatab.empty) (make_ancestry [] []) (make_history ProtoPureN 0 []);
    1.63  
    1.64  
    1.65  (* named theory nodes *)
    1.66 @@ -363,7 +366,7 @@
    1.67        val data1 = data_of thy1 and data2 = data_of thy2;
    1.68        val data = make_data
    1.69          (merge_data (pp thy1) (#theory data1, #theory data2))
    1.70 -        (Inttab.merge (K true) (#proof data1, #proof data2));
    1.71 +        (Datatab.merge (K true) (#proof data1, #proof data2));
    1.72        val ancestry = make_ancestry [] [];
    1.73        val history = make_history "" 0 [];
    1.74      in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
    1.75 @@ -415,7 +418,7 @@
    1.76  (* theory data *)
    1.77  
    1.78  fun dest_data name_of tab =
    1.79 -  map name_of (Inttab.keys tab)
    1.80 +  map name_of (Datatab.keys tab)
    1.81    |> map (rpair ()) |> Symtab.make_list |> Symtab.dest
    1.82    |> map (apsnd length)
    1.83    |> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n));
    1.84 @@ -428,12 +431,12 @@
    1.85  val declare = declare_theory_data;
    1.86  
    1.87  fun get k dest thy =
    1.88 -  (case Inttab.lookup (#theory (data_of thy)) k of
    1.89 +  (case Datatab.lookup (#theory (data_of thy)) k of
    1.90      SOME x => (dest x handle Match =>
    1.91        error ("Failed to access theory data " ^ quote (invoke_name k)))
    1.92    | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
    1.93  
    1.94 -fun put k mk x = modify_thy (map_theory_data (Inttab.update (k, mk x)));
    1.95 +fun put k mk x = modify_thy (map_theory_data (Datatab.update (k, mk x)));
    1.96  fun init k = put k I (invoke_empty k);
    1.97  
    1.98  end;
    1.99 @@ -506,7 +509,7 @@
   1.100  
   1.101  (* datatype proof *)
   1.102  
   1.103 -datatype proof = Proof of theory_ref * Object.T Inttab.table;
   1.104 +datatype proof = Proof of theory_ref * Object.T Datatab.table;
   1.105  
   1.106  fun theory_of_proof (Proof (thy_ref, _)) = deref thy_ref;
   1.107  fun data_of_proof (Proof (_, data)) = data;
   1.108 @@ -526,10 +529,10 @@
   1.109   {name: string,
   1.110    init: theory -> Object.T};
   1.111  
   1.112 -val kinds = ref (Inttab.empty: kind Inttab.table);
   1.113 +val kinds = ref (Datatab.empty: kind Datatab.table);
   1.114  
   1.115  fun invoke meth_name meth_fn k =
   1.116 -  (case Inttab.lookup (! kinds) k of
   1.117 +  (case Datatab.lookup (! kinds) k of
   1.118      SOME kind => meth_fn kind |> transform_failure (fn exn =>
   1.119        EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   1.120    | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
   1.121 @@ -542,7 +545,7 @@
   1.122  val proof_data_of = dest_data invoke_name o #proof o data_of;
   1.123  
   1.124  fun init_proof thy =
   1.125 -  Proof (self_ref thy, Inttab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
   1.126 +  Proof (self_ref thy, Datatab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
   1.127  
   1.128  structure ProofData =
   1.129  struct
   1.130 @@ -551,20 +554,20 @@
   1.131    let
   1.132      val k = serial ();
   1.133      val kind = {name = name, init = init};
   1.134 -    val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   1.135 +    val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   1.136        warning ("Duplicate declaration of proof data " ^ quote name));
   1.137 -    val _ = change kinds (Inttab.update (k, kind));
   1.138 +    val _ = change kinds (Datatab.update (k, kind));
   1.139    in k end;
   1.140  
   1.141 -fun init k = modify_thy (map_proof_data (Inttab.update (k, ())));
   1.142 +fun init k = modify_thy (map_proof_data (Datatab.update (k, ())));
   1.143  
   1.144  fun get k dest prf =
   1.145 -  (case Inttab.lookup (data_of_proof prf) k of
   1.146 +  (case Datatab.lookup (data_of_proof prf) k of
   1.147      SOME x => (dest x handle Match =>
   1.148        error ("Failed to access proof data " ^ quote (invoke_name k)))
   1.149    | NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
   1.150  
   1.151 -fun put k mk x = map_prf (Inttab.update (k, mk x));
   1.152 +fun put k mk x = map_prf (Datatab.update (k, mk x));
   1.153  
   1.154  end;
   1.155