1.1 --- a/etc/isar-keywords-ZF.el	Wed Mar 21 21:24:13 2012 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Wed Mar 21 23:26:35 2012 +0100
     1.3 @@ -45,7 +45,6 @@
     1.4      "commit"
     1.5      "consts"
     1.6      "context"
     1.7 -    "context_includes"
     1.8      "corollary"
     1.9      "datatype"
    1.10      "declaration"
    1.11 @@ -227,6 +226,7 @@
    1.12      "if"
    1.13      "imports"
    1.14      "in"
    1.15 +    "includes"
    1.16      "induction"
    1.17      "infix"
    1.18      "infixl"
    1.19 @@ -357,7 +357,6 @@
    1.20      "coinductive"
    1.21      "consts"
    1.22      "context"
    1.23 -    "context_includes"
    1.24      "datatype"
    1.25      "declaration"
    1.26      "declare"

     2.1 --- a/etc/isar-keywords.el	Wed Mar 21 21:24:13 2012 +0100
     2.2 +++ b/etc/isar-keywords.el	Wed Mar 21 23:26:35 2012 +0100
     2.3 @@ -64,7 +64,6 @@
     2.4      "commit"
     2.5      "consts"
     2.6      "context"
     2.7 -    "context_includes"
     2.8      "corollary"
     2.9      "cpodef"
    2.10      "datatype"
    2.11 @@ -306,6 +305,7 @@
    2.12      "if"
    2.13      "imports"
    2.14      "in"
    2.15 +    "includes"
    2.16      "infix"
    2.17      "infixl"
    2.18      "infixr"
    2.19 @@ -471,7 +471,6 @@
    2.20      "coinductive_set"
    2.21      "consts"
    2.22      "context"
    2.23 -    "context_includes"
    2.24      "datatype"
    2.25      "declaration"
    2.26      "declare"

     3.1 --- a/src/Pure/Isar/bundle.ML	Wed Mar 21 21:24:13 2012 +0100
     3.2 +++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 23:26:35 2012 +0100
     3.3 @@ -15,12 +15,12 @@
     3.4      (binding * string option * mixfix) list -> local_theory -> local_theory
     3.5    val includes: string list -> Proof.context -> Proof.context
     3.6    val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
     3.7 +  val context_includes: string list -> generic_theory -> local_theory
     3.8 +  val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory
     3.9    val include_: string list -> Proof.state -> Proof.state
    3.10    val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    3.11    val including: string list -> Proof.state -> Proof.state
    3.12    val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    3.13 -  val context_includes: string list -> local_theory -> local_theory
    3.14 -  val context_includes_cmd: (xstring * Position.T) list -> local_theory -> local_theory
    3.15    val print_bundles: Proof.context -> unit
    3.16  end;
    3.17  
    3.18 @@ -93,16 +93,22 @@
    3.19      val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
    3.20    in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
    3.21  
    3.22 -fun gen_context prep args lthy =
    3.23 -  Named_Target.assert lthy
    3.24 -  |> gen_includes prep args
    3.25 -  |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
    3.26 +fun gen_context prep args (Context.Theory thy) =
    3.27 +      Named_Target.theory_init thy
    3.28 +      |> Local_Theory.target (gen_includes prep args)
    3.29 +  | gen_context prep args (Context.Proof lthy) =
    3.30 +      Named_Target.assert lthy
    3.31 +      |> gen_includes prep args
    3.32 +      |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
    3.33  
    3.34  in
    3.35  
    3.36  val includes = gen_includes (K I);
    3.37  val includes_cmd = gen_includes check;
    3.38  
    3.39 +val context_includes = gen_context (K I);
    3.40 +val context_includes_cmd = gen_context check;
    3.41 +
    3.42  fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
    3.43  fun include_cmd bs =
    3.44    Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
    3.45 @@ -110,9 +116,6 @@
    3.46  fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
    3.47  fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
    3.48  
    3.49 -val context_includes = gen_context (K I);
    3.50 -val context_includes_cmd = gen_context check;
    3.51 -
    3.52  end;
    3.53  
    3.54  

     4.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Mar 21 21:24:13 2012 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 21 23:26:35 2012 +0100
     4.3 @@ -25,16 +25,17 @@
     4.4  (** init and exit **)
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory"
     4.8 +  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
     4.9      (Thy_Header.args >> (fn header =>
    4.10        Toplevel.print o
    4.11          Toplevel.init_theory
    4.12            (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
    4.13  
    4.14  val _ =
    4.15 -  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end (local) theory"
    4.16 +  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end context"
    4.17      (Scan.succeed
    4.18 -      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
    4.19 +      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
    4.20 +        Toplevel.end_proof (K Proof.end_notepad)));
    4.21  
    4.22  
    4.23  
    4.24 @@ -406,14 +407,6 @@
    4.25        (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
    4.26  
    4.27  
    4.28 -(* local theories *)
    4.29 -
    4.30 -val _ =
    4.31 -  Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
    4.32 -    (Parse.position Parse.xname --| Parse.begin >> (fn name =>
    4.33 -      Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
    4.34 -
    4.35 -
    4.36  (* bundled declarations *)
    4.37  
    4.38  val _ =
    4.39 @@ -434,17 +427,21 @@
    4.40        >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
    4.41  
    4.42  val _ =
    4.43 -  Outer_Syntax.local_theory ("context_includes", Keyword.thy_decl)  (* FIXME 'context' 'includes' *)
    4.44 -    "nested target context including bundled declarations"
    4.45 -    (Scan.repeat1 (Parse.position Parse.xname) --| Parse.begin
    4.46 -      >> Bundle.context_includes_cmd);
    4.47 -
    4.48 -val _ =
    4.49    Outer_Syntax.improper_command ("print_bundles", Keyword.diag) "print bundles of declarations"
    4.50      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    4.51        Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
    4.52  
    4.53  
    4.54 +(* local theories *)
    4.55 +
    4.56 +val _ =
    4.57 +  Outer_Syntax.command ("context", Keyword.thy_decl) "begin local theory context"
    4.58 +    ((Parse_Spec.includes >> (Toplevel.open_target o Bundle.context_includes_cmd) ||
    4.59 +      Parse.position Parse.xname >> (fn name =>
    4.60 +        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)))
    4.61 +      --| Parse.begin);
    4.62 +
    4.63 +
    4.64  (* locales *)
    4.65  
    4.66  val locale_val =
    4.67 @@ -567,8 +564,7 @@
    4.68  val _ = gen_theorem true Thm.corollaryK;
    4.69  
    4.70  val _ =
    4.71 -  Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl)
    4.72 -    "Isar proof state as formal notepad, without any result"
    4.73 +  Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl) "begin proof context"
    4.74      (Parse.begin >> K Proof.begin_notepad);
    4.75  
    4.76  val _ =

     5.1 --- a/src/Pure/Isar/named_target.ML	Wed Mar 21 21:24:13 2012 +0100
     5.2 +++ b/src/Pure/Isar/named_target.ML	Wed Mar 21 23:26:35 2012 +0100
     5.3 @@ -215,7 +215,7 @@
     5.4  val theory_init = init I "";
     5.5  
     5.6  val reinit =
     5.7 -  assert #> Data.get #> the #>
     5.8 +  Local_Theory.assert_bottom true #> Data.get #> the #>
     5.9    (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
    5.10  
    5.11  fun context_cmd ("-", _) thy = init I "" thy

     6.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 21 21:24:13 2012 +0100
     6.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 21 23:26:35 2012 +0100
     6.3 @@ -58,6 +58,8 @@
     6.4    val theory': (bool -> theory -> theory) -> transition -> transition
     6.5    val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
     6.6    val end_local_theory: transition -> transition
     6.7 +  val open_target: (generic_theory -> local_theory) -> transition -> transition
     6.8 +  val close_target: transition -> transition
     6.9    val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
    6.10      transition -> transition
    6.11    val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
    6.12 @@ -105,7 +107,7 @@
    6.13  (* local theory wrappers *)
    6.14  
    6.15  val loc_init = Named_Target.context_cmd;
    6.16 -val loc_exit = Local_Theory.exit_global;
    6.17 +val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
    6.18  
    6.19  fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
    6.20    | loc_begin NONE (Context.Proof lthy) = lthy
    6.21 @@ -456,6 +458,20 @@
    6.22    (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
    6.23      | _ => raise UNDEF));
    6.24  
    6.25 +fun open_target f = transaction (fn _ =>
    6.26 +  (fn Theory (gthy, _) =>
    6.27 +        let val lthy = f gthy
    6.28 +        in Theory (Context.Proof lthy, SOME lthy) end
    6.29 +    | _ => raise UNDEF));
    6.30 +
    6.31 +val close_target = transaction (fn _ =>
    6.32 +  (fn Theory (Context.Proof lthy, _) =>
    6.33 +        (case try Local_Theory.close_target lthy of
    6.34 +          SOME lthy' => Theory (Context.Proof lthy', SOME lthy)
    6.35 +        | NONE => raise UNDEF)
    6.36 +    | _ => raise UNDEF));
    6.37 +
    6.38 +
    6.39  local
    6.40  
    6.41  fun local_theory_presentation loc f = present_transaction (fn int =>