more general context command with auxiliary fixes/assumes etc.;

--- a/src/Pure/Isar/bundle.ML	Sun Apr 01 21:45:25 2012 +0200
+++ b/src/Pure/Isar/bundle.ML	Sun Apr 01 21:46:45 2012 +0200
@@ -15,12 +15,13 @@
     (binding * string option * mixfix) list -> local_theory -> local_theory
   val includes: string list -> Proof.context -> Proof.context
   val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
-  val context_includes: string list -> generic_theory -> local_theory
-  val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory
   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: string list -> Element.context_i list -> generic_theory -> local_theory
+  val context_cmd: (xstring * Position.T) list -> Element.context list ->
+    generic_theory -> local_theory
   val print_bundles: Proof.context -> unit
 end;
 
@@ -90,23 +91,23 @@
   let val decls = maps (the_bundle ctxt o prep ctxt) args
   in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
 
-fun gen_context prep args (Context.Theory thy) =
-      Named_Target.theory_init thy
-      |> Local_Theory.target (gen_includes prep args)
-      |> Local_Theory.restore
-  | gen_context prep args (Context.Proof lthy) =
-      Local_Theory.assert lthy
-      |> gen_includes prep args
-      |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
+fun gen_context prep_bundle prep_stmt raw_incls raw_elems gthy =
+  let
+    val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
+    val augment = gen_includes prep_bundle raw_incls #> prep_stmt raw_elems [] #> snd;
+  in
+    (case gthy of
+      Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
+    | Context.Proof _ =>
+        augment lthy |>
+        Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy))
+  end;
 
 in
 
 val includes = gen_includes (K I);
 val includes_cmd = gen_includes check;
 
-val context_includes = gen_context (K I);
-val context_includes_cmd = gen_context check;
-
 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
 fun include_cmd bs =
   Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
@@ -114,6 +115,9 @@
 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
 
+val context = gen_context (K I) Expression.cert_statement;
+val context_cmd = gen_context check Expression.read_statement;
+
 end;
 
 

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