# HG changeset patch
# User haftmann
# Date 1602487538 0
# Node ID e1ee4a9902bd329a79c09b7b42ca670dfa29279e
# Parent  faad63aca1e724d09898f4ac31a4aa28dc622ac2
centralized case distinction for beginning and ending nested targets in one place

diff -r faad63aca1e7 -r e1ee4a9902bd src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sun Oct 11 22:26:55 2020 +0200
+++ b/src/Pure/Isar/bundle.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -24,9 +24,11 @@
   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 ->
-    generic_theory -> Binding.scope * local_theory
+    local_theory -> Binding.scope * local_theory
   val context_cmd: (xstring * Position.T) list -> Element.context list ->
-    generic_theory -> Binding.scope * local_theory
+    local_theory -> Binding.scope * local_theory
+  val begin_nested: Context.generic -> local_theory
+  val end_nested: local_theory -> Context.generic
 end;
 
 structure Bundle: BUNDLE =
@@ -206,18 +208,12 @@
 
 fun gen_includes get = gen_activate (Attrib.local_notes "") get;
 
-fun gen_context get prep_decl raw_incls raw_elems gthy =
-  let
-    val import =
-      gen_includes get raw_incls
-      #> prep_decl ([], []) I raw_elems
-      #> (#4 o fst);
-  in
-    gthy
-    |> Context.cases Named_Target.theory_init Local_Theory.assert
-    |> import
-    |> Local_Theory.begin_target
-  end;
+fun gen_context get prep_decl raw_incls raw_elems lthy =
+  lthy
+  |> gen_includes get raw_incls
+  |> prep_decl ([], []) I raw_elems
+  |> (#4 o fst)
+  |> Local_Theory.begin_target;
 
 in
 
@@ -235,8 +231,17 @@
 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
 
 val context = gen_context get_bundle Expression.cert_declaration;
+
 val context_cmd = gen_context get_bundle_cmd Expression.read_declaration;
 
+val begin_nested =
+  Context.cases Named_Target.theory_init Local_Theory.assert;
+
+fun end_nested lthy = 
+  if Named_Target.is_theory lthy
+  then Context.Theory (Local_Theory.exit_global lthy)
+  else Context.Proof lthy;
+
 end;
 
 end;
diff -r faad63aca1e7 -r e1ee4a9902bd src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Oct 11 22:26:55 2020 +0200
+++ 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: (generic_theory -> local_theory) -> transition -> transition
+  val begin_nested_target: (local_theory -> 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
@@ -450,19 +450,17 @@
 
 fun begin_nested_target f = transaction0 (fn _ =>
   (fn Theory gthy =>
-        let val lthy = f gthy
-        in Theory (Context.Proof lthy) end
+        let
+          val lthy = Bundle.begin_nested gthy;
+          val lthy' = f lthy
+        in Theory (Context.Proof lthy') end
     | _ => raise UNDEF));
 
 val end_nested_target = transaction (fn _ =>
   (fn Theory (Context.Proof lthy) =>
         (case try Local_Theory.close_target lthy of
           SOME lthy' =>
-            let
-              val gthy' =
-                if Named_Target.is_theory lthy'
-                then Context.Theory (Local_Theory.exit_global lthy')
-                else Context.Proof lthy'
+            let val gthy' = Bundle.end_nested lthy'
             in (Theory gthy', lthy) end
         | NONE => raise UNDEF)
     | _ => raise UNDEF));