# HG changeset patch
# User wenzelm
# Date 1332368795 -3600
# Node ID 451fc10a81f3f9bc68583a34830c14730b799054
# Parent  2027ff3136cc82604f2b990965f474eaae50057b
more explicit Toplevel.open_target/close_target;
replaced 'context_includes' by 'context' 'includes';
tuned command descriptions;

diff -r 2027ff3136cc -r 451fc10a81f3 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Mar 21 21:24:13 2012 +0100
+++ b/etc/isar-keywords-ZF.el	Wed Mar 21 23:26:35 2012 +0100
@@ -45,7 +45,6 @@
     "commit"
     "consts"
     "context"
-    "context_includes"
     "corollary"
     "datatype"
     "declaration"
@@ -227,6 +226,7 @@
     "if"
     "imports"
     "in"
+    "includes"
     "induction"
     "infix"
     "infixl"
@@ -357,7 +357,6 @@
     "coinductive"
     "consts"
     "context"
-    "context_includes"
     "datatype"
     "declaration"
     "declare"
diff -r 2027ff3136cc -r 451fc10a81f3 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Mar 21 21:24:13 2012 +0100
+++ b/etc/isar-keywords.el	Wed Mar 21 23:26:35 2012 +0100
@@ -64,7 +64,6 @@
     "commit"
     "consts"
     "context"
-    "context_includes"
     "corollary"
     "cpodef"
     "datatype"
@@ -306,6 +305,7 @@
     "if"
     "imports"
     "in"
+    "includes"
     "infix"
     "infixl"
     "infixr"
@@ -471,7 +471,6 @@
     "coinductive_set"
     "consts"
     "context"
-    "context_includes"
     "datatype"
     "declaration"
     "declare"
diff -r 2027ff3136cc -r 451fc10a81f3 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Wed Mar 21 21:24:13 2012 +0100
+++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 23:26:35 2012 +0100
@@ -15,12 +15,12 @@
     (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_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;
 
@@ -93,16 +93,22 @@
     val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
   in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
 
-fun gen_context prep args lthy =
-  Named_Target.assert lthy
-  |> gen_includes prep args
-  |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
+fun gen_context prep args (Context.Theory thy) =
+      Named_Target.theory_init thy
+      |> Local_Theory.target (gen_includes prep args)
+  | gen_context prep args (Context.Proof lthy) =
+      Named_Target.assert lthy
+      |> gen_includes prep args
+      |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
 
 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;
@@ -110,9 +116,6 @@
 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_includes = gen_context (K I);
-val context_includes_cmd = gen_context check;
-
 end;
 
 
diff -r 2027ff3136cc -r 451fc10a81f3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 21 21:24:13 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 21 23:26:35 2012 +0100
@@ -25,16 +25,17 @@
 (** init and exit **)
 
 val _ =
-  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory"
+  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
     (Thy_Header.args >> (fn header =>
       Toplevel.print o
         Toplevel.init_theory
           (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
 
 val _ =
-  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end (local) theory"
+  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end context"
     (Scan.succeed
-      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
+      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+        Toplevel.end_proof (K Proof.end_notepad)));
 
 
 
@@ -406,14 +407,6 @@
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
 
-(* local theories *)
-
-val _ =
-  Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
-    (Parse.position Parse.xname --| Parse.begin >> (fn name =>
-      Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
-
-
 (* bundled declarations *)
 
 val _ =
@@ -434,17 +427,21 @@
       >> (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"
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
 
 
+(* local theories *)
+
+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.begin);
+
+
 (* locales *)
 
 val locale_val =
@@ -567,8 +564,7 @@
 val _ = gen_theorem true Thm.corollaryK;
 
 val _ =
-  Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl)
-    "Isar proof state as formal notepad, without any result"
+  Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl) "begin proof context"
     (Parse.begin >> K Proof.begin_notepad);
 
 val _ =
diff -r 2027ff3136cc -r 451fc10a81f3 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Mar 21 21:24:13 2012 +0100
+++ b/src/Pure/Isar/named_target.ML	Wed Mar 21 23:26:35 2012 +0100
@@ -215,7 +215,7 @@
 val theory_init = init I "";
 
 val reinit =
-  assert #> Data.get #> the #>
+  Local_Theory.assert_bottom true #> Data.get #> the #>
   (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
 
 fun context_cmd ("-", _) thy = init I "" thy
diff -r 2027ff3136cc -r 451fc10a81f3 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Mar 21 21:24:13 2012 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 21 23:26:35 2012 +0100
@@ -58,6 +58,8 @@
   val theory': (bool -> theory -> theory) -> transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
   val end_local_theory: transition -> transition
+  val open_target: (generic_theory -> local_theory) -> transition -> transition
+  val close_target: transition -> transition
   val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
     transition -> transition
   val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
@@ -105,7 +107,7 @@
 (* local theory wrappers *)
 
 val loc_init = Named_Target.context_cmd;
-val loc_exit = Local_Theory.exit_global;
+val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
   | loc_begin NONE (Context.Proof lthy) = lthy
@@ -456,6 +458,20 @@
   (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
     | _ => raise UNDEF));
 
+fun open_target f = transaction (fn _ =>
+  (fn Theory (gthy, _) =>
+        let val lthy = f gthy
+        in Theory (Context.Proof lthy, SOME lthy) end
+    | _ => raise UNDEF));
+
+val close_target = transaction (fn _ =>
+  (fn Theory (Context.Proof lthy, _) =>
+        (case try Local_Theory.close_target lthy of
+          SOME lthy' => Theory (Context.Proof lthy', SOME lthy)
+        | NONE => raise UNDEF)
+    | _ => raise UNDEF));
+
+
 local
 
 fun local_theory_presentation loc f = present_transaction (fn int =>