--- a/NEWS Fri Jun 10 17:12:14 2016 +0100
+++ b/NEWS Fri Jun 10 22:47:25 2016 +0200
@@ -45,6 +45,10 @@
declare b [intro]
end
+* Command 'unbundle' is like 'include', but works within a local theory
+context. Unlike "context includes ... begin", the effect of 'unbundle'
+on the target context persists, until different declarations are given.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Isar_Ref/Spec.thy Fri Jun 10 17:12:14 2016 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Jun 10 22:47:25 2016 +0200
@@ -253,9 +253,13 @@
\<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
current context; the ``\<open>!\<close>'' option indicates extra verbosity.
- \<^descr> \<^theory_text>\<open>include b\<^sub>1 \<dots> b\<^sub>n\<close> includes the declarations from the given bundles into
- the current proof body context. This is analogous to \<^theory_text>\<open>note\<close>
- (\secref{sec:proof-facts}) with the expanded bundles.
+ \<^descr> \<^theory_text>\<open>unbundle b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles in
+ the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close>
+ (\secref{sec:theorems}) with the expanded bundles.
+
+ \<^descr> \<^theory_text>\<open>include\<close> is similar to \<^theory_text>\<open>unbundle\<close>, but works in a proof body (forward
+ mode). This is analogous to \<^theory_text>\<open>note\<close> (\secref{sec:proof-facts}) with the
+ expanded bundles.
\<^descr> \<^theory_text>\<open>including\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof refinement
(backward mode). This is analogous to \<^theory_text>\<open>using\<close> (\secref{sec:proof-facts})
--- a/src/Pure/Isar/bundle.ML Fri Jun 10 17:12:14 2016 +0100
+++ b/src/Pure/Isar/bundle.ML Fri Jun 10 22:47:25 2016 +0200
@@ -15,6 +15,8 @@
val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
(binding * string option * mixfix) list -> local_theory -> local_theory
val init: binding -> theory -> local_theory
+ val unbundle: string list -> local_theory -> local_theory
+ val unbundle_cmd: (xstring * Position.T) 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 include_: string list -> Proof.state -> Proof.state
@@ -190,18 +192,20 @@
-(** include bundles **)
+(** activate bundles **)
local
-fun gen_includes get args ctxt =
+fun gen_activate notes get args ctxt =
let val decls = maps (get ctxt) args in
ctxt
|> Context_Position.set_visible false
- |> Attrib.local_notes "" [((Binding.empty, []), decls)] |> #2
+ |> notes [((Binding.empty, []), decls)] |> #2
|> Context_Position.restore_visible ctxt
end;
+fun gen_includes get = gen_activate (Attrib.local_notes "") get;
+
fun gen_context get prep_decl raw_incls raw_elems gthy =
let
val (after_close, lthy) =
@@ -217,6 +221,9 @@
in
+val unbundle = gen_activate Local_Theory.notes get_bundle;
+val unbundle_cmd = gen_activate Local_Theory.notes get_bundle_cmd;
+
val includes = gen_includes get_bundle;
val includes_cmd = gen_includes get_bundle_cmd;
--- a/src/Pure/Pure.thy Fri Jun 10 17:12:14 2016 +0100
+++ b/src/Pure/Pure.thy Fri Jun 10 22:47:25 2016 +0200
@@ -32,6 +32,7 @@
"parse_ast_translation" "parse_translation" "print_translation"
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
and "bundle" :: thy_decl_block
+ and "unbundle" :: thy_decl
and "include" "including" :: prf_decl
and "print_bundles" :: diag
and "context" "locale" "experiment" :: thy_decl_block
@@ -498,13 +499,18 @@
(Parse.binding --| Parse.begin >> Bundle.init);
val _ =
+ Outer_Syntax.local_theory @{command_keyword unbundle}
+ "activate declarations from bundle in local theory"
+ (Scan.repeat1 (Parse.position Parse.name) >> Bundle.unbundle_cmd);
+
+val _ =
Outer_Syntax.command @{command_keyword include}
- "include declarations from bundle in proof body"
+ "activate declarations from bundle in proof body"
(Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
val _ =
Outer_Syntax.command @{command_keyword including}
- "include declarations from bundle in goal refinement"
+ "activate declarations from bundle in goal refinement"
(Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
val _ =