src/Pure/Isar/toplevel.ML
changeset 47069 451fc10a81f3
parent 46959 cdc791910460
child 47274 feef9b0b6031
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 21 21:24:13 2012 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 21 23:26:35 2012 +0100
     1.3 @@ -58,6 +58,8 @@
     1.4    val theory': (bool -> theory -> theory) -> transition -> transition
     1.5    val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
     1.6    val end_local_theory: transition -> transition
     1.7 +  val open_target: (generic_theory -> local_theory) -> transition -> transition
     1.8 +  val close_target: transition -> transition
     1.9    val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
    1.10      transition -> transition
    1.11    val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
    1.12 @@ -105,7 +107,7 @@
    1.13  (* local theory wrappers *)
    1.14  
    1.15  val loc_init = Named_Target.context_cmd;
    1.16 -val loc_exit = Local_Theory.exit_global;
    1.17 +val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
    1.18  
    1.19  fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
    1.20    | loc_begin NONE (Context.Proof lthy) = lthy
    1.21 @@ -456,6 +458,20 @@
    1.22    (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
    1.23      | _ => raise UNDEF));
    1.24  
    1.25 +fun open_target f = transaction (fn _ =>
    1.26 +  (fn Theory (gthy, _) =>
    1.27 +        let val lthy = f gthy
    1.28 +        in Theory (Context.Proof lthy, SOME lthy) end
    1.29 +    | _ => raise UNDEF));
    1.30 +
    1.31 +val close_target = transaction (fn _ =>
    1.32 +  (fn Theory (Context.Proof lthy, _) =>
    1.33 +        (case try Local_Theory.close_target lthy of
    1.34 +          SOME lthy' => Theory (Context.Proof lthy', SOME lthy)
    1.35 +        | NONE => raise UNDEF)
    1.36 +    | _ => raise UNDEF));
    1.37 +
    1.38 +
    1.39  local
    1.40  
    1.41  fun local_theory_presentation loc f = present_transaction (fn int =>