# HG changeset patch
# User wenzelm
# Date 1332347135 -3600
# Node ID 8a6124d09ff5bbdf549a3ec7ca7ff19080ed8d6c
# Parent  cce369d41d506f5a2d1e4362dfba8cb94ed2820d
basic support for nested contexts including bundles;
include multiple bundles;
renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML);
tuned signatures;

diff -r cce369d41d50 -r 8a6124d09ff5 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Mar 21 17:16:39 2012 +0100
+++ b/etc/isar-keywords-ZF.el	Wed Mar 21 17:25:35 2012 +0100
@@ -45,6 +45,7 @@
     "commit"
     "consts"
     "context"
+    "context_includes"
     "corollary"
     "datatype"
     "declaration"
@@ -356,6 +357,7 @@
     "coinductive"
     "consts"
     "context"
+    "context_includes"
     "datatype"
     "declaration"
     "declare"
diff -r cce369d41d50 -r 8a6124d09ff5 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Mar 21 17:16:39 2012 +0100
+++ b/etc/isar-keywords.el	Wed Mar 21 17:25:35 2012 +0100
@@ -64,6 +64,7 @@
     "commit"
     "consts"
     "context"
+    "context_includes"
     "corollary"
     "cpodef"
     "datatype"
@@ -470,6 +471,7 @@
     "coinductive_set"
     "consts"
     "context"
+    "context_includes"
     "datatype"
     "declaration"
     "declare"
diff -r cce369d41d50 -r 8a6124d09ff5 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Wed Mar 21 17:16:39 2012 +0100
+++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 17:25:35 2012 +0100
@@ -13,10 +13,12 @@
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
-  val include_: string -> Proof.state -> Proof.state
-  val include_cmd: xstring * Position.T -> Proof.state -> Proof.state
-  val including: string -> Proof.state -> Proof.state
-  val including_cmd: xstring * Position.T -> Proof.state -> Proof.state
+  val include_: string list -> Proof.state -> Proof.state
+  val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+  val including: string list -> Proof.state -> Proof.state
+  val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+  val context_includes: string list -> local_theory -> local_theory
+  val context_includes_cmd: (xstring * Position.T) list -> local_theory -> local_theory
   val print_bundles: Proof.context -> unit
 end;
 
@@ -78,20 +80,36 @@
 end;
 
 
-(* include bundle *)
+(* include bundles *)
+
+local
+
+fun gen_include prep raw_names ctxt =
+  let
+    val bundle = maps (the_bundle ctxt o prep ctxt) raw_names;
+    val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
+    val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
+  in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
 
-fun gen_include prep raw_name =
-  Proof.map_context (fn ctxt =>
-    let
-      val bundle = the_bundle ctxt (prep ctxt raw_name);
-      val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
-      val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
-    in #2 (Proof_Context.note_thmss "" [note] ctxt) end);
+fun gen_includes prep raw_names lthy =
+  Named_Target.assert lthy
+  |> gen_include prep raw_names
+  |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
+
+in
 
-fun include_ name = Proof.assert_forward #> gen_include (K I) name #> Proof.put_facts NONE;
-fun include_cmd name = Proof.assert_forward #> gen_include check name #> Proof.put_facts NONE;
-fun including name = Proof.assert_backward #> gen_include (K I) name;
-fun including_cmd name = Proof.assert_backward #> gen_include check name;
+fun include_ names =
+  Proof.assert_forward #> Proof.map_context (gen_include (K I) names) #> Proof.put_facts NONE;
+fun include_cmd names =
+  Proof.assert_forward #> Proof.map_context (gen_include check names) #> Proof.put_facts NONE;
+
+fun including names = Proof.assert_backward #> Proof.map_context (gen_include (K I) names);
+fun including_cmd names = Proof.assert_backward #> Proof.map_context (gen_include check names);
+
+val context_includes = gen_includes (K I);
+val context_includes_cmd = gen_includes check;
+
+end;
 
 
 (* print_bundles *)
diff -r cce369d41d50 -r 8a6124d09ff5 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 21 17:16:39 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 21 17:25:35 2012 +0100
@@ -424,12 +424,20 @@
 val _ =
   Outer_Syntax.command ("include", Keyword.prf_decl)
     "include declarations from bundle in proof body"
-    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
+    (Scan.repeat1 (Parse.position Parse.xname)
+      >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
 
 val _ =
   Outer_Syntax.command ("including", Keyword.prf_decl)
     "include declarations from bundle in goal refinement"
-    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
+    (Scan.repeat1 (Parse.position Parse.xname)
+      >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
+
+val _ =
+  Outer_Syntax.local_theory ("context_includes", Keyword.thy_decl)  (* FIXME 'context' 'includes' *)
+    "nested target context including bundled declarations"
+    (Scan.repeat1 (Parse.position Parse.xname) --| Parse.begin
+      >> Bundle.context_includes_cmd);
 
 val _ =
   Outer_Syntax.improper_command ("print_bundles", Keyword.diag) "print bundles of declarations"
diff -r cce369d41d50 -r 8a6124d09ff5 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Mar 21 17:16:39 2012 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Mar 21 17:25:35 2012 +0100
@@ -10,9 +10,10 @@
 signature LOCAL_THEORY =
 sig
   type operations
+  val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
+  val assert: local_theory -> local_theory
   val level: Proof.context -> int
-  val affirm: local_theory -> local_theory
-  val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
+  val assert_bottom: bool -> local_theory -> local_theory
   val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
   val close_target: local_theory -> local_theory
   val naming_of: local_theory -> Name_Space.naming
@@ -33,6 +34,7 @@
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
   val global_morphism: local_theory -> morphism
+  val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -96,31 +98,39 @@
   fun init _ = [];
 );
 
-val level = length o Data.get;
-
-fun affirm lthy =
-  if level lthy > 0 then lthy
-  else error "Missing local theory context";
-
-val get_lthy = hd o Data.get o affirm;
-
-fun map_lthy f = affirm #>
-  Data.map (fn {naming, operations, target} :: parents =>
-    make_lthy (f (naming, operations, target)) :: parents);
-
 fun map_contexts f =
   (Data.map o map) (fn {naming, operations, target} => make_lthy (naming, operations, f target))
   #> f;
 
+fun assert lthy =
+  if null (Data.get lthy) then error "Missing local theory context" else lthy;
+
+val get_lthy = hd o Data.get o assert;
+
+fun map_lthy f = assert #>
+  Data.map (fn {naming, operations, target} :: parents =>
+    make_lthy (f (naming, operations, target)) :: parents);
+
 
 (* nested structure *)
 
-fun open_target naming operations target = affirm target
+val level = length o Data.get;
+
+fun assert_bottom b lthy =
+  let
+    val _ = assert lthy;
+    val b' = level lthy <= 1;
+  in
+    if b andalso not b' then error "Not at bottom of local theory nesting"
+    else if not b andalso b' then error "Already at bottom of local theory nesting"
+    else lthy
+  end;
+
+fun open_target naming operations target = assert target
   |> Data.map (cons (make_lthy (naming, operations, target)));
 
 fun close_target lthy =
-  if level lthy >= 2 then Data.map tl lthy
-  else error "Unbalanced local theory targets";
+  assert_bottom false lthy |> Data.map tl;
 
 
 (* naming *)
@@ -205,9 +215,12 @@
 
 (** operations **)
 
+val operations_of = #operations o get_lthy;
+
+
 (* primitives *)
 
-fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
+fun operation f lthy = f (operations_of lthy) lthy;
 fun operation2 f x y = operation (fn ops => f ops x y);
 
 val pretty = operation #pretty;
diff -r cce369d41d50 -r 8a6124d09ff5 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Mar 21 17:16:39 2012 +0100
+++ b/src/Pure/Isar/named_target.ML	Wed Mar 21 17:25:35 2012 +0100
@@ -2,16 +2,17 @@
     Author:     Makarius
     Author:     Florian Haftmann, TU Muenchen
 
-Targets for theory, locale and class.
+Targets for theory, locale, class -- at the bottom the nested structure.
 *)
 
 signature NAMED_TARGET =
 sig
+  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
+  val assert: local_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 * Position.T -> theory -> local_theory
-  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
 end;
 
 structure Named_Target: NAMED_TARGET =
@@ -43,6 +44,10 @@
   Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
     {target = target, is_locale = is_locale, is_class = is_class});
 
+fun assert lthy =
+  if is_some (peek lthy) then lthy
+  else error "Not in a named target (global theory, locale, class)";
+
 
 (* generic declarations *)
 
@@ -209,11 +214,9 @@
 
 val theory_init = init I "";
 
-fun reinit lthy =
-  (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");
+val reinit =
+  assert #> Data.get #> the #>
+  (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
 
 fun context_cmd ("-", _) thy = init I "" thy
   | context_cmd target thy = init I (Locale.check thy target) thy;
diff -r cce369d41d50 -r 8a6124d09ff5 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Mar 21 17:16:39 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Mar 21 17:25:35 2012 +0100
@@ -381,7 +381,7 @@
 fun gen_theorem schematic prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
   let
-    val _ = Local_Theory.affirm lthy;
+    val _ = Local_Theory.assert lthy;
     val thy = Proof_Context.theory_of lthy;
 
     val attrib = prep_att thy;