# HG changeset patch
# User haftmann
# Date 1602355900 0
# Node ID d62d84634b066f3859b0b6bd4cc447e3ba11d747
# Parent  166fc8b9b4cd587164b0f6caefa62327e1ab9986
direct exit to theory when ending nested target on theory target

diff -r 166fc8b9b4cd -r d62d84634b06 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Sat Oct 10 18:43:10 2020 +0000
+++ b/src/HOL/Eisbach/method_closure.ML	Sat Oct 10 18:51:40 2020 +0000
@@ -178,7 +178,8 @@
   let
     val (uses_internal, lthy1) = lthy
       |> Proof_Context.concealed
-      |> Local_Theory.begin_target I |-> Proof_Context.private_scope
+      |> Local_Theory.begin_target
+      |-> Proof_Context.private_scope
       |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
       |> Config.put Method.old_section_parser true
       |> fold setup_local_method methods
diff -r 166fc8b9b4cd -r d62d84634b06 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sat Oct 10 18:43:10 2020 +0000
+++ b/src/Pure/Isar/bundle.ML	Sat Oct 10 18:51:40 2020 +0000
@@ -208,18 +208,15 @@
 
 fun gen_context get prep_decl raw_incls raw_elems gthy =
   let
-    val init = Context.cases
-      (pair Local_Theory.exit o Named_Target.theory_init)
-      (pair I o Local_Theory.assert);
     val import =
       gen_includes get raw_incls
       #> prep_decl ([], []) I raw_elems
       #> (#4 o fst);
   in
     gthy
-    |> init
-    ||> import
-    |-> (fn after_close => Local_Theory.begin_target after_close)
+    |> Context.cases Named_Target.theory_init Local_Theory.assert
+    |> import
+    |> Local_Theory.begin_target
   end;
 
 in
diff -r 166fc8b9b4cd -r d62d84634b06 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Oct 10 18:43:10 2020 +0000
+++ b/src/Pure/Isar/local_theory.ML	Sat Oct 10 18:51:40 2020 +0000
@@ -73,7 +73,7 @@
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
-  val begin_target: (local_theory -> local_theory) -> local_theory -> Binding.scope * local_theory
+  val begin_target: local_theory -> Binding.scope * local_theory
   val open_target: local_theory -> local_theory
   val close_target: local_theory -> local_theory
   val subtarget: (local_theory -> local_theory) -> local_theory -> local_theory
@@ -383,20 +383,16 @@
 
 (* nested targets *)
 
-fun init_target {background_naming, after_close} operations lthy =
+fun begin_target lthy =
   let
     val _ = assert lthy;
-    val after_close' = Proof_Context.restore_naming lthy #> after_close;
     val (scope, target) = Proof_Context.new_scope lthy;
-    val entry = make_lthy (background_naming, operations, after_close', exit_of lthy, true, target);
+    val entry = make_lthy (background_naming_of lthy, operations_of lthy,
+      Proof_Context.restore_naming lthy, exit_of lthy, true, target);
     val lthy' = Data.map (cons entry) target;
   in (scope, lthy') end;
 
-fun begin_target after_close lthy =
-  init_target {background_naming = background_naming_of lthy, after_close = after_close}
-    (operations_of lthy) lthy;
-
-val open_target = begin_target I #> #2;
+val open_target = begin_target #> snd;
 
 fun close_target lthy =
   let
diff -r 166fc8b9b4cd -r d62d84634b06 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Oct 10 18:43:10 2020 +0000
+++ b/src/Pure/Isar/toplevel.ML	Sat Oct 10 18:51:40 2020 +0000
@@ -457,12 +457,12 @@
 val end_nested_target = transaction (fn _ =>
   (fn Theory (Context.Proof lthy) =>
         (case try Local_Theory.close_target lthy of
-          SOME ctxt' =>
+          SOME lthy' =>
             let
               val gthy' =
-                if can Local_Theory.assert ctxt'
-                then Context.Proof ctxt'
-                else Context.Theory (Proof_Context.theory_of ctxt');
+                if Named_Target.is_theory lthy'
+                then Context.Theory (Local_Theory.exit_global lthy')
+                else Context.Proof lthy'
             in (Theory gthy', lthy) end
         | NONE => raise UNDEF)
     | _ => raise UNDEF));