# HG changeset patch
# User wenzelm
# Date 1186151300 -7200
# Node ID 73baca9860873c86c1fdd896bb899d33061b8efc
# Parent  0683a2fc40418118064285eccd1ebc8d8ed42e49
improved check_thy: produce a checked theory_ref (thread-safe version);
removed obsolete self_ref (cf. check_thy);
thread-safeness: when creating certified items, perform Theory.check_thy *last*;
eq_thy: no check here;
marked some critical sections;

diff -r 0683a2fc4041 -r 73baca986087 src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Aug 03 16:28:19 2007 +0200
+++ b/src/Pure/context.ML	Fri Aug 03 16:28:20 2007 +0200
@@ -3,8 +3,8 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Generic theory contexts with unique identity, arbitrarily typed data,
-development graph and history support.  Generic proof contexts with
-arbitrarily typed data.
+monotonic development graph and history support.  Generic proof
+contexts with arbitrarily typed data.
 *)
 
 signature BASIC_CONTEXT =
@@ -33,15 +33,14 @@
   val pprint_thy: theory -> pprint_args -> unit
   val pretty_abbrev_thy: theory -> Pretty.T
   val str_of_thy: theory -> string
-  val check_thy: theory -> theory
+  val deref: theory_ref -> theory
+  val check_thy: theory -> theory_ref
   val eq_thy: theory * theory -> bool
   val thy_ord: theory * theory -> order
   val subthy: theory * theory -> bool
   val joinable: theory * theory -> bool
   val merge: theory * theory -> theory
   val merge_refs: theory_ref * theory_ref -> theory_ref
-  val self_ref: theory -> theory_ref
-  val deref: theory_ref -> theory
   val copy_thy: theory -> theory
   val checkpoint_thy: theory -> theory
   val finish_thy: theory -> theory
@@ -227,11 +226,24 @@
 val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
 
 
-(* consistency *)
+(* theory references *)
+
+(*theory_ref provides a safe way to store dynamic references to a
+  theory in external data structures -- a plain theory value would
+  become stale as the self reference moves on*)
+
+datatype theory_ref = TheoryRef of theory ref;
 
-fun check_thy thy =
-  if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
-  else thy;
+fun deref (TheoryRef (ref thy)) = thy;
+
+fun check_thy thy =  (*thread-safe version*)
+  let val thy_ref = TheoryRef (the_self thy) in
+    if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
+    else thy_ref
+  end;
+
+
+(* consistency *)
 
 fun check_ins id ids =
   if draft_id id orelse Inttab.defined ids (#1 id) then ids
@@ -253,7 +265,7 @@
 
 (* equality and inclusion *)
 
-val eq_thy = eq_id o pairself (#id o identity_of o check_thy);
+val eq_thy = eq_id o pairself (#id o identity_of);
 val thy_ord = int_ord o pairself (#1 o #id o identity_of);
 
 fun proper_subthy
@@ -265,18 +277,6 @@
 fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
 
 
-(* theory references *)
-
-(*theory_ref provides a safe way to store dynamic references to a
-  theory in external data structures -- a plain theory value would
-  become stale as the self reference moves on*)
-
-datatype theory_ref = TheoryRef of theory ref;
-
-val self_ref = TheoryRef o the_self o check_thy;
-fun deref (TheoryRef (ref thy)) = thy;
-
-
 (* trivial merge *)
 
 fun merge (thy1, thy2) =
@@ -289,7 +289,7 @@
 
 fun merge_refs (ref1, ref2) =
   if ref1 = ref2 then ref1
-  else self_ref (merge (deref ref1, deref ref2));
+  else check_thy (merge (deref ref1, deref ref2));
 
 
 
@@ -307,9 +307,10 @@
     val identity' = make_identity self id' ids' iids';
   in vitalize (Theory (identity', data, ancestry, history)) end;
 
-fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) =
+fun change_thy name f thy = NAMED_CRITICAL "theory" (fn () =>
   let
     val _ = check_thy thy;
+    val Theory ({self, id, ids, iids}, data, ancestry, history) = thy;
     val (self', data', ancestry') =
       if is_draft thy then (self, data, ancestry)    (*destructive change!*)
       else if #version history > 0
@@ -317,14 +318,17 @@
       else (NONE, extend_data data,
         make_ancestry [thy] (thy :: #ancestors ancestry));
     val data'' = f data';
-  in create_thy name self' id ids iids data'' ancestry' history end;
+  in create_thy name self' id ids iids data'' ancestry' history end);
 
 fun name_thy name = change_thy name I;
 val modify_thy = change_thy draftN;
 val extend_thy = modify_thy I;
 
-fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) =
-  (check_thy thy; create_thy draftN NONE id ids iids (copy_data data) ancestry history);
+fun copy_thy thy = NAMED_CRITICAL "theory" (fn () =>
+  let
+    val _ = check_thy thy;
+    val Theory ({id, ids, iids, ...}, data, ancestry, history) = thy;
+  in create_thy draftN NONE id ids iids (copy_data data) ancestry history end);
 
 val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
   Datatab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []);
@@ -335,23 +339,25 @@
 fun merge_thys pp (thy1, thy2) =
   if exists_name CPureN thy1 <> exists_name CPureN thy2 then
     error "Cannot merge Pure and CPure developments"
-  else
+  else NAMED_CRITICAL "theory" (fn () =>
     let
+      val _ = check_thy thy1;
+      val _ = check_thy thy2;
       val (ids, iids) = check_merge thy1 thy2;
       val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
       val ancestry = make_ancestry [] [];
       val history = make_history "" 0 [];
-    in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
+    in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end);
 
 fun maximal_thys thys =
   thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
 
 fun begin_thy pp name imports =
   if name = draftN then error ("Illegal theory name: " ^ quote draftN)
-  else
+  else NAMED_CRITICAL "theory" (fn () =>
     let
-      val parents =
-        maximal_thys (distinct eq_thy (map check_thy imports));
+      val _ = map check_thy imports;
+      val parents = maximal_thys (distinct eq_thy imports);
       val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
       val Theory ({id, ids, iids, ...}, data, _, _) =
         (case parents of
@@ -360,31 +366,31 @@
         | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
       val ancestry = make_ancestry parents ancestors;
       val history = make_history name 0 [];
-    in create_thy draftN NONE id ids iids data ancestry history end;
+    in create_thy draftN NONE id ids iids data ancestry history end);
 
 
 (* undoable checkpoints *)
 
 fun checkpoint_thy thy =
   if not (is_draft thy) then thy
-  else
+  else NAMED_CRITICAL "theory" (fn () =>
     let
       val {name, version, intermediates} = history_of thy;
       val thy' as Theory (identity', data', ancestry', _) =
         name_thy (name ^ ":" ^ string_of_int version) thy;
       val history' = make_history name (version + 1) (thy' :: intermediates);
-    in vitalize (Theory (identity', data', ancestry', history')) end;
+    in vitalize (Theory (identity', data', ancestry', history')) end);
 
-fun finish_thy thy =
+fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
   let
     val {name, version, intermediates} = history_of thy;
-    val rs = map (the_self o check_thy) intermediates;
+    val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
     val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
     val identity' = make_identity self id ids Inttab.empty;
     val history' = make_history name 0 [];
     val thy'' = vitalize (Theory (identity', data', ancestry', history'));
     val _ = List.app (fn r => r := thy'') rs;
-  in thy'' end;
+  in thy'' end);
 
 
 (* theory data *)
@@ -435,12 +441,15 @@
 
 in
 
-fun init_proof thy = Proof (self_ref thy, init_data thy);
+fun init_proof thy = Proof (check_thy thy, init_data thy);
 
 fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
-  if not (subthy (deref thy_ref, thy')) then
-    error "transfer proof context: not a super theory"
-  else Proof (self_ref thy', init_new_data data thy');
+  let
+    val thy = deref thy_ref;
+    val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
+    val _ = check_thy thy;
+    val thy_ref' = check_thy thy';
+  in Proof (thy_ref', init_new_data data thy') end;
 
 
 structure ProofData =