more explicit Toplevel.open_target/close_target;
replaced 'context_includes' by 'context' 'includes';
tuned command descriptions;
--- 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"
--- 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"
--- 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;
--- 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 _ =
--- 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
--- 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 =>