73 val exit_global: local_theory -> theory |
73 val exit_global: local_theory -> theory |
74 val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context |
74 val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context |
75 val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory |
75 val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory |
76 val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} -> |
76 val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} -> |
77 operations -> local_theory -> Binding.scope * local_theory |
77 operations -> local_theory -> Binding.scope * local_theory |
78 val open_target: local_theory -> Binding.scope * local_theory |
78 val begin_target: local_theory -> Binding.scope * local_theory |
|
79 val open_target: local_theory -> local_theory |
79 val close_target: local_theory -> local_theory |
80 val close_target: local_theory -> local_theory |
80 val subtarget: (local_theory -> local_theory) -> local_theory -> local_theory |
81 val subtarget: (local_theory -> local_theory) -> local_theory -> local_theory |
81 val subtarget_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> |
82 val subtarget_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> |
82 local_theory -> 'b * local_theory |
83 local_theory -> 'b * local_theory |
83 end; |
84 end; |
391 val (scope, target) = Proof_Context.new_scope lthy; |
392 val (scope, target) = Proof_Context.new_scope lthy; |
392 val entry = make_lthy (background_naming, operations, after_close', exit_of lthy, true, target); |
393 val entry = make_lthy (background_naming, operations, after_close', exit_of lthy, true, target); |
393 val lthy' = Data.map (cons entry) target; |
394 val lthy' = Data.map (cons entry) target; |
394 in (scope, lthy') end; |
395 in (scope, lthy') end; |
395 |
396 |
396 fun open_target lthy = |
397 fun begin_target lthy = |
397 init_target {background_naming = background_naming_of lthy, after_close = I} |
398 init_target {background_naming = background_naming_of lthy, after_close = I} |
398 (operations_of lthy) lthy; |
399 (operations_of lthy) lthy; |
|
400 |
|
401 val open_target = begin_target #> #2; |
399 |
402 |
400 fun close_target lthy = |
403 fun close_target lthy = |
401 let |
404 let |
402 val _ = assert_not_bottom lthy; |
405 val _ = assert_not_bottom lthy; |
403 val ({after_close, ...} :: rest) = Data.get lthy; |
406 val ({after_close, ...} :: rest) = Data.get lthy; |
404 in lthy |> Data.put rest |> reset |> after_close end; |
407 in lthy |> Data.put rest |> reset |> after_close end; |
405 |
408 |
406 fun subtarget body = open_target #> #2 #> body #> close_target; |
409 fun subtarget body = open_target #> body #> close_target; |
407 |
410 |
408 fun subtarget_result decl body lthy = |
411 fun subtarget_result decl body lthy = |
409 let |
412 let |
410 val (x, inner_lthy) = lthy |> open_target |> #2 |> body; |
413 val (x, inner_lthy) = lthy |> open_target |> body; |
411 val lthy' = inner_lthy |> close_target; |
414 val lthy' = inner_lthy |> close_target; |
412 val phi = Proof_Context.export_morphism inner_lthy lthy'; |
415 val phi = Proof_Context.export_morphism inner_lthy lthy'; |
413 in (decl phi x, lthy') end; |
416 in (decl phi x, lthy') end; |
414 |
417 |
415 end; |
418 end; |