equal
deleted
inserted
replaced
126 {pos: Position.T, |
126 {pos: Position.T, |
127 empty: Object.T, |
127 empty: Object.T, |
128 extend: Object.T -> Object.T, |
128 extend: Object.T -> Object.T, |
129 merge: pretty -> Object.T * Object.T -> Object.T}; |
129 merge: pretty -> Object.T * Object.T -> Object.T}; |
130 |
130 |
131 val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table); |
131 val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table); |
132 |
132 |
133 fun invoke name f k x = |
133 fun invoke name f k x = |
134 (case Datatab.lookup (! kinds) k of |
134 (case Datatab.lookup (Synchronized.value kinds) k of |
135 SOME kind => |
135 SOME kind => |
136 if ! timing andalso name <> "" then |
136 if ! timing andalso name <> "" then |
137 Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind)) |
137 Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind)) |
138 (fn () => f kind x) |
138 (fn () => f kind x) |
139 else f kind x |
139 else f kind x |
147 |
147 |
148 fun declare_theory_data pos empty extend merge = |
148 fun declare_theory_data pos empty extend merge = |
149 let |
149 let |
150 val k = serial (); |
150 val k = serial (); |
151 val kind = {pos = pos, empty = empty, extend = extend, merge = merge}; |
151 val kind = {pos = pos, empty = empty, extend = extend, merge = merge}; |
152 val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind))); |
152 val _ = Synchronized.change kinds (Datatab.update (k, kind)); |
153 in k end; |
153 in k end; |
154 |
154 |
155 val extend_data = Datatab.map invoke_extend; |
155 val extend_data = Datatab.map invoke_extend; |
156 fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data; |
156 fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data; |
157 |
157 |
473 |
473 |
474 (* proof data kinds *) |
474 (* proof data kinds *) |
475 |
475 |
476 local |
476 local |
477 |
477 |
478 val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table); |
478 val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Object.T) Datatab.table); |
479 |
479 |
480 fun invoke_init k = |
480 fun invoke_init k = |
481 (case Datatab.lookup (! kinds) k of |
481 (case Datatab.lookup (Synchronized.value kinds) k of |
482 SOME init => init |
482 SOME init => init |
483 | NONE => raise Fail "Invalid proof data identifier"); |
483 | NONE => raise Fail "Invalid proof data identifier"); |
484 |
484 |
485 fun init_data thy = |
485 fun init_data thy = |
486 Datatab.map (fn k => fn _ => invoke_init k thy) (! kinds); |
486 Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds); |
487 |
487 |
488 fun init_new_data data thy = |
488 fun init_new_data data thy = |
489 Datatab.merge (K true) (data, init_data thy); |
489 Datatab.merge (K true) (data, init_data thy); |
490 |
490 |
491 in |
491 in |
509 struct |
509 struct |
510 |
510 |
511 fun declare init = |
511 fun declare init = |
512 let |
512 let |
513 val k = serial (); |
513 val k = serial (); |
514 val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init))); |
514 val _ = Synchronized.change kinds (Datatab.update (k, init)); |
515 in k end; |
515 in k end; |
516 |
516 |
517 fun get k dest prf = |
517 fun get k dest prf = |
518 dest (case Datatab.lookup (data_of_proof prf) k of |
518 dest (case Datatab.lookup (data_of_proof prf) k of |
519 SOME x => x |
519 SOME x => x |