# HG changeset patch
# User haftmann
# Date 1501827174 -7200
# Node ID a849ce33923d791568d386441ce66860acbe81d6
# Parent  b210ae666a42a9754f0fe32d5b9bd45ea45488dc
treat exit separate from regular local theory operations

diff -r b210ae666a42 -r a849ce33923d src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/bundle.ML	Fri Aug 04 08:12:54 2017 +0200
@@ -178,15 +178,16 @@
   |> Sign.change_begin
   |> set_target []
   |> Proof_Context.init_global
-  |> Local_Theory.init (Sign.naming_of thy)
+  |> Local_Theory.init
+     {background_naming = Sign.naming_of thy,
+      exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
      {define = bad_operation,
       notes = bundle_notes,
       abbrev = bad_operation,
       declaration = K bundle_declaration,
       theory_registration = bad_operation,
       locale_dependency = bad_operation,
-      pretty = pretty binding,
-      exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
+      pretty = pretty binding}
 
 end;
 
@@ -216,7 +217,8 @@
       |> prep_decl ([], []) I raw_elems;
   in
     lthy' |> Local_Theory.init_target
-      (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
+      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close,
+       exit = Local_Theory.exit_of lthy} (Local_Theory.operations_of lthy)
   end;
 
 in
diff -r b210ae666a42 -r a849ce33923d src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/class.ML	Fri Aug 04 08:12:54 2017 +0200
@@ -694,15 +694,16 @@
     |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
-    |> Local_Theory.init (Sign.naming_of thy)
+    |> Local_Theory.init
+       {background_naming = Sign.naming_of thy,
+        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         theory_registration = Generic_Target.theory_registration,
         locale_dependency = fn _ => error "Not possible in instantiation target",
-        pretty = pretty,
-        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+        pretty = pretty}
   end;
 
 fun instantiation_cmd arities thy =
diff -r b210ae666a42 -r a849ce33923d src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Aug 04 08:12:54 2017 +0200
@@ -65,12 +65,15 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
-  val init: Name_Space.naming -> operations -> Proof.context -> local_theory
+  val init: {background_naming: Name_Space.naming, exit: local_theory -> Proof.context} ->
+    operations -> Proof.context -> local_theory
+  val exit_of: local_theory -> local_theory -> Proof.context
   val exit: local_theory -> Proof.context
   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) ->
+  val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory,
+    exit: local_theory -> Proof.context} -> operations ->
     local_theory -> Binding.scope * local_theory
   val open_target: local_theory -> Binding.scope * local_theory
   val close_target: local_theory -> local_theory
@@ -95,19 +98,19 @@
      local_theory -> local_theory,
   locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
      local_theory -> local_theory,
-  pretty: local_theory -> Pretty.T list,
-  exit: local_theory -> Proof.context};
+  pretty: local_theory -> Pretty.T list};
 
 type lthy =
  {background_naming: Name_Space.naming,
   operations: operations,
   after_close: local_theory -> local_theory,
+  exit: local_theory -> Proof.context,
   brittle: bool,
   target: Proof.context};
 
-fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy =
+fun make_lthy (background_naming, operations, after_close, exit, brittle, target) : lthy =
   {background_naming = background_naming, operations = operations,
-    after_close = after_close, brittle = brittle, target = target};
+    after_close = after_close, exit = exit, brittle = brittle, target = target};
 
 
 (* context data *)
@@ -146,16 +149,16 @@
 
 fun map_top f =
   assert #>
-  Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
-    make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
+  Data.map (fn {background_naming, operations, after_close, exit, brittle, target} :: parents =>
+    make_lthy (f (background_naming, operations, after_close, exit, brittle, target)) :: parents);
 
 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
 fun map_contexts f lthy =
   let val n = level lthy in
     lthy |> (Data.map o map_index)
-      (fn (i, {background_naming, operations, after_close, brittle, target}) =>
-        make_lthy (background_naming, operations, after_close, brittle,
+      (fn (i, {background_naming, operations, after_close, exit, brittle, target}) =>
+        make_lthy (background_naming, operations, after_close, exit, brittle,
           target
           |> Context_Position.set_visible false
           |> f (n - i - 1)
@@ -168,8 +171,8 @@
 
 fun mark_brittle lthy =
   if level lthy = 1 then
-    map_top (fn (background_naming, operations, after_close, _, target) =>
-      (background_naming, operations, after_close, true, target)) lthy
+    map_top (fn (background_naming, operations, after_close, exit, _, target) =>
+      (background_naming, operations, after_close, exit, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
@@ -182,8 +185,8 @@
 val background_naming_of = #background_naming o top_of;
 
 fun map_background_naming f =
-  map_top (fn (background_naming, operations, after_close, brittle, target) =>
-    (f background_naming, operations, after_close, brittle, target));
+  map_top (fn (background_naming, operations, after_close, exit, brittle, target) =>
+    (f background_naming, operations, after_close, exit, brittle, target));
 
 val restore_background_naming = map_background_naming o K o background_naming_of;
 
@@ -348,12 +351,14 @@
 
 (* outermost target *)
 
-fun init background_naming operations target =
+fun init {background_naming, exit} operations target =
   target |> Data.map
-    (fn [] => [make_lthy (background_naming, operations, I, false, target)]
+    (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)]
       | _ => error "Local theory already initialized");
 
-val exit = operation #exit;
+val exit_of = #exit o top_of;
+
+fun exit lthy = exit_of lthy lthy;
 val exit_global = Proof_Context.theory_of o exit;
 
 fun exit_result f (x, lthy) =
@@ -372,18 +377,19 @@
 
 (* nested targets *)
 
-fun init_target background_naming operations after_close lthy =
+fun init_target {background_naming, after_close, exit} operations lthy =
   let
     val _ = assert lthy;
     val after_close' = Proof_Context.restore_naming lthy #> after_close;
     val (scope, target) = Proof_Context.new_scope lthy;
     val lthy' =
       target
-      |> Data.map (cons (make_lthy (background_naming, operations, after_close', true, target)));
+      |> Data.map (cons (make_lthy (background_naming, operations, after_close', exit, true, target)));
   in (scope, lthy') end;
 
 fun open_target lthy =
-  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
+  init_target {background_naming = background_naming_of lthy, after_close = I,
+    exit = exit_of lthy} (operations_of lthy) lthy;
 
 fun close_target lthy =
   let
diff -r b210ae666a42 -r a849ce33923d src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Aug 04 08:12:54 2017 +0200
@@ -128,22 +128,21 @@
 fun init' {setup, conclude} ident thy =
   let
     val target = make_target thy ident;
-    val background_naming =
-      Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident);
   in
     thy
     |> Sign.change_begin
     |> init_context target
     |> setup
-    |> Local_Theory.init background_naming
+    |> Local_Theory.init
+       {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident),
+        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
        {define = Generic_Target.define (foundation target),
         notes = Generic_Target.notes (notes target),
         abbrev = abbrev target,
         declaration = declaration target,
         theory_registration = theory_registration target,
         locale_dependency = locale_dependency target,
-        pretty = pretty target,
-        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+        pretty = pretty target}
   end;
 
 fun init ident thy =
diff -r b210ae666a42 -r a849ce33923d src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/overloading.ML	Fri Aug 04 08:12:54 2017 +0200
@@ -199,15 +199,16 @@
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
     |> activate_improvable_syntax
     |> synchronize_syntax
-    |> Local_Theory.init (Sign.naming_of thy)
+    |> Local_Theory.init
+       {background_naming = Sign.naming_of thy,
+        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         theory_registration = Generic_Target.theory_registration,
         locale_dependency = fn _ => error "Not possible in overloading target",
-        pretty = pretty,
-        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+        pretty = pretty}
   end;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);