# HG changeset patch
# User haftmann
# Date 1501827157 -7200
# Node ID b210ae666a42a9754f0fe32d5b9bd45ea45488dc
# Parent  30c1639a343ae185df220d43cd5f24ff25fa85e0
provide explicit variant initializers for regular named target vs. almost-named target

diff -r 30c1639a343a -r b210ae666a42 src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Fri Aug 04 08:12:37 2017 +0200
@@ -91,8 +91,7 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Named_Target.init: "(local_theory -> local_theory) option ->
-    string -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
   @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
diff -r 30c1639a343a -r b210ae666a42 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -298,7 +298,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Named_Target.init NONE name
+  |> Named_Target.init name
   |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
diff -r 30c1639a343a -r b210ae666a42 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -327,7 +327,7 @@
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
     |> snd
-    |> Named_Target.init NONE class
+    |> Named_Target.init class
     |> pair class
   end;
 
diff -r 30c1639a343a -r b210ae666a42 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -825,7 +825,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
-      |> Named_Target.init NONE name
+      |> Named_Target.init name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
diff -r 30c1639a343a -r b210ae666a42 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/interpretation.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -220,7 +220,7 @@
 fun gen_global_sublocale prep_loc prep_interpretation
     raw_locale expression raw_defs raw_eqns thy =
   let
-    val lthy = Named_Target.init NONE (prep_loc thy raw_locale) thy;
+    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
     fun setup_proof after_qed =
       Element.witness_proof_eqs
         (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
diff -r 30c1639a343a -r b210ae666a42 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:37 2017 +0200
@@ -11,7 +11,9 @@
   val locale_of: local_theory -> string option
   val bottom_locale_of: local_theory -> string option
   val class_of: local_theory -> string option
-  val init: (local_theory -> local_theory) option -> string -> theory -> local_theory
+  val init: string -> theory -> local_theory
+  val init': {setup: local_theory -> local_theory, conclude: local_theory -> local_theory} ->
+    string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val theory_map: (local_theory -> local_theory) -> theory -> theory
   val begin: xstring * Position.T -> theory -> local_theory
@@ -123,7 +125,7 @@
   | init_context (Locale locale) = Locale.init locale
   | init_context (Class class) = Class.init class;
 
-fun init before_exit ident thy =
+fun init' {setup, conclude} ident thy =
   let
     val target = make_target thy ident;
     val background_naming =
@@ -132,7 +134,7 @@
     thy
     |> Sign.change_begin
     |> init_context target
-    |> is_none before_exit ? Data.put (SOME target)
+    |> setup
     |> Local_Theory.init background_naming
        {define = Generic_Target.define (foundation target),
         notes = Generic_Target.notes (notes target),
@@ -141,11 +143,13 @@
         theory_registration = theory_registration target,
         locale_dependency = locale_dependency target,
         pretty = pretty target,
-        exit = the_default I before_exit
-          #> Local_Theory.target_of #> Sign.change_end_local}
+        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   end;
 
-val theory_init = init NONE "";
+fun init ident thy =
+  init' {setup = Data.put (SOME (make_target thy ident)), conclude = I} ident thy;
+
+val theory_init = init "";
 
 fun theory_map f = theory_init #> f #> Local_Theory.exit_global;
 
@@ -153,7 +157,7 @@
 (* toplevel interaction *)
 
 fun begin ("-", _) thy = theory_init thy
-  | begin target thy = init NONE (Locale.check thy target) thy;
+  | begin target thy = init (Locale.check thy target) thy;
 
 val exit = Local_Theory.assert_bottom #> Local_Theory.exit_global;
 
@@ -164,7 +168,7 @@
   | switch NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.reset, lthy)
   | switch (SOME name) (Context.Proof lthy) =
-      (Context.Proof o init NONE (ident_of lthy) o exit,
+      (Context.Proof o init (ident_of lthy) o exit,
         (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
 
 end;