src/Pure/General/file.ML
changeset 32738 15bb09ca0378
parent 31818 f698f76a3713
child 32943 2cb928848e77
     1.1 --- a/src/Pure/General/file.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/General/file.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -85,7 +85,8 @@
     1.4  (* file identification *)
     1.5  
     1.6  local
     1.7 -  val ident_cache = ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
     1.8 +  val ident_cache =
     1.9 +    Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
    1.10  in
    1.11  
    1.12  fun check_cache (path, time) = CRITICAL (fn () =>
    1.13 @@ -94,7 +95,8 @@
    1.14    | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
    1.15  
    1.16  fun update_cache (path, (time, id)) = CRITICAL (fn () =>
    1.17 -  change ident_cache (Symtab.update (path, {time_stamp = time, id = id})));
    1.18 +  Unsynchronized.change ident_cache
    1.19 +    (Symtab.update (path, {time_stamp = time, id = id})));
    1.20  
    1.21  end;
    1.22