equal
deleted
inserted
replaced
105 fun cache expr = |
105 fun cache expr = |
106 Cache {expr = expr, var = var "Synchronized.cache" NONE}; |
106 Cache {expr = expr, var = var "Synchronized.cache" NONE}; |
107 |
107 |
108 fun cache_eval (Cache {expr, var}) = |
108 fun cache_eval (Cache {expr, var}) = |
109 change_result var (fn state => |
109 change_result var (fn state => |
110 (case state of |
110 (case Option.mapPartial Unsynchronized.weak_peek state of |
111 SOME (Unsynchronized.ref (SOME (Unsynchronized.ref result))) => (result, state) |
111 SOME result => (result, state) |
112 | _ => |
112 | NONE => |
113 let val result = expr () |
113 let val result = expr () |
114 in (result, SOME (Unsynchronized.weak_ref result)) end)); |
114 in (result, SOME (Unsynchronized.weak_ref result)) end)); |
115 |
115 |
116 end; |
116 end; |
117 |
117 |
118 end; |
118 end; |