# HG changeset patch
# User wenzelm
# Date 1357403934 -3600
# Node ID 5165d7e6d3b9e696654e6cdc4ce89d33c48f0870
# Parent  d5725e56cd049b5f98e0948555e03c0d646126ea
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
explicit target for context within global theory with after_close = exit to manage the 2 levels involved here;
reject "(in target)" for nested contexts more reliably -- difficult to handle due to lack of nested reinit;

diff -r d5725e56cd04 -r 5165d7e6d3b9 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sat Jan 05 17:24:27 2013 +0100
+++ b/src/Pure/Isar/bundle.ML	Sat Jan 05 17:38:54 2013 +0100
@@ -93,20 +93,15 @@
 
 fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy =
   let
-    val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
-    fun augment ctxt =
-      let
-        val ((_, _, _, ctxt'), _) = ctxt
-          |> Context_Position.restore_visible lthy
-          |> gen_includes prep_bundle raw_incls
-          |> prep_decl ([], []) I raw_elems;
-      in ctxt' |> Context_Position.restore_visible ctxt end;
+    val (after_close, lthy) =
+      gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init)
+        (pair I o Local_Theory.assert);
+    val ((_, _, _, lthy'), _) = lthy
+      |> gen_includes prep_bundle raw_incls
+      |> prep_decl ([], []) I raw_elems;
   in
-    (case gthy of
-      Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
-    | Context.Proof _ =>
-        augment lthy |>
-        Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy))
+    lthy' |> Local_Theory.open_target
+      (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy) after_close
   end;
 
 in
diff -r d5725e56cd04 -r 5165d7e6d3b9 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Jan 05 17:24:27 2013 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Jan 05 17:38:54 2013 +0100
@@ -14,7 +14,8 @@
   val restore: local_theory -> local_theory
   val level: Proof.context -> int
   val assert_bottom: bool -> local_theory -> local_theory
-  val open_target: Name_Space.naming -> operations -> 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 naming_of: local_theory -> Name_Space.naming
@@ -83,10 +84,11 @@
 type lthy =
  {naming: Name_Space.naming,
   operations: operations,
+  after_close: local_theory -> local_theory,
   target: Proof.context};
 
-fun make_lthy (naming, operations, target) : lthy =
-  {naming = naming, operations = operations, target = target};
+fun make_lthy (naming, operations, after_close, target) : lthy =
+  {naming = naming, operations = operations, after_close = after_close, target = target};
 
 
 (* context data *)
@@ -103,16 +105,17 @@
 val get_last_lthy = List.last o Data.get o assert;
 val get_first_lthy = hd o Data.get o assert;
 
-fun map_first_lthy f = assert #>
-  Data.map (fn {naming, operations, target} :: parents =>
-    make_lthy (f (naming, operations, target)) :: parents);
+fun map_first_lthy f =
+  assert #>
+  Data.map (fn {naming, operations, after_close, target} :: parents =>
+    make_lthy (f (naming, operations, after_close, target)) :: parents);
 
 fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
 
 
 (* nested structure *)
 
-val level = length o Data.get;
+val level = length o Data.get;  (*1: main target at bottom, >= 2: nested context*)
 
 fun assert_bottom b lthy =
   let
@@ -124,16 +127,20 @@
     else lthy
   end;
 
-fun open_target naming operations target = assert target
-  |> Data.map (cons (make_lthy (naming, operations, target)));
+fun open_target naming operations after_close target =
+  assert target
+  |> Data.map (cons (make_lthy (naming, operations, after_close, target)));
 
 fun close_target lthy =
-  assert_bottom false lthy |> Data.map tl |> restore;
+  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) (fn (i, {naming, operations, target}) =>
-      make_lthy (naming, operations,
+    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, target}) =>
+      make_lthy (naming, operations, after_close,
         target
         |> Context_Position.set_visible false
         |> f (n - i - 1)
@@ -148,7 +155,8 @@
 val full_name = Name_Space.full_name o naming_of;
 
 fun map_naming f =
-  map_first_lthy (fn (naming, operations, target) => (f naming, operations, target));
+  map_first_lthy (fn (naming, operations, after_close, target) =>
+    (f naming, operations, after_close, target));
 
 val conceal = map_naming Name_Space.conceal;
 val new_group = map_naming Name_Space.new_group;
@@ -279,7 +287,7 @@
 
 fun init naming operations target =
   target |> Data.map
-    (fn [] => [make_lthy (naming, operations, target)]
+    (fn [] => [make_lthy (naming, operations, I, target)]
       | _ => error "Local theory already initialized")
   |> checkpoint;
 
diff -r d5725e56cd04 -r 5165d7e6d3b9 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jan 05 17:24:27 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Jan 05 17:38:54 2013 +0100
@@ -461,7 +461,13 @@
 val close_target = transaction (fn _ =>
   (fn Theory (Context.Proof lthy, _) =>
         (case try Local_Theory.close_target lthy of
-          SOME lthy' => Theory (Context.Proof lthy', SOME lthy)
+          SOME ctxt' =>
+            let
+              val gthy' =
+                if can Local_Theory.assert ctxt'
+                then Context.Proof ctxt'
+                else Context.Theory (Proof_Context.theory_of ctxt');
+            in Theory (gthy', SOME lthy) end
         | NONE => raise UNDEF)
     | _ => raise UNDEF));