equal
deleted
inserted
replaced
245 |
245 |
246 local |
246 local |
247 |
247 |
248 type kind = { empty: Object.T }; |
248 type kind = { empty: Object.T }; |
249 |
249 |
250 val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table); |
250 val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table); |
251 |
251 |
252 fun invoke f k = case Datatab.lookup (! kinds) k |
252 fun invoke f k = |
253 of SOME kind => f kind |
253 (case Datatab.lookup (Synchronized.value kinds) k of |
254 | NONE => raise Fail "Invalid code data identifier"; |
254 SOME kind => f kind |
|
255 | NONE => raise Fail "Invalid code data identifier"); |
255 |
256 |
256 in |
257 in |
257 |
258 |
258 fun declare_data empty = |
259 fun declare_data empty = |
259 let |
260 let |
260 val k = serial (); |
261 val k = serial (); |
261 val kind = { empty = empty }; |
262 val kind = { empty = empty }; |
262 val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind))); |
263 val _ = Synchronized.change kinds (Datatab.update (k, kind)); |
263 in k end; |
264 in k end; |
264 |
265 |
265 fun invoke_init k = invoke (fn kind => #empty kind) k; |
266 fun invoke_init k = invoke (fn kind => #empty kind) k; |
266 |
267 |
267 end; (*local*) |
268 end; (*local*) |