1.1 --- a/src/Pure/Isar/bundle.ML	Sun Apr 01 21:45:25 2012 +0200
     1.2 +++ b/src/Pure/Isar/bundle.ML	Sun Apr 01 21:46:45 2012 +0200
     1.3 @@ -15,12 +15,13 @@
     1.4      (binding * string option * mixfix) list -> local_theory -> local_theory
     1.5    val includes: string list -> Proof.context -> Proof.context
     1.6    val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
     1.7 -  val context_includes: string list -> generic_theory -> local_theory
     1.8 -  val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory
     1.9    val include_: string list -> Proof.state -> Proof.state
    1.10    val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    1.11    val including: string list -> Proof.state -> Proof.state
    1.12    val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    1.13 +  val context: string list -> Element.context_i list -> generic_theory -> local_theory
    1.14 +  val context_cmd: (xstring * Position.T) list -> Element.context list ->
    1.15 +    generic_theory -> local_theory
    1.16    val print_bundles: Proof.context -> unit
    1.17  end;
    1.18  
    1.19 @@ -90,23 +91,23 @@
    1.20    let val decls = maps (the_bundle ctxt o prep ctxt) args
    1.21    in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
    1.22  
    1.23 -fun gen_context prep args (Context.Theory thy) =
    1.24 -      Named_Target.theory_init thy
    1.25 -      |> Local_Theory.target (gen_includes prep args)
    1.26 -      |> Local_Theory.restore
    1.27 -  | gen_context prep args (Context.Proof lthy) =
    1.28 -      Local_Theory.assert lthy
    1.29 -      |> gen_includes prep args
    1.30 -      |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
    1.31 +fun gen_context prep_bundle prep_stmt raw_incls raw_elems gthy =
    1.32 +  let
    1.33 +    val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
    1.34 +    val augment = gen_includes prep_bundle raw_incls #> prep_stmt raw_elems [] #> snd;
    1.35 +  in
    1.36 +    (case gthy of
    1.37 +      Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
    1.38 +    | Context.Proof _ =>
    1.39 +        augment lthy |>
    1.40 +        Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy))
    1.41 +  end;
    1.42  
    1.43  in
    1.44  
    1.45  val includes = gen_includes (K I);
    1.46  val includes_cmd = gen_includes check;
    1.47  
    1.48 -val context_includes = gen_context (K I);
    1.49 -val context_includes_cmd = gen_context check;
    1.50 -
    1.51  fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
    1.52  fun include_cmd bs =
    1.53    Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
    1.54 @@ -114,6 +115,9 @@
    1.55  fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
    1.56  fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
    1.57  
    1.58 +val context = gen_context (K I) Expression.cert_statement;
    1.59 +val context_cmd = gen_context check Expression.read_statement;
    1.60 +
    1.61  end;
    1.62  
    1.63  

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Apr 01 21:45:25 2012 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 01 21:46:45 2012 +0200
     2.3 @@ -436,9 +436,10 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command ("context", Keyword.thy_decl) "begin local theory context"
     2.7 -    ((Parse_Spec.includes >> (Toplevel.open_target o Bundle.context_includes_cmd) ||
     2.8 -      Parse.position Parse.xname >> (fn name =>
     2.9 -        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)))
    2.10 +    ((Parse.position Parse.xname >> (fn name =>
    2.11 +        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
    2.12 +      Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
    2.13 +        >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
    2.14        --| Parse.begin);
    2.15  
    2.16