49 val theory: (theory -> theory) -> transition -> transition |
49 val theory: (theory -> theory) -> transition -> transition |
50 val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition |
50 val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition |
51 val end_local_theory: transition -> transition |
51 val end_local_theory: transition -> transition |
52 val open_target: (generic_theory -> local_theory) -> transition -> transition |
52 val open_target: (generic_theory -> local_theory) -> transition -> transition |
53 val close_target: transition -> transition |
53 val close_target: transition -> transition |
54 val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) -> |
54 val local_theory': Position.T option -> (xstring * Position.T) option -> |
55 transition -> transition |
55 (bool -> local_theory -> local_theory) -> transition -> transition |
56 val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) -> |
56 val local_theory: Position.T option -> (xstring * Position.T) option -> |
57 transition -> transition |
57 (local_theory -> local_theory) -> transition -> transition |
58 val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> |
58 val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> |
59 transition -> transition |
59 transition -> transition |
60 val local_theory_to_proof': (xstring * Position.T) option -> |
60 val local_theory_to_proof': Position.T option -> (xstring * Position.T) option -> |
61 (bool -> local_theory -> Proof.state) -> transition -> transition |
61 (bool -> local_theory -> Proof.state) -> transition -> transition |
62 val local_theory_to_proof: (xstring * Position.T) option -> |
62 val local_theory_to_proof: Position.T option -> (xstring * Position.T) option -> |
63 (local_theory -> Proof.state) -> transition -> transition |
63 (local_theory -> Proof.state) -> transition -> transition |
64 val theory_to_proof: (theory -> Proof.state) -> transition -> transition |
64 val theory_to_proof: (theory -> Proof.state) -> transition -> transition |
65 val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition |
65 val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition |
66 val forget_proof: bool -> transition -> transition |
66 val forget_proof: bool -> transition -> transition |
67 val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition |
67 val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition |
410 else Context.Theory (Proof_Context.theory_of ctxt'); |
410 else Context.Theory (Proof_Context.theory_of ctxt'); |
411 in Theory (gthy', SOME lthy) end |
411 in Theory (gthy', SOME lthy) end |
412 | NONE => raise UNDEF) |
412 | NONE => raise UNDEF) |
413 | _ => raise UNDEF)); |
413 | _ => raise UNDEF)); |
414 |
414 |
415 fun local_theory' loc f = present_transaction (fn int => |
415 fun local_theory' private target f = present_transaction (fn int => |
416 (fn Theory (gthy, _) => |
416 (fn Theory (gthy, _) => |
417 let |
417 let |
418 val (finish, lthy) = Named_Target.switch loc gthy; |
418 val (finish, lthy) = Named_Target.switch target gthy; |
419 val lthy' = lthy |
419 val lthy' = lthy |
|
420 |> fold Proof_Context.private (the_list private) |
420 |> Local_Theory.new_group |
421 |> Local_Theory.new_group |
421 |> f int |
422 |> f int |
422 |> Local_Theory.reset_group; |
423 |> Local_Theory.reset_group; |
423 in Theory (finish lthy', SOME lthy') end |
424 in Theory (finish lthy', SOME lthy') end |
424 | _ => raise UNDEF)) |
425 | _ => raise UNDEF)) |
425 (K ()); |
426 (K ()); |
426 |
427 |
427 fun local_theory loc f = local_theory' loc (K f); |
428 fun local_theory private target f = local_theory' private target (K f); |
428 |
429 |
429 fun present_local_theory loc = present_transaction (fn int => |
430 fun present_local_theory target = present_transaction (fn int => |
430 (fn Theory (gthy, _) => |
431 (fn Theory (gthy, _) => |
431 let val (finish, lthy) = Named_Target.switch loc gthy; |
432 let val (finish, lthy) = Named_Target.switch target gthy; |
432 in Theory (finish lthy, SOME lthy) end |
433 in Theory (finish lthy, SOME lthy) end |
433 | _ => raise UNDEF)); |
434 | _ => raise UNDEF)); |
434 |
435 |
435 |
436 |
436 (* proof transitions *) |
437 (* proof transitions *) |
467 end |
468 end |
468 | _ => raise UNDEF)); |
469 | _ => raise UNDEF)); |
469 |
470 |
470 in |
471 in |
471 |
472 |
472 fun local_theory_to_proof' loc f = begin_proof |
473 fun local_theory_to_proof' private target f = begin_proof |
473 (fn int => fn gthy => |
474 (fn int => fn gthy => |
474 let val (finish, lthy) = Named_Target.switch loc gthy |
475 let |
475 in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end); |
476 val (finish, lthy) = Named_Target.switch target gthy; |
476 |
477 val prf = lthy |
477 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); |
478 |> fold Proof_Context.private (the_list private) |
|
479 |> Local_Theory.new_group |
|
480 |> f int; |
|
481 in (finish o Local_Theory.reset_group, prf) end); |
|
482 |
|
483 fun local_theory_to_proof private target f = |
|
484 local_theory_to_proof' private target (K f); |
478 |
485 |
479 fun theory_to_proof f = begin_proof |
486 fun theory_to_proof f = begin_proof |
480 (fn _ => fn gthy => |
487 (fn _ => fn gthy => |
481 (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of, |
488 (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of, |
482 (case gthy of |
489 (case gthy of |