Sublocale: removed public after_qed; identifiers private to NewLocale.

--- a/src/Pure/Isar/expression.ML	Wed Dec 03 15:26:46 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Dec 03 15:27:41 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/expression.ML
-    ID:         $Id$
     Author:     Clemens Ballarin, TU Muenchen
 
 New locale development --- experimental.
@@ -25,10 +24,8 @@
     string * Proof.context
 
   (* Interpretation *)
-  val sublocale_cmd: (thm list list -> Proof.context -> Proof.context) ->
-    string -> expression -> theory -> Proof.state;
-  val sublocale: (thm list list -> Proof.context -> Proof.context) ->
-    string -> expression_i -> theory -> Proof.state;
+  val sublocale_cmd: string -> expression -> theory -> Proof.state;
+  val sublocale: string -> expression_i -> theory -> Proof.state;
 
   (* Debugging and development *)
   val parse_expression: OuterParse.token list -> expression * OuterParse.token list
@@ -434,7 +431,7 @@
 
     val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
 
-    fun prep_inst (loc, (prfx, inst)) (i, marked, insts, ctxt) =
+    fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
       let
         val (parm_names, parm_types) = NewLocale.params_of thy loc |>
           map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
@@ -443,11 +440,11 @@
           Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
         val inst'' = map2 TypeInfer.constrain parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
-        val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt;
+        val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
         val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
-        val (marked', ctxt'') = NewLocale.activate_declarations thy (loc, morph) (marked, ctxt);
-      in (i+1, marked', insts', ctxt'') end;
+        val ctxt'' = NewLocale.activate_declarations thy (loc, morph) ctxt;
+      in (i+1, insts', ctxt'') end;
   
     fun prep_elem raw_elem (insts, elems, ctxt) =
       let
@@ -465,7 +462,7 @@
 
     val fors = prep_vars fixed context |> fst;
     val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
-    val (_, _, insts', ctxt') = fold prep_inst raw_insts (0, NewLocale.empty, [], ctxt);
+    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_idents ctxt);
     val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
     val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
 
@@ -542,7 +539,7 @@
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
-      pair NewLocale.empty |> fold (NewLocale.activate_facts thy) deps |> snd;
+      NewLocale.clear_idents |> fold (NewLocale.activate_facts thy) deps;
     val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
   in ((fixed, deps, elems'), (parms, spec, defs)) end;
 
@@ -804,7 +801,7 @@
 local
 
 fun gen_sublocale prep_expr intern
-    after_qed raw_target expression thy =
+    raw_target expression thy =
   let
     val target = intern thy raw_target;
     val target_ctxt = NewLocale.init target thy;
@@ -814,13 +811,10 @@
     fun store_dep ((name, morph), thms) =
       NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
 
-    fun after_qed' results =
-      fold store_dep (deps ~~ prep_result propss results) #>
-      after_qed results;
-
+    fun after_qed results = fold store_dep (deps ~~ prep_result propss results);
   in
     goal_ctxt |>
-      Proof.theorem_i NONE after_qed' (prep_propp propss) |>
+      Proof.theorem_i NONE after_qed (prep_propp propss) |>
       Element.refine_witness |> Seq.hd
   end;
 

--- a/src/Pure/Isar/isar_syn.ML	Wed Dec 03 15:26:46 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Dec 03 15:27:41 2008 +0100
@@ -403,7 +403,7 @@
     "prove sublocale relation between a locale and a locale expression" K.thy_goal
     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
       >> (fn (loc, expr) =>
-        Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd (K I) loc expr))));
+        Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
 
 val _ =
   OuterSyntax.command "interpretation"

--- a/src/Pure/Isar/new_locale.ML	Wed Dec 03 15:26:46 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Wed Dec 03 15:27:41 2008 +0100
@@ -1,5 +1,4 @@
-(*  Title:      Pure/Isar/expression.ML
-    ID:         $Id$
+(*  Title:      Pure/Isar/new_locale.ML
     Author:     Clemens Ballarin, TU Muenchen
 
 New locale development --- experimental.
@@ -7,11 +6,9 @@
 
 signature NEW_LOCALE =
 sig
-  type identifiers
-  val empty: identifiers
-
   type locale
 
+  val clear_idents: Proof.context -> Proof.context
   val test_locale: theory -> string -> bool
   val register_locale: string ->
     (string * sort) list * (Name.binding * typ option * mixfix) list ->
@@ -39,9 +36,9 @@
 
   (* Activation *)
   val activate_declarations: theory -> string * Morphism.morphism ->
-    identifiers * Proof.context -> identifiers * Proof.context
+    Proof.context -> Proof.context
   val activate_facts: theory -> string * Morphism.morphism ->
-    identifiers * Proof.context -> identifiers * Proof.context
+    Proof.context -> Proof.context
 (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
   val init: string -> theory -> Proof.context
 
@@ -57,6 +54,8 @@
 end;
 
 
+(*** Theorem list extensible via attribute --- to control intro_locales_tac ***)
+
 (* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
 functor ThmsFun() =
 struct
@@ -184,15 +183,36 @@
 
 (*** Activate context elements of locale ***)
 
-(** Resolve locale dependencies in a depth-first fashion **)
+(** Identifiers: activated locales in theory or proof context **)
 
 type identifiers = (string * term list) list;
 
 val empty = ([] : identifiers);
 
+fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
+
 local
 
-fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
+structure IdentifiersData = GenericDataFun
+(
+  type T = identifiers;
+  val empty = empty;
+  val extend = I;
+  fun merge _ = Library.merge (op =);  (* FIXME cannot do this properly without theory context *)
+);
+
+in
+
+val get_idents = IdentifiersData.get o Context.Proof;
+val put_idents = Context.proof_map o IdentifiersData.put;
+val clear_idents = put_idents empty;
+
+end;
+
+
+(** Resolve locale dependencies in a depth-first fashion **)
+
+local
 
 val roundup_bound = 120;
 
@@ -220,18 +240,17 @@
 
 in
 
-fun roundup thy activate_dep (name, morph) (marked, ctxt) =
+fun roundup thy activate_dep (name, morph) (marked, input) =
   let
-    val Loc {dependencies, ...} = the_locale thy name;
     val (dependencies', marked') = add thy 0 (name, morph) ([], marked);
   in
-    (marked', ctxt |> fold_rev (activate_dep thy) dependencies')
+    (marked', input |> fold_rev (activate_dep thy) dependencies')
   end;
 
 end;
 
 
-(* Declarations and facts *)
+(* Declarations, facts and entire locale content *)
 
 fun activate_decls thy (name, morph) ctxt =
   let
@@ -252,10 +271,7 @@
     fold_rev activate notes input
   end;
 
-
-(* Entire locale content *)
-
-fun activate name thy activ_elem input =
+fun activate_all name thy activ_elem (marked, input) =
   let
     val Loc {parameters = (_, params), spec = (asm, defs), dependencies, ...} =
       the_locale thy name;
@@ -267,7 +283,7 @@
       (if not (null defs)
         then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
         else I) |>
-      pair empty |> roundup thy (activate_notes activ_elem) (name, Morphism.identity) |> snd
+      pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity)
   end;
 
 
@@ -302,11 +318,14 @@
 
 in
 
-fun activate_declarations thy = roundup thy activate_decls;
+fun activate_declarations thy dep ctxt =
+  roundup thy activate_decls dep (get_idents ctxt, ctxt) |> uncurry put_idents;
+  
+fun activate_facts thy dep ctxt =
+  roundup thy (activate_notes init_elem) dep (get_idents ctxt, ctxt) |> uncurry put_idents;
 
-fun activate_facts thy = roundup thy (activate_notes init_elem);
-
-fun init name thy = activate name thy init_elem (ProofContext.init thy);
+fun init name thy = activate_all name thy init_elem (empty, ProofContext.init thy) |>
+  uncurry put_idents;
 
 fun print_locale thy show_facts name =
   let
@@ -314,7 +333,7 @@
     val ctxt = init name' thy
   in
     Pretty.big_list "locale elements:"
-      (activate name' thy (cons_elem show_facts) [] |> rev |> 
+      (activate_all name' thy (cons_elem show_facts) (empty, []) |> snd |> rev |> 
         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   end