src/Pure/Thy/thy_info.ML
changeset 32738 15bb09ca0378
parent 32106 d7697e311d81
child 32794 7b100d30eb32
     1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -50,9 +50,9 @@
     1.4  val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
     1.5  
     1.6  local
     1.7 -  val hooks = ref ([]: (action -> string -> unit) list);
     1.8 +  val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
     1.9  in
    1.10 -  fun add_hook f = CRITICAL (fn () => change hooks (cons f));
    1.11 +  fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
    1.12    fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
    1.13  end;
    1.14  
    1.15 @@ -111,10 +111,10 @@
    1.16  type thy = deps option * theory option;
    1.17  
    1.18  local
    1.19 -  val database = ref (Graph.empty: thy Graph.T);
    1.20 +  val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
    1.21  in
    1.22    fun get_thys () = ! database;
    1.23 -  fun change_thys f = CRITICAL (fn () => Library.change database f);
    1.24 +  fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
    1.25  end;
    1.26  
    1.27