# HG changeset patch
# User wenzelm
# Date 1427887952 -7200
# Node ID 01aff5aa081d6ba6e660ca2c281477efc7c92e47
# Parent  30eef3e45bd011c4f2c5d45e26fb38c36655be82
tuned signature;

diff -r 30eef3e45bd0 -r 01aff5aa081d src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Wed Apr 01 11:55:23 2015 +0200
+++ b/src/Pure/Isar/bundle.ML	Wed Apr 01 13:32:32 2015 +0200
@@ -20,9 +20,10 @@
   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 -> generic_theory -> local_theory
+  val context: string list -> Element.context_i list ->
+    generic_theory -> Binding.scope * local_theory
   val context_cmd: (xstring * Position.T) list -> Element.context list ->
-    generic_theory -> local_theory
+    generic_theory -> Binding.scope * local_theory
   val print_bundles: Proof.context -> unit
 end;
 
@@ -97,7 +98,7 @@
       |> gen_includes get raw_incls
       |> prep_decl ([], []) I raw_elems;
   in
-    lthy' |> Local_Theory.open_target
+    lthy' |> Local_Theory.init_target
       (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
   end;
 
@@ -137,4 +138,3 @@
   end |> Pretty.writeln_chunks;
 
 end;
-
diff -r 30eef3e45bd0 -r 01aff5aa081d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 01 11:55:23 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 01 13:32:32 2015 +0200
@@ -361,7 +361,7 @@
     ((Parse.position Parse.xname >> (fn 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)))
+        >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
       --| Parse.begin);
 
 
diff -r 30eef3e45bd0 -r 01aff5aa081d src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Apr 01 11:55:23 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Apr 01 13:32:32 2015 +0200
@@ -21,9 +21,6 @@
   val assert_bottom: bool -> local_theory -> local_theory
   val mark_brittle: local_theory -> local_theory
   val assert_nonbrittle: local_theory -> local_theory
-  val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
-    local_theory -> local_theory
-  val close_target: local_theory -> local_theory
   val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
   val background_naming_of: local_theory -> Name_Space.naming
   val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
@@ -73,6 +70,10 @@
   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 init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
+    local_theory -> Binding.scope * local_theory
+  val open_target: local_theory -> Binding.scope * local_theory
+  val close_target: local_theory -> local_theory
 end;
 
 structure Local_Theory: LOCAL_THEORY =
@@ -144,20 +145,6 @@
     else lthy
   end;
 
-fun open_target background_naming operations after_close lthy =
-  let
-    val _ = assert lthy;
-    val (_, target) = Proof_Context.new_scope lthy;
-  in
-    target |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)))
-  end;
-
-fun close_target lthy =
-  let
-    val _ = assert_bottom false lthy;
-    val ({after_close, ...} :: rest) = Data.get lthy;
-  in lthy |> Data.put rest |> restore |> after_close end;
-
 fun map_contexts f lthy =
   let val n = level lthy in
     lthy |> (Data.map o map_index)
@@ -350,18 +337,15 @@
 
 
 
-(** init and exit **)
+(** manage targets **)
 
-(* init *)
+(* outermost target *)
 
 fun init background_naming operations target =
   target |> Data.map
     (fn [] => [make_lthy (background_naming, operations, I, false, target)]
       | _ => error "Local theory already initialized");
 
-
-(* exit *)
-
 val exit = operation #exit;
 val exit_global = Proof_Context.theory_of o exit;
 
@@ -378,4 +362,25 @@
     val phi = standard_morphism lthy thy_ctxt;
   in (f phi x, thy) end;
 
+
+(* nested targets *)
+
+fun init_target background_naming operations after_close lthy =
+  let
+    val _ = assert lthy;
+    val (scope, target) = Proof_Context.new_scope lthy;
+    val lthy' =
+      target
+      |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+  in (scope, lthy') end;
+
+fun open_target lthy =
+  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
+
+fun close_target lthy =
+  let
+    val _ = assert_bottom false lthy;
+    val ({after_close, ...} :: rest) = Data.get lthy;
+  in lthy |> Data.put rest |> restore |> after_close end;
+
 end;