local mutex for theory content/identity operations;
authorwenzelm
Wed Nov 11 00:11:26 2009 +0100 (2009-11-11)
changeset 336062b27020ffcb2
parent 33605 f91ec14e20b6
child 33607 9b3c4e95380e
local mutex for theory content/identity operations;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Wed Nov 11 00:09:15 2009 +0100
     1.2 +++ b/src/Pure/context.ML	Wed Nov 11 00:11:26 2009 +0100
     1.3 @@ -325,6 +325,12 @@
     1.4  
     1.5  (* primitives *)
     1.6  
     1.7 +local
     1.8 +  val lock = Mutex.mutex ();
     1.9 +in
    1.10 +  fun SYNCHRONIZED e = SimpleThread.synchronized "theory" lock e;
    1.11 +end;
    1.12 +
    1.13  fun create_thy self draft ids data ancestry history =
    1.14    let val identity = make_identity self draft (serial ()) ids;
    1.15    in vitalize (Theory (identity, data, ancestry, history)) end;
    1.16 @@ -339,7 +345,7 @@
    1.17        else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
    1.18      val ids' = insert_id draft id ids;
    1.19      val data'' = f data';
    1.20 -    val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.21 +    val thy' = SYNCHRONIZED (fn () =>
    1.22        (check_thy thy; create_thy self' draft' ids' data'' ancestry' history));
    1.23    in thy' end;
    1.24  
    1.25 @@ -352,7 +358,7 @@
    1.26      val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
    1.27      val ids' = insert_id draft id ids;
    1.28      val data' = copy_data data;
    1.29 -    val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.30 +    val thy' = SYNCHRONIZED (fn () =>
    1.31        (check_thy thy; create_thy NONE true ids' data' ancestry history));
    1.32    in thy' end;
    1.33  
    1.34 @@ -368,7 +374,7 @@
    1.35      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
    1.36      val ancestry = make_ancestry [] [];
    1.37      val history = make_history "" 0;
    1.38 -    val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.39 +    val thy' = SYNCHRONIZED (fn () =>
    1.40       (check_thy thy1; check_thy thy2; create_thy NONE true ids data ancestry history));
    1.41    in thy' end;
    1.42  
    1.43 @@ -392,7 +398,7 @@
    1.44  
    1.45        val ancestry = make_ancestry parents ancestors;
    1.46        val history = make_history name 0;
    1.47 -      val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.48 +      val thy' = SYNCHRONIZED (fn () =>
    1.49          (map check_thy imports; create_thy NONE true ids data ancestry history));
    1.50      in thy' end;
    1.51  
    1.52 @@ -405,7 +411,7 @@
    1.53      val _ = stage = finished andalso raise THEORY ("Theory already finished", [thy]);
    1.54      val history' = make_history name (f stage);
    1.55      val thy' as Theory (identity', data', ancestry', _) = name_thy thy;
    1.56 -    val thy'' = NAMED_CRITICAL "theory" (fn () =>
    1.57 +    val thy'' = SYNCHRONIZED (fn () =>
    1.58        (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
    1.59    in thy'' end;
    1.60