centralized (ad-hoc) switching of targets in named_target.ML

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

--- a/src/Pure/Isar/named_target.ML	Tue Jul 01 21:57:08 2014 -0700
+++ b/src/Pure/Isar/named_target.ML	Wed Jul 02 08:03:48 2014 +0200
@@ -13,7 +13,10 @@
   val class_of: local_theory -> string option
   val init: string -> theory -> local_theory
   val theory_init: theory -> local_theory
-  val context_cmd: xstring * Position.T -> theory -> local_theory
+  val begin: xstring * Position.T -> theory -> local_theory
+  val exit: local_theory -> theory
+  val switch: (xstring * Position.T) option -> Context.generic
+    -> (local_theory -> Context.generic) * local_theory
 end;
 
 structure Named_Target: NAMED_TARGET =
@@ -164,7 +167,22 @@
 
 val theory_init = init "";
 
-fun context_cmd ("-", _) thy = theory_init thy
-  | context_cmd target thy = init (Locale.check thy target) thy;
+
+(* toplevel interaction *)
+
+fun begin ("-", _) thy = theory_init thy
+  | begin target thy = init (Locale.check thy target) thy;
+
+val exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
+
+fun switch NONE (Context.Theory thy) =
+      (Context.Theory o exit, theory_init thy)
+  | switch (SOME name) (Context.Theory thy) =
+      (Context.Theory o exit, begin name thy)
+  | switch NONE (Context.Proof lthy) =
+      (Context.Proof o Local_Theory.restore, lthy)
+  | switch (SOME name) (Context.Proof lthy) =
+      (Context.Proof o init (the (locale_of lthy)) o exit,
+        (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
 
 end;

--- a/src/Pure/Isar/toplevel.ML	Tue Jul 01 21:57:08 2014 -0700
+++ b/src/Pure/Isar/toplevel.ML	Wed Jul 02 08:03:48 2014 +0200
@@ -103,22 +103,6 @@
 exception UNDEF = Runtime.UNDEF;
 
 
-(* named target wrappers *)
-
-val named_init = Named_Target.context_cmd;
-val named_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
-
-fun named_begin NONE (Context.Theory thy) =
-      (Context.Theory o named_exit, named_init ("-", Position.none) thy)
-  | named_begin (SOME loc) (Context.Theory thy) =
-      (Context.Theory o named_exit, named_init loc thy)
-  | named_begin NONE (Context.Proof lthy) =
-      (Context.Proof o Local_Theory.restore, lthy)
-  | named_begin (SOME loc) (Context.Proof lthy) =
-      (Context.Proof o Named_Target.init (the (Named_Target.locale_of lthy)) o named_exit,
-        (named_init loc o named_exit o Local_Theory.assert_nonbrittle) lthy);
-
-
 (* datatype node *)
 
 datatype node =
@@ -413,7 +397,7 @@
   (fn Theory (Context.Theory thy, _) =>
         let
           val lthy = f thy;
-          val gthy = if begin then Context.Proof lthy else Context.Theory (named_exit lthy);
+          val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
           val _ =
             if begin then
               Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
@@ -422,7 +406,7 @@
     | _ => raise UNDEF));
 
 val end_local_theory = transaction (fn _ =>
-  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (named_exit lthy), SOME lthy)
+  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (Named_Target.exit lthy), SOME lthy)
     | _ => raise UNDEF));
 
 fun open_target f = transaction (fn _ =>
@@ -450,7 +434,7 @@
 fun local_theory_presentation loc f = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
         let
-          val (finish, lthy) = named_begin loc gthy;
+          val (finish, lthy) = Named_Target.switch loc gthy;
           val lthy' = lthy
             |> Local_Theory.new_group
             |> f int
@@ -506,7 +490,7 @@
 
 fun local_theory_to_proof' loc f = begin_proof
   (fn int => fn gthy =>
-    let val (finish, lthy) = named_begin loc gthy
+    let val (finish, lthy) = Named_Target.switch loc gthy
     in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
 
 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);