src/Pure/General/table.ML
changeset 80591 1d6e5b7a6906
parent 80583 9a40ec7a2027
child 80809 4a64fc4d1cde
equal deleted inserted replaced
80590:505f97165f52 80591:1d6e5b7a6906
   604       | NONE =>
   604       | NONE =>
   605           (case lookup (! cache2) x of
   605           (case lookup (! cache2) x of
   606             SOME exn => Exn.reraise exn
   606             SOME exn => Exn.reraise exn
   607           | NONE =>
   607           | NONE =>
   608               (case Exn.result f x of
   608               (case Exn.result f x of
   609                 Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
   609                 Exn.Res y => (Unsynchronized.change cache1 (default (x, y)); y)
   610               | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))));
   610               | Exn.Exn exn => (Unsynchronized.change cache2 (default (x, exn)); Exn.reraise exn))));
   611     fun reset () = (cache2 := empty; cache1 := empty);
   611     fun reset () = (cache2 := empty; cache1 := empty);
   612     fun total_size () = size (! cache1) + size (! cache2);
   612     fun total_size () = size (! cache1) + size (! cache2);
   613   in {apply = apply, reset = reset, size = total_size} end;
   613   in {apply = apply, reset = reset, size = total_size} end;
   614 
   614 
   615 
   615