1.1 --- a/etc/isar-keywords-ZF.el	Wed Mar 21 17:16:39 2012 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Wed Mar 21 17:25:35 2012 +0100
     1.3 @@ -45,6 +45,7 @@
     1.4      "commit"
     1.5      "consts"
     1.6      "context"
     1.7 +    "context_includes"
     1.8      "corollary"
     1.9      "datatype"
    1.10      "declaration"
    1.11 @@ -356,6 +357,7 @@
    1.12      "coinductive"
    1.13      "consts"
    1.14      "context"
    1.15 +    "context_includes"
    1.16      "datatype"
    1.17      "declaration"
    1.18      "declare"

     2.1 --- a/etc/isar-keywords.el	Wed Mar 21 17:16:39 2012 +0100
     2.2 +++ b/etc/isar-keywords.el	Wed Mar 21 17:25:35 2012 +0100
     2.3 @@ -64,6 +64,7 @@
     2.4      "commit"
     2.5      "consts"
     2.6      "context"
     2.7 +    "context_includes"
     2.8      "corollary"
     2.9      "cpodef"
    2.10      "datatype"
    2.11 @@ -470,6 +471,7 @@
    2.12      "coinductive_set"
    2.13      "consts"
    2.14      "context"
    2.15 +    "context_includes"
    2.16      "datatype"
    2.17      "declaration"
    2.18      "declare"

     3.1 --- a/src/Pure/Isar/bundle.ML	Wed Mar 21 17:16:39 2012 +0100
     3.2 +++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 17:25:35 2012 +0100
     3.3 @@ -13,10 +13,12 @@
     3.4      (binding * typ option * mixfix) list -> local_theory -> local_theory
     3.5    val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
     3.6      (binding * string option * mixfix) list -> local_theory -> local_theory
     3.7 -  val include_: string -> Proof.state -> Proof.state
     3.8 -  val include_cmd: xstring * Position.T -> Proof.state -> Proof.state
     3.9 -  val including: string -> Proof.state -> Proof.state
    3.10 -  val including_cmd: xstring * Position.T -> Proof.state -> Proof.state
    3.11 +  val include_: string list -> Proof.state -> Proof.state
    3.12 +  val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    3.13 +  val including: string list -> Proof.state -> Proof.state
    3.14 +  val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    3.15 +  val context_includes: string list -> local_theory -> local_theory
    3.16 +  val context_includes_cmd: (xstring * Position.T) list -> local_theory -> local_theory
    3.17    val print_bundles: Proof.context -> unit
    3.18  end;
    3.19  
    3.20 @@ -78,20 +80,36 @@
    3.21  end;
    3.22  
    3.23  
    3.24 -(* include bundle *)
    3.25 +(* include bundles *)
    3.26  
    3.27 -fun gen_include prep raw_name =
    3.28 -  Proof.map_context (fn ctxt =>
    3.29 -    let
    3.30 -      val bundle = the_bundle ctxt (prep ctxt raw_name);
    3.31 -      val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
    3.32 -      val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
    3.33 -    in #2 (Proof_Context.note_thmss "" [note] ctxt) end);
    3.34 +local
    3.35  
    3.36 -fun include_ name = Proof.assert_forward #> gen_include (K I) name #> Proof.put_facts NONE;
    3.37 -fun include_cmd name = Proof.assert_forward #> gen_include check name #> Proof.put_facts NONE;
    3.38 -fun including name = Proof.assert_backward #> gen_include (K I) name;
    3.39 -fun including_cmd name = Proof.assert_backward #> gen_include check name;
    3.40 +fun gen_include prep raw_names ctxt =
    3.41 +  let
    3.42 +    val bundle = maps (the_bundle ctxt o prep ctxt) raw_names;
    3.43 +    val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
    3.44 +    val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
    3.45 +  in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
    3.46 +
    3.47 +fun gen_includes prep raw_names lthy =
    3.48 +  Named_Target.assert lthy
    3.49 +  |> gen_include prep raw_names
    3.50 +  |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
    3.51 +
    3.52 +in
    3.53 +
    3.54 +fun include_ names =
    3.55 +  Proof.assert_forward #> Proof.map_context (gen_include (K I) names) #> Proof.put_facts NONE;
    3.56 +fun include_cmd names =
    3.57 +  Proof.assert_forward #> Proof.map_context (gen_include check names) #> Proof.put_facts NONE;
    3.58 +
    3.59 +fun including names = Proof.assert_backward #> Proof.map_context (gen_include (K I) names);
    3.60 +fun including_cmd names = Proof.assert_backward #> Proof.map_context (gen_include check names);
    3.61 +
    3.62 +val context_includes = gen_includes (K I);
    3.63 +val context_includes_cmd = gen_includes check;
    3.64 +
    3.65 +end;
    3.66  
    3.67  
    3.68  (* print_bundles *)

     4.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Mar 21 17:16:39 2012 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 21 17:25:35 2012 +0100
     4.3 @@ -424,12 +424,20 @@
     4.4  val _ =
     4.5    Outer_Syntax.command ("include", Keyword.prf_decl)
     4.6      "include declarations from bundle in proof body"
     4.7 -    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
     4.8 +    (Scan.repeat1 (Parse.position Parse.xname)
     4.9 +      >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
    4.10  
    4.11  val _ =
    4.12    Outer_Syntax.command ("including", Keyword.prf_decl)
    4.13      "include declarations from bundle in goal refinement"
    4.14 -    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
    4.15 +    (Scan.repeat1 (Parse.position Parse.xname)
    4.16 +      >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
    4.17 +
    4.18 +val _ =
    4.19 +  Outer_Syntax.local_theory ("context_includes", Keyword.thy_decl)  (* FIXME 'context' 'includes' *)
    4.20 +    "nested target context including bundled declarations"
    4.21 +    (Scan.repeat1 (Parse.position Parse.xname) --| Parse.begin
    4.22 +      >> Bundle.context_includes_cmd);
    4.23  
    4.24  val _ =
    4.25    Outer_Syntax.improper_command ("print_bundles", Keyword.diag) "print bundles of declarations"

     5.1 --- a/src/Pure/Isar/local_theory.ML	Wed Mar 21 17:16:39 2012 +0100
     5.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Mar 21 17:25:35 2012 +0100
     5.3 @@ -10,9 +10,10 @@
     5.4  signature LOCAL_THEORY =
     5.5  sig
     5.6    type operations
     5.7 +  val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
     5.8 +  val assert: local_theory -> local_theory
     5.9    val level: Proof.context -> int
    5.10 -  val affirm: local_theory -> local_theory
    5.11 -  val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
    5.12 +  val assert_bottom: bool -> local_theory -> local_theory
    5.13    val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
    5.14    val close_target: local_theory -> local_theory
    5.15    val naming_of: local_theory -> Name_Space.naming
    5.16 @@ -33,6 +34,7 @@
    5.17    val standard_morphism: local_theory -> Proof.context -> morphism
    5.18    val target_morphism: local_theory -> morphism
    5.19    val global_morphism: local_theory -> morphism
    5.20 +  val operations_of: local_theory -> operations
    5.21    val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    5.22      (term * (string * thm)) * local_theory
    5.23    val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    5.24 @@ -96,31 +98,39 @@
    5.25    fun init _ = [];
    5.26  );
    5.27  
    5.28 -val level = length o Data.get;
    5.29 -
    5.30 -fun affirm lthy =
    5.31 -  if level lthy > 0 then lthy
    5.32 -  else error "Missing local theory context";
    5.33 -
    5.34 -val get_lthy = hd o Data.get o affirm;
    5.35 -
    5.36 -fun map_lthy f = affirm #>
    5.37 -  Data.map (fn {naming, operations, target} :: parents =>
    5.38 -    make_lthy (f (naming, operations, target)) :: parents);
    5.39 -
    5.40  fun map_contexts f =
    5.41    (Data.map o map) (fn {naming, operations, target} => make_lthy (naming, operations, f target))
    5.42    #> f;
    5.43  
    5.44 +fun assert lthy =
    5.45 +  if null (Data.get lthy) then error "Missing local theory context" else lthy;
    5.46 +
    5.47 +val get_lthy = hd o Data.get o assert;
    5.48 +
    5.49 +fun map_lthy f = assert #>
    5.50 +  Data.map (fn {naming, operations, target} :: parents =>
    5.51 +    make_lthy (f (naming, operations, target)) :: parents);
    5.52 +
    5.53  
    5.54  (* nested structure *)
    5.55  
    5.56 -fun open_target naming operations target = affirm target
    5.57 +val level = length o Data.get;
    5.58 +
    5.59 +fun assert_bottom b lthy =
    5.60 +  let
    5.61 +    val _ = assert lthy;
    5.62 +    val b' = level lthy <= 1;
    5.63 +  in
    5.64 +    if b andalso not b' then error "Not at bottom of local theory nesting"
    5.65 +    else if not b andalso b' then error "Already at bottom of local theory nesting"
    5.66 +    else lthy
    5.67 +  end;
    5.68 +
    5.69 +fun open_target naming operations target = assert target
    5.70    |> Data.map (cons (make_lthy (naming, operations, target)));
    5.71  
    5.72  fun close_target lthy =
    5.73 -  if level lthy >= 2 then Data.map tl lthy
    5.74 -  else error "Unbalanced local theory targets";
    5.75 +  assert_bottom false lthy |> Data.map tl;
    5.76  
    5.77  
    5.78  (* naming *)
    5.79 @@ -205,9 +215,12 @@
    5.80  
    5.81  (** operations **)
    5.82  
    5.83 +val operations_of = #operations o get_lthy;
    5.84 +
    5.85 +
    5.86  (* primitives *)
    5.87  
    5.88 -fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
    5.89 +fun operation f lthy = f (operations_of lthy) lthy;
    5.90  fun operation2 f x y = operation (fn ops => f ops x y);
    5.91  
    5.92  val pretty = operation #pretty;

     6.1 --- a/src/Pure/Isar/named_target.ML	Wed Mar 21 17:16:39 2012 +0100
     6.2 +++ b/src/Pure/Isar/named_target.ML	Wed Mar 21 17:25:35 2012 +0100
     6.3 @@ -2,16 +2,17 @@
     6.4      Author:     Makarius
     6.5      Author:     Florian Haftmann, TU Muenchen
     6.6  
     6.7 -Targets for theory, locale and class.
     6.8 +Targets for theory, locale, class -- at the bottom the nested structure.
     6.9  *)
    6.10  
    6.11  signature NAMED_TARGET =
    6.12  sig
    6.13 +  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
    6.14 +  val assert: local_theory -> local_theory
    6.15    val init: (local_theory -> local_theory) -> string -> theory -> local_theory
    6.16    val theory_init: theory -> local_theory
    6.17    val reinit: local_theory -> local_theory -> local_theory
    6.18    val context_cmd: xstring * Position.T -> theory -> local_theory
    6.19 -  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
    6.20  end;
    6.21  
    6.22  structure Named_Target: NAMED_TARGET =
    6.23 @@ -43,6 +44,10 @@
    6.24    Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
    6.25      {target = target, is_locale = is_locale, is_class = is_class});
    6.26  
    6.27 +fun assert lthy =
    6.28 +  if is_some (peek lthy) then lthy
    6.29 +  else error "Not in a named target (global theory, locale, class)";
    6.30 +
    6.31  
    6.32  (* generic declarations *)
    6.33  
    6.34 @@ -209,11 +214,9 @@
    6.35  
    6.36  val theory_init = init I "";
    6.37  
    6.38 -fun reinit lthy =
    6.39 -  (case Data.get lthy of
    6.40 -    SOME (Target {target, before_exit, ...}) =>
    6.41 -      init before_exit target o Local_Theory.exit_global
    6.42 -  | NONE => error "Not in a named target");
    6.43 +val reinit =
    6.44 +  assert #> Data.get #> the #>
    6.45 +  (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
    6.46  
    6.47  fun context_cmd ("-", _) thy = init I "" thy
    6.48    | context_cmd target thy = init I (Locale.check thy target) thy;

     7.1 --- a/src/Pure/Isar/specification.ML	Wed Mar 21 17:16:39 2012 +0100
     7.2 +++ b/src/Pure/Isar/specification.ML	Wed Mar 21 17:25:35 2012 +0100
     7.3 @@ -381,7 +381,7 @@
     7.4  fun gen_theorem schematic prep_att prep_stmt
     7.5      kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
     7.6    let
     7.7 -    val _ = Local_Theory.affirm lthy;
     7.8 +    val _ = Local_Theory.assert lthy;
     7.9      val thy = Proof_Context.theory_of lthy;
    7.10  
    7.11      val attrib = prep_att thy;