equal
deleted
inserted
replaced
126 |
126 |
127 fun open_target naming operations target = assert target |
127 fun open_target naming operations target = assert target |
128 |> Data.map (cons (make_lthy (naming, operations, target))); |
128 |> Data.map (cons (make_lthy (naming, operations, target))); |
129 |
129 |
130 fun close_target lthy = |
130 fun close_target lthy = |
131 assert_bottom false lthy |> Data.map tl; |
131 assert_bottom false lthy |> Data.map tl |> restore; |
132 |
132 |
133 fun map_contexts f lthy = |
133 fun map_contexts f lthy = |
134 let val n = level lthy in |
134 let val n = level lthy in |
135 lthy |> (Data.map o map_index) (fn (i, {naming, operations, target}) => |
135 lthy |> (Data.map o map_index) (fn (i, {naming, operations, target}) => |
136 make_lthy (naming, operations, |
136 make_lthy (naming, operations, |