added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;

--- a/src/HOL/Statespace/ROOT.ML	Sat Jan 15 22:40:17 2011 +0100
+++ b/src/HOL/Statespace/ROOT.ML	Sun Jan 16 14:57:14 2011 +0100
@@ -1,1 +1,1 @@
-use_thys ["StateSpaceEx"];
\ No newline at end of file
+use_thys ["StateSpaceEx"];

--- a/src/HOL/Statespace/state_space.ML	Sat Jan 15 22:40:17 2011 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sun Jan 16 14:57:14 2011 +0100
@@ -145,20 +145,20 @@
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_cmd name expr []
+   |> Expression.sublocale_cmd I name expr []
    |> Proof.global_terminal_proof
          (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    |> ProofContext.theory_of
 
 fun add_locale name expr elems thy =
   thy 
-  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
+  |> Expression.add_locale I (Binding.name name) (Binding.name name) expr elems
   |> snd
   |> Local_Theory.exit;
 
 fun add_locale_cmd name expr elems thy =
   thy 
-  |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
+  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty expr elems
   |> snd
   |> Local_Theory.exit;
 
@@ -349,7 +349,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Named_Target.init name
+  |> Named_Target.init I name
   |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
   |> Local_Theory.exit_global;
 

--- a/src/Pure/Isar/class_declaration.ML	Sat Jan 15 22:40:17 2011 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Sun Jan 16 14:57:14 2011 +0100
@@ -6,13 +6,14 @@
 
 signature CLASS_DECLARATION =
 sig
-  val class: binding -> class list -> Element.context_i list
-    -> theory -> string * local_theory
-  val class_cmd: binding -> xstring list -> Element.context list
-    -> theory -> string * local_theory
-  val prove_subclass: tactic -> class -> local_theory -> local_theory
-  val subclass: class -> local_theory -> Proof.state
-  val subclass_cmd: xstring -> local_theory -> Proof.state
+  val class: (local_theory -> local_theory) -> binding -> class list ->
+    Element.context_i list -> theory -> string * local_theory
+  val class_cmd: (local_theory -> local_theory) -> binding -> xstring list ->
+    Element.context list -> theory -> string * local_theory
+  val prove_subclass: (local_theory -> local_theory) -> tactic -> class ->
+    local_theory -> local_theory
+  val subclass: (local_theory -> local_theory) -> class -> local_theory -> Proof.state
+  val subclass_cmd: (local_theory -> local_theory) -> xstring -> local_theory -> Proof.state
 end;
 
 structure Class_Declaration: CLASS_DECLARATION =
@@ -288,14 +289,14 @@
     #> pair (param_map, params, assm_axiom)))
   end;
 
-fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
   let
     val class = Sign.full_name thy b;
     val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
       prep_class_spec thy raw_supclasses raw_elems;
   in
     thy
-    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
+    |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems
     |> snd |> Local_Theory.exit_global
     |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
     ||> Theory.checkpoint
@@ -305,7 +306,7 @@
        Context.theory_map (Locale.add_registration (class, base_morph)
          (Option.map (rpair true) eq_morph) export_morph)
     #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
-    |> Named_Target.init class
+    |> Named_Target.init before_exit class
     |> pair class
   end;
 
@@ -321,7 +322,7 @@
 
 local
 
-fun gen_subclass prep_class do_proof raw_sup lthy =
+fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
@@ -338,7 +339,7 @@
     fun after_qed some_wit =
       ProofContext.background_theory (Class.register_subclass (sub, sup)
         some_dep_morph some_wit export)
-      #> ProofContext.theory_of #> Named_Target.init sub;
+      #> ProofContext.theory_of #> Named_Target.init before_exit sub;
   in do_proof after_qed some_prop goal_ctxt end;
 
 fun user_proof after_qed some_prop =
@@ -352,7 +353,7 @@
 in
 
 val subclass = gen_subclass (K I) user_proof;
-fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
+fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
 val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
 
 end; (*local*)

--- a/src/Pure/Isar/expression.ML	Sat Jan 15 22:40:17 2011 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Jan 16 14:57:14 2011 +0100
@@ -29,20 +29,20 @@
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
-  val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
-    theory -> string * local_theory
-  val add_locale_cmd: binding -> binding -> expression -> Element.context list ->
-    theory -> string * local_theory
+  val add_locale: (local_theory -> local_theory) -> binding -> binding ->
+    expression_i -> Element.context_i list -> theory -> string * local_theory
+  val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
+    expression -> Element.context list -> theory -> string * local_theory
 
   (* Interpretation *)
   val cert_goal_expression: expression_i -> Proof.context ->
     (term list list * (string * morphism) list * morphism) * Proof.context
   val read_goal_expression: expression -> Proof.context ->
     (term list list * (string * morphism) list * morphism) * Proof.context
-  val sublocale: string -> expression_i -> (Attrib.binding * term) list ->
-    theory -> Proof.state
-  val sublocale_cmd: string -> expression -> (Attrib.binding * string) list ->
-    theory -> Proof.state
+  val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
+    (Attrib.binding * term) list -> theory -> Proof.state
+  val sublocale_cmd: (local_theory -> local_theory) -> string -> expression ->
+    (Attrib.binding * string) list -> theory -> Proof.state
   val interpretation: expression_i -> (Attrib.binding * term) list ->
     theory -> Proof.state
   val interpretation_cmd: expression -> (Attrib.binding * string) list ->
@@ -731,7 +731,7 @@
   | defines_to_notes _ e = e;
 
 fun gen_add_locale prep_decl
-    binding raw_predicate_binding raw_import raw_body thy =
+    before_exit binding raw_predicate_binding raw_import raw_body thy =
   let
     val name = Sign.full_name thy binding;
     val _ = Locale.defined thy name andalso
@@ -784,7 +784,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
-      |> Named_Target.init name
+      |> Named_Target.init before_exit name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
@@ -900,11 +900,11 @@
           export theory) (deps ~~ witss))
   end;
 
-fun gen_sublocale prep_expr intern parse_prop prep_attr raw_target
-    expression equations thy =
+fun gen_sublocale prep_expr intern parse_prop prep_attr
+    before_exit raw_target expression equations thy =
   let
     val target = intern thy raw_target;
-    val target_ctxt = Named_Target.init target thy;
+    val target_ctxt = Named_Target.init before_exit target thy;
     val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
 
     val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
@@ -919,8 +919,8 @@
 in
 
 fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
-fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern
-  Syntax.parse_prop Attrib.intern_src x;
+fun sublocale_cmd x =
+  gen_sublocale read_goal_expression Locale.intern Syntax.parse_prop Attrib.intern_src x;
 
 end;
 

--- a/src/Pure/Isar/isar_syn.ML	Sat Jan 15 22:40:17 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Jan 16 14:57:14 2011 +0100
@@ -413,7 +413,7 @@
       Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
+            (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
 
 fun parse_interpretation_arguments mandatory =
   Parse.!!! (Parse_Spec.locale_expression mandatory) --
@@ -426,7 +426,7 @@
     (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
       parse_interpretation_arguments false
       >> (fn (loc, (expr, equations)) =>
-          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr equations)));
+          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
 
 val _ =
   Outer_Syntax.command "interpretation"
@@ -456,11 +456,11 @@
    (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-          (Class_Declaration.class_cmd name supclasses elems #> snd)));
+          (Class_Declaration.class_cmd I name supclasses elems #> snd)));
 
 val _ =
   Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
-    (Parse.xname >> Class_Declaration.subclass_cmd);
+    (Parse.xname >> Class_Declaration.subclass_cmd I);
 
 val _ =
   Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl

--- a/src/Pure/Isar/named_target.ML	Sat Jan 15 22:40:17 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Jan 16 14:57:14 2011 +0100
@@ -7,7 +7,7 @@
 
 signature NAMED_TARGET =
 sig
-  val init: string -> theory -> local_theory
+  val init: (local_theory -> local_theory) -> string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val reinit: local_theory -> local_theory -> local_theory
   val context_cmd: xstring -> theory -> local_theory
@@ -19,12 +19,18 @@
 
 (* context data *)
 
-datatype target = Target of {target: string, is_locale: bool, is_class: bool};
+datatype target =
+  Target of {target: string, is_locale: bool, is_class: bool,
+    before_exit: local_theory -> local_theory};
 
-fun named_target _ "" = Target {target = "", is_locale = false, is_class = false}
-  | named_target thy locale =
+fun make_target target is_locale is_class before_exit =
+  Target {target = target, is_locale = is_locale, is_class = is_class,
+    before_exit = before_exit};
+
+fun named_target _ "" before_exit = make_target "" false false before_exit
+  | named_target thy locale before_exit =
       if Locale.defined thy locale
-      then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
+      then make_target locale true (Class.is_class thy locale) before_exit
       else error ("No such locale: " ^ quote locale);
 
 structure Data = Proof_Data
@@ -33,7 +39,9 @@
   fun init _ = NONE;
 );
 
-val peek = Option.map (fn Target args => args) o Data.get;
+val peek =
+  Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
+    {target = target, is_locale = is_locale, is_class = is_class});
 
 
 (* generic declarations *)
@@ -169,14 +177,14 @@
 
 (* init *)
 
-fun init_context (Target {target, is_locale, is_class}) =
+fun init_context (Target {target, is_locale, is_class, ...}) =
   if not is_locale then ProofContext.init_global
   else if not is_class then Locale.init target
   else Class.init target;
 
-fun init target thy =
+fun init before_exit target thy =
   let
-    val ta = named_target thy target;
+    val ta = named_target thy target before_exit;
   in
     thy
     |> init_context ta
@@ -190,17 +198,17 @@
         syntax_declaration = fn pervasive => target_declaration ta
           {syntax = true, pervasive = pervasive},
         pretty = pretty ta,
-        exit = Local_Theory.target_of}
+        exit = Local_Theory.target_of o before_exit}
   end;
 
-val theory_init = init "";
+val theory_init = init I "";
 
 fun reinit lthy =
-  (case peek lthy of
-    SOME {target, ...} => init target o Local_Theory.exit_global
+  (case Data.get lthy of
+    SOME (Target {target, before_exit, ...}) => init before_exit target o Local_Theory.exit_global
   | NONE => error "Not in a named target");
 
-fun context_cmd "-" thy = init "" thy
-  | context_cmd target thy = init (Locale.intern thy target) thy;
+fun context_cmd "-" thy = init I "" thy
+  | context_cmd target thy = init I (Locale.intern thy target) thy;
 
 end;