src/Pure/context.ML
changeset 32738 15bb09ca0378
parent 31971 8c1b845ed105
child 32784 1a5dde5079ac
     1.1 --- a/src/Pure/context.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/context.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4    extend: Object.T -> Object.T,
     1.5    merge: Pretty.pp -> Object.T * Object.T -> Object.T};
     1.6  
     1.7 -val kinds = ref (Datatab.empty: kind Datatab.table);
     1.8 +val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
     1.9  
    1.10  fun invoke f k =
    1.11    (case Datatab.lookup (! kinds) k of
    1.12 @@ -125,7 +125,7 @@
    1.13    let
    1.14      val k = serial ();
    1.15      val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
    1.16 -    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
    1.17 +    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    1.18    in k end;
    1.19  
    1.20  val copy_data = Datatab.map' invoke_copy;
    1.21 @@ -149,7 +149,7 @@
    1.22  datatype theory =
    1.23    Theory of
    1.24     (*identity*)
    1.25 -   {self: theory ref option,      (*dynamic self reference -- follows theory changes*)
    1.26 +   {self: theory Unsynchronized.ref option,  (*dynamic self reference -- follows theory changes*)
    1.27      draft: bool,                  (*draft mode -- linear destructive changes*)
    1.28      id: serial,                   (*identifier*)
    1.29      ids: unit Inttab.table} *     (*cumulative identifiers of non-drafts -- symbolic body content*)
    1.30 @@ -186,14 +186,15 @@
    1.31  fun eq_id (i: int, j) = i = j;
    1.32  
    1.33  fun is_stale
    1.34 -    (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
    1.35 +    (Theory ({self =
    1.36 +        SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
    1.37        not (eq_id (id, id'))
    1.38    | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
    1.39  
    1.40  fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
    1.41    | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
    1.42        let
    1.43 -        val r = ref thy;
    1.44 +        val r = Unsynchronized.ref thy;
    1.45          val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
    1.46        in r := thy'; thy' end;
    1.47  
    1.48 @@ -243,9 +244,9 @@
    1.49    theory in external data structures -- a plain theory value would
    1.50    become stale as the self reference moves on*)
    1.51  
    1.52 -datatype theory_ref = TheoryRef of theory ref;
    1.53 +datatype theory_ref = TheoryRef of theory Unsynchronized.ref;
    1.54  
    1.55 -fun deref (TheoryRef (ref thy)) = thy;
    1.56 +fun deref (TheoryRef (Unsynchronized.ref thy)) = thy;
    1.57  
    1.58  fun check_thy thy =  (*thread-safe version*)
    1.59    let val thy_ref = TheoryRef (the_self thy) in
    1.60 @@ -437,7 +438,7 @@
    1.61  
    1.62  local
    1.63  
    1.64 -val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
    1.65 +val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
    1.66  
    1.67  fun invoke_init k =
    1.68    (case Datatab.lookup (! kinds) k of
    1.69 @@ -470,7 +471,7 @@
    1.70  fun declare init =
    1.71    let
    1.72      val k = serial ();
    1.73 -    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
    1.74 +    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
    1.75    in k end;
    1.76  
    1.77  fun get k dest prf =