equal
deleted
inserted
replaced
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 |