dedicated module for toplevel target handling

--- a/src/Pure/Isar/bundle.ML	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/Pure/Isar/bundle.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -23,12 +23,6 @@
   val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
   val including: string list -> Proof.state -> Proof.state
   val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
-  val context: string list -> Element.context_i list ->
-    local_theory -> Binding.scope * local_theory
-  val context_cmd: (xstring * Position.T) list -> Element.context list ->
-    local_theory -> Binding.scope * local_theory
-  val begin_nested_target: Context.generic -> local_theory
-  val end_nested_target: local_theory -> Context.generic
 end;
 
 structure Bundle: BUNDLE =
@@ -208,13 +202,6 @@
 
 fun gen_includes prep_bundle = gen_activate (Attrib.local_notes "") prep_bundle;
 
-fun gen_context prep_bundle prep_decl raw_incls raw_elems lthy =
-  lthy
-  |> gen_includes prep_bundle raw_incls
-  |> prep_decl ([], []) I raw_elems
-  |> (#4 o fst)
-  |> Local_Theory.begin_nested;
-
 in
 
 val unbundle = gen_activate Local_Theory.notes get;
@@ -230,18 +217,6 @@
 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
 
-val context = gen_context get Expression.cert_declaration;
-
-val context_cmd = gen_context read Expression.read_declaration;
-
-val begin_nested_target =
-  Context.cases Named_Target.theory_init Local_Theory.assert;
-
-fun end_nested_target lthy = 
-  if Named_Target.is_theory lthy
-  then Context.Theory (Local_Theory.exit_global lthy)
-  else Context.Proof lthy;
-
 end;
 
 end;

--- a/src/Pure/Isar/named_target.ML	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/Pure/Isar/named_target.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -18,10 +18,7 @@
   val theory_map: (local_theory -> local_theory) -> theory -> theory
   val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
     theory -> 'b * 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
+  val reinit: local_theory -> theory -> local_theory
 end;
 
 structure Named_Target: NAMED_TARGET =
@@ -141,22 +138,6 @@
 
 fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f;
 
-
-(* toplevel interaction *)
-
-fun begin ("-", _) thy = theory_init thy
-  | begin target thy = init (Locale.check thy target) thy;
-
-val exit = Local_Theory.assert_bottom #> 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.reset, lthy)
-  | switch (SOME name) (Context.Proof lthy) =
-      (Context.Proof o init (ident_of lthy) o exit,
-        (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
+fun reinit lthy = init (ident_of lthy);
 
 end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/target_context.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -0,0 +1,55 @@
+(*  Title:      Pure/Isar/target_context.ML
+    Author:     Florian Haftmann
+
+Handling of named and nested targets at the Isar toplevel via context begin / end blocks.
+*)
+
+signature TARGET_CONTEXT =
+sig
+  val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory
+  val end_named_cmd: local_theory -> theory
+  val switch_named_cmd: (xstring * Position.T) option -> Context.generic ->
+    (local_theory -> Context.generic) * local_theory
+  val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list ->
+    Context.generic -> local_theory
+  val end_nested_cmd: local_theory -> Context.generic
+end;
+
+structure Target_Context: TARGET_CONTEXT =
+struct
+
+fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy
+  | context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy;
+
+val end_named_cmd = Local_Theory.assert_bottom #> Local_Theory.exit_global;
+
+fun switch_named_cmd NONE (Context.Theory thy) =
+      (Context.Theory o end_named_cmd, Named_Target.theory_init thy)
+  | switch_named_cmd (SOME name) (Context.Theory thy) =
+      (Context.Theory o end_named_cmd, context_begin_named_cmd name thy)
+  | switch_named_cmd NONE (Context.Proof lthy) =
+      (Context.Proof o Local_Theory.reset, lthy)
+  | switch_named_cmd (SOME name) (Context.Proof lthy) =
+      (Context.Proof o Named_Target.reinit lthy o end_named_cmd,
+        (context_begin_named_cmd name o end_named_cmd o Local_Theory.assert_nonbrittle) lthy);
+
+fun includes raw_incls lthy =
+  Bundle.includes (map (Bundle.check lthy) raw_incls) lthy;
+
+fun context_begin_nested_cmd raw_incls raw_elems gthy =
+  gthy
+  |> Context.cases Named_Target.theory_init Local_Theory.assert
+  |> includes raw_incls
+  |> Expression.read_declaration ([], []) I raw_elems
+  |> (#4 o fst)
+  |> Local_Theory.begin_nested
+  |> snd;
+
+fun end_nested_cmd lthy = 
+  if Named_Target.is_theory lthy
+  then Context.Theory (Local_Theory.exit_global lthy)
+  else Context.Proof lthy;
+
+end;
+
+structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;

--- a/src/Pure/Isar/toplevel.ML	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/Pure/Isar/toplevel.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -54,7 +54,7 @@
   val theory: (theory -> theory) -> transition -> transition
   val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition
   val end_main_target: transition -> transition
-  val begin_nested_target: (local_theory -> local_theory) -> transition -> transition
+  val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition
   val end_nested_target: transition -> transition
   val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
     (bool -> local_theory -> local_theory) -> transition -> transition
@@ -436,7 +436,10 @@
   (fn Theory (Context.Theory thy) =>
         let
           val lthy = f thy;
-          val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
+          val gthy =
+            if begin
+            then Context.Proof lthy
+            else Context.Theory (Target_Context.end_named_cmd lthy);
           val _ =
             (case Local_Theory.pretty lthy of
               [] => ()
@@ -445,14 +448,13 @@
     | _ => raise UNDEF));
 
 val end_main_target = transaction (fn _ =>
-  (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Named_Target.exit lthy)), lthy)
+  (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Target_Context.end_named_cmd lthy)), lthy)
     | _ => raise UNDEF));
 
 fun begin_nested_target f = transaction0 (fn _ =>
   (fn Theory gthy =>
         let
-          val lthy = Bundle.begin_nested_target gthy;
-          val lthy' = f lthy
+          val lthy' = f gthy;
         in Theory (Context.Proof lthy') end
     | _ => raise UNDEF));
 
@@ -460,7 +462,7 @@
   (fn Theory (Context.Proof lthy) =>
         (case try Local_Theory.end_nested lthy of
           SOME lthy' =>
-            let val gthy' = Bundle.end_nested_target lthy'
+            let val gthy' = Target_Context.end_nested_cmd lthy'
             in (Theory gthy', lthy) end
         | NONE => raise UNDEF)
     | _ => raise UNDEF));
@@ -472,7 +474,7 @@
 fun local_theory' restricted target f = present_transaction (fn int =>
   (fn Theory gthy =>
         let
-          val (finish, lthy) = Named_Target.switch target gthy;
+          val (finish, lthy) = Target_Context.switch_named_cmd target gthy;
           val lthy' = lthy
             |> restricted_context restricted
             |> Local_Theory.new_group
@@ -486,7 +488,7 @@
 
 fun present_local_theory target = present_transaction (fn _ =>
   (fn Theory gthy =>
-        let val (finish, lthy) = Named_Target.switch target gthy;
+        let val (finish, lthy) = Target_Context.switch_named_cmd target gthy;
         in (Theory (finish lthy), lthy) end
     | _ => raise UNDEF));
 
@@ -531,7 +533,7 @@
 fun local_theory_to_proof' restricted target f = begin_proof
   (fn int => fn gthy =>
     let
-      val (finish, lthy) = Named_Target.switch target gthy;
+      val (finish, lthy) = Target_Context.switch_named_cmd target gthy;
       val prf = lthy
         |> restricted_context restricted
         |> Local_Theory.new_group
@@ -789,5 +791,3 @@
 end;
 
 end;
-
-structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;

--- a/src/Pure/Pure.thy	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/Pure/Pure.thy	Mon Oct 12 07:25:38 2020 +0000
@@ -626,9 +626,10 @@
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
-    ((Parse.name_position >> (Toplevel.begin_main_target true o Named_Target.begin) ||
+    ((Parse.name_position
+        >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
-        >> (fn (incls, elems) => Toplevel.begin_nested_target (#2 o Bundle.context_cmd incls elems)))
+        >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems)))
       --| Parse.begin);
 
 val _ =

--- a/src/Pure/ROOT.ML	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/Pure/ROOT.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -268,6 +268,7 @@
 ML_file "Isar/interpretation.ML";
 ML_file "Isar/class_declaration.ML";
 ML_file "Isar/bundle.ML";
+ML_file "Isar/target_context.ML";
 ML_file "Isar/experiment.ML";
 
 ML_file "simplifier.ML";