1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jul 01 21:57:08 2014 -0700
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 02 08:03:48 2014 +0200
     1.3 @@ -423,7 +423,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.command @{command_spec "context"} "begin local theory context"
     1.6      ((Parse.position Parse.xname >> (fn name =>
     1.7 -        Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
     1.8 +        Toplevel.begin_local_theory true (Named_Target.begin name)) ||
     1.9        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
    1.10          >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
    1.11        --| Parse.begin);

     2.1 --- a/src/Pure/Isar/named_target.ML	Tue Jul 01 21:57:08 2014 -0700
     2.2 +++ b/src/Pure/Isar/named_target.ML	Wed Jul 02 08:03:48 2014 +0200
     2.3 @@ -13,7 +13,10 @@
     2.4    val class_of: local_theory -> string option
     2.5    val init: string -> theory -> local_theory
     2.6    val theory_init: theory -> local_theory
     2.7 -  val context_cmd: xstring * Position.T -> theory -> local_theory
     2.8 +  val begin: xstring * Position.T -> theory -> local_theory
     2.9 +  val exit: local_theory -> theory
    2.10 +  val switch: (xstring * Position.T) option -> Context.generic
    2.11 +    -> (local_theory -> Context.generic) * local_theory
    2.12  end;
    2.13  
    2.14  structure Named_Target: NAMED_TARGET =
    2.15 @@ -164,7 +167,22 @@
    2.16  
    2.17  val theory_init = init "";
    2.18  
    2.19 -fun context_cmd ("-", _) thy = theory_init thy
    2.20 -  | context_cmd target thy = init (Locale.check thy target) thy;
    2.21 +
    2.22 +(* toplevel interaction *)
    2.23 +
    2.24 +fun begin ("-", _) thy = theory_init thy
    2.25 +  | begin target thy = init (Locale.check thy target) thy;
    2.26 +
    2.27 +val exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
    2.28 +
    2.29 +fun switch NONE (Context.Theory thy) =
    2.30 +      (Context.Theory o exit, theory_init thy)
    2.31 +  | switch (SOME name) (Context.Theory thy) =
    2.32 +      (Context.Theory o exit, begin name thy)
    2.33 +  | switch NONE (Context.Proof lthy) =
    2.34 +      (Context.Proof o Local_Theory.restore, lthy)
    2.35 +  | switch (SOME name) (Context.Proof lthy) =
    2.36 +      (Context.Proof o init (the (locale_of lthy)) o exit,
    2.37 +        (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
    2.38  
    2.39  end;

     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 01 21:57:08 2014 -0700
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jul 02 08:03:48 2014 +0200
     3.3 @@ -103,22 +103,6 @@
     3.4  exception UNDEF = Runtime.UNDEF;
     3.5  
     3.6  
     3.7 -(* named target wrappers *)
     3.8 -
     3.9 -val named_init = Named_Target.context_cmd;
    3.10 -val named_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
    3.11 -
    3.12 -fun named_begin NONE (Context.Theory thy) =
    3.13 -      (Context.Theory o named_exit, named_init ("-", Position.none) thy)
    3.14 -  | named_begin (SOME loc) (Context.Theory thy) =
    3.15 -      (Context.Theory o named_exit, named_init loc thy)
    3.16 -  | named_begin NONE (Context.Proof lthy) =
    3.17 -      (Context.Proof o Local_Theory.restore, lthy)
    3.18 -  | named_begin (SOME loc) (Context.Proof lthy) =
    3.19 -      (Context.Proof o Named_Target.init (the (Named_Target.locale_of lthy)) o named_exit,
    3.20 -        (named_init loc o named_exit o Local_Theory.assert_nonbrittle) lthy);
    3.21 -
    3.22 -
    3.23  (* datatype node *)
    3.24  
    3.25  datatype node =
    3.26 @@ -413,7 +397,7 @@
    3.27    (fn Theory (Context.Theory thy, _) =>
    3.28          let
    3.29            val lthy = f thy;
    3.30 -          val gthy = if begin then Context.Proof lthy else Context.Theory (named_exit lthy);
    3.31 +          val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
    3.32            val _ =
    3.33              if begin then
    3.34                Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
    3.35 @@ -422,7 +406,7 @@
    3.36      | _ => raise UNDEF));
    3.37  
    3.38  val end_local_theory = transaction (fn _ =>
    3.39 -  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (named_exit lthy), SOME lthy)
    3.40 +  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (Named_Target.exit lthy), SOME lthy)
    3.41      | _ => raise UNDEF));
    3.42  
    3.43  fun open_target f = transaction (fn _ =>
    3.44 @@ -450,7 +434,7 @@
    3.45  fun local_theory_presentation loc f = present_transaction (fn int =>
    3.46    (fn Theory (gthy, _) =>
    3.47          let
    3.48 -          val (finish, lthy) = named_begin loc gthy;
    3.49 +          val (finish, lthy) = Named_Target.switch loc gthy;
    3.50            val lthy' = lthy
    3.51              |> Local_Theory.new_group
    3.52              |> f int
    3.53 @@ -506,7 +490,7 @@
    3.54  
    3.55  fun local_theory_to_proof' loc f = begin_proof
    3.56    (fn int => fn gthy =>
    3.57 -    let val (finish, lthy) = named_begin loc gthy
    3.58 +    let val (finish, lthy) = Named_Target.switch loc gthy
    3.59      in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
    3.60  
    3.61  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);