tuned CRITICAL sections;
authorwenzelm
Mon Aug 20 23:41:35 2007 +0200 (2007-08-20)
changeset 243690cb1f4d76452
parent 24368 4c2e80f30aeb
child 24370 757b093e3459
tuned CRITICAL sections;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Mon Aug 20 23:35:51 2007 +0200
     1.2 +++ b/src/Pure/context.ML	Mon Aug 20 23:41:35 2007 +0200
     1.3 @@ -307,28 +307,30 @@
     1.4      val identity' = make_identity self id' ids' iids';
     1.5    in vitalize (Theory (identity', data, ancestry, history)) end;
     1.6  
     1.7 -fun change_thy name f thy = NAMED_CRITICAL "theory" (fn () =>
     1.8 +fun change_thy name f thy =
     1.9    let
    1.10 -    val _ = check_thy thy;
    1.11      val Theory ({self, id, ids, iids}, data, ancestry, history) = thy;
    1.12      val (self', data', ancestry') =
    1.13        if is_draft thy then (self, data, ancestry)    (*destructive change!*)
    1.14        else if #version history > 0
    1.15        then (NONE, copy_data data, ancestry)
    1.16 -      else (NONE, extend_data data,
    1.17 -        make_ancestry [thy] (thy :: #ancestors ancestry));
    1.18 +      else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry));
    1.19      val data'' = f data';
    1.20 -  in create_thy name self' id ids iids data'' ancestry' history end);
    1.21 +    val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.22 +      (check_thy thy; create_thy name self' id ids iids data'' ancestry' history));
    1.23 +  in thy' end;
    1.24  
    1.25  fun name_thy name = change_thy name I;
    1.26  val modify_thy = change_thy draftN;
    1.27  val extend_thy = modify_thy I;
    1.28  
    1.29 -fun copy_thy thy = NAMED_CRITICAL "theory" (fn () =>
    1.30 +fun copy_thy thy =
    1.31    let
    1.32 -    val _ = check_thy thy;
    1.33      val Theory ({id, ids, iids, ...}, data, ancestry, history) = thy;
    1.34 -  in create_thy draftN NONE id ids iids (copy_data data) ancestry history end);
    1.35 +    val data' = copy_data data;
    1.36 +    val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.37 +      (check_thy thy; create_thy draftN NONE id ids iids data' ancestry history));
    1.38 +  in thy' end;
    1.39  
    1.40  val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
    1.41    Datatab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []);
    1.42 @@ -339,24 +341,24 @@
    1.43  fun merge_thys pp (thy1, thy2) =
    1.44    if exists_name CPureN thy1 <> exists_name CPureN thy2 then
    1.45      error "Cannot merge Pure and CPure developments"
    1.46 -  else NAMED_CRITICAL "theory" (fn () =>
    1.47 +  else
    1.48      let
    1.49 -      val _ = check_thy thy1;
    1.50 -      val _ = check_thy thy2;
    1.51        val (ids, iids) = check_merge thy1 thy2;
    1.52        val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
    1.53        val ancestry = make_ancestry [] [];
    1.54        val history = make_history "" 0 [];
    1.55 -    in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end);
    1.56 +      val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.57 +       (check_thy thy1; check_thy thy2;
    1.58 +        create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
    1.59 +    in thy' end;
    1.60  
    1.61  fun maximal_thys thys =
    1.62    thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
    1.63  
    1.64  fun begin_thy pp name imports =
    1.65    if name = draftN then error ("Illegal theory name: " ^ quote draftN)
    1.66 -  else NAMED_CRITICAL "theory" (fn () =>
    1.67 +  else
    1.68      let
    1.69 -      val _ = map check_thy imports;
    1.70        val parents = maximal_thys (distinct eq_thy imports);
    1.71        val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
    1.72        val Theory ({id, ids, iids, ...}, data, _, _) =
    1.73 @@ -366,20 +368,24 @@
    1.74          | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
    1.75        val ancestry = make_ancestry parents ancestors;
    1.76        val history = make_history name 0 [];
    1.77 -    in create_thy draftN NONE id ids iids data ancestry history end);
    1.78 +      val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.79 +        (map check_thy imports; create_thy draftN NONE id ids iids data ancestry history));
    1.80 +    in thy' end;
    1.81  
    1.82  
    1.83  (* undoable checkpoints *)
    1.84  
    1.85  fun checkpoint_thy thy =
    1.86    if not (is_draft thy) then thy
    1.87 -  else NAMED_CRITICAL "theory" (fn () =>
    1.88 +  else
    1.89      let
    1.90        val {name, version, intermediates} = history_of thy;
    1.91        val thy' as Theory (identity', data', ancestry', _) =
    1.92          name_thy (name ^ ":" ^ string_of_int version) thy;
    1.93        val history' = make_history name (version + 1) (thy' :: intermediates);
    1.94 -    in vitalize (Theory (identity', data', ancestry', history')) end);
    1.95 +      val thy'' = NAMED_CRITICAL "theory" (fn () =>
    1.96 +        (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
    1.97 +    in thy'' end;
    1.98  
    1.99  fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
   1.100    let