--- a/etc/isar-keywords-ZF.el Tue Mar 20 18:42:45 2012 +0100
+++ b/etc/isar-keywords-ZF.el Tue Mar 20 21:37:31 2012 +0100
@@ -29,6 +29,7 @@
"axiomatization"
"axioms"
"back"
+ "bundle"
"by"
"cannot_undo"
"case"
@@ -76,6 +77,8 @@
"hide_const"
"hide_fact"
"hide_type"
+ "include"
+ "including"
"inductive"
"inductive_cases"
"init_toplevel"
@@ -120,6 +123,7 @@
"print_ast_translation"
"print_attributes"
"print_binds"
+ "print_bundles"
"print_cases"
"print_claset"
"print_classes"
@@ -287,6 +291,7 @@
"print_antiquotations"
"print_attributes"
"print_binds"
+ "print_bundles"
"print_cases"
"print_claset"
"print_classes"
@@ -342,6 +347,7 @@
"attribute_setup"
"axiomatization"
"axioms"
+ "bundle"
"class"
"classes"
"classrel"
@@ -458,6 +464,8 @@
(defconst isar-keywords-proof-decl
'("ML_prf"
"also"
+ "include"
+ "including"
"let"
"moreover"
"note"
--- a/etc/isar-keywords.el Tue Mar 20 18:42:45 2012 +0100
+++ b/etc/isar-keywords.el Tue Mar 20 21:37:31 2012 +0100
@@ -35,6 +35,7 @@
"boogie_open"
"boogie_status"
"boogie_vc"
+ "bundle"
"by"
"cannot_undo"
"case"
@@ -108,6 +109,8 @@
"hide_fact"
"hide_type"
"import_tptp"
+ "include"
+ "including"
"inductive"
"inductive_cases"
"inductive_set"
@@ -162,6 +165,7 @@
"print_ast_translation"
"print_attributes"
"print_binds"
+ "print_bundles"
"print_cases"
"print_claset"
"print_classes"
@@ -372,6 +376,7 @@
"print_antiquotations"
"print_attributes"
"print_binds"
+ "print_bundles"
"print_cases"
"print_claset"
"print_classes"
@@ -446,6 +451,7 @@
"axioms"
"boogie_end"
"boogie_open"
+ "bundle"
"class"
"classes"
"classrel"
@@ -613,6 +619,8 @@
(defconst isar-keywords-proof-decl
'("ML_prf"
"also"
+ "include"
+ "including"
"let"
"moreover"
"note"
--- a/src/Pure/IsaMakefile Tue Mar 20 18:42:45 2012 +0100
+++ b/src/Pure/IsaMakefile Tue Mar 20 21:37:31 2012 +0100
@@ -108,6 +108,7 @@
Isar/args.ML \
Isar/attrib.ML \
Isar/auto_bind.ML \
+ Isar/bundle.ML \
Isar/calculation.ML \
Isar/class.ML \
Isar/class_declaration.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/bundle.ML Tue Mar 20 21:37:31 2012 +0100
@@ -0,0 +1,115 @@
+(* Title: Pure/Isar/bundle.ML
+ Author: Makarius
+
+Bundled declarations (notes etc.).
+*)
+
+signature BUNDLE =
+sig
+ type bundle = (thm list * Args.src list) list
+ val the_bundle: Proof.context -> string -> bundle
+ val check: Proof.context -> xstring * Position.T -> string
+ val bundle: binding * (thm list * Args.src list) list ->
+ (binding * typ option * mixfix) list -> local_theory -> local_theory
+ val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
+ (binding * string option * mixfix) list -> local_theory -> local_theory
+ val include_: string -> Proof.state -> Proof.state
+ val include_cmd: xstring * Position.T -> Proof.state -> Proof.state
+ val including: string -> Proof.state -> Proof.state
+ val including_cmd: xstring * Position.T -> Proof.state -> Proof.state
+ val print_bundles: Proof.context -> unit
+end;
+
+structure Bundle: BUNDLE =
+struct
+
+(* maintain bundles *)
+
+type bundle = (thm list * Args.src list) list;
+
+fun transform_bundle phi : bundle -> bundle =
+ map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts));
+
+structure Data = Generic_Data
+(
+ type T = bundle Name_Space.table;
+ val empty : T = Name_Space.empty_table "bundle";
+ val extend = I;
+ val merge = Name_Space.merge_tables;
+);
+
+val get_bundles = Data.get o Context.Proof;
+
+fun the_bundle ctxt name =
+ (case Symtab.lookup (#2 (get_bundles ctxt)) name of
+ SOME bundle => bundle
+ | NONE => error ("Unknown bundle " ^ quote name));
+
+fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
+
+
+(* define bundle *)
+
+local
+
+fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy =
+ let
+ val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
+ val bundle0 = raw_bundle
+ |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
+ val bundle =
+ Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
+ |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
+ in
+ lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => fn context =>
+ context |> Data.map
+ (#2 o Name_Space.define context true
+ (Morphism.binding phi binding, transform_bundle phi bundle)))
+ end;
+
+in
+
+val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
+val bundle_cmd =
+ gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of)
+ Proof_Context.read_vars;
+
+end;
+
+
+(* include bundle *)
+
+fun gen_include prep raw_name =
+ Proof.map_context (fn ctxt =>
+ let
+ val bundle = the_bundle ctxt (prep ctxt raw_name);
+ val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
+ val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
+ in #2 (Proof_Context.note_thmss "" [note] ctxt) end);
+
+fun include_ name = Proof.assert_forward #> gen_include (K I) name #> Proof.put_facts NONE;
+fun include_cmd name = Proof.assert_forward #> gen_include check name #> Proof.put_facts NONE;
+fun including name = Proof.assert_backward #> gen_include (K I) name;
+fun including_cmd name = Proof.assert_backward #> gen_include check name;
+
+
+(* print_bundles *)
+
+fun print_bundles ctxt =
+ let
+ val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
+
+ fun prt_fact (ths, []) = map prt_thm ths
+ | prt_fact (ths, atts) = Pretty.enclose "(" ")"
+ (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
+
+ fun prt_bundle (name, bundle) =
+ Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name ::
+ Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
+ in
+ map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt))
+ end |> Pretty.chunks |> Pretty.writeln;
+
+end;
+
--- a/src/Pure/Isar/isar_syn.ML Tue Mar 20 18:42:45 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Mar 20 21:37:31 2012 +0100
@@ -414,6 +414,29 @@
Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
+(* bundled declarations *)
+
+val _ =
+ Outer_Syntax.local_theory ("bundle", Keyword.thy_decl) "define bundle of declarations"
+ ((Parse.binding --| Parse.$$$ "=") -- Parse_Spec.xthms1 -- Parse.for_fixes
+ >> (uncurry Bundle.bundle_cmd));
+
+val _ =
+ Outer_Syntax.command ("include", Keyword.prf_decl)
+ "include declarations from bundle in proof body"
+ (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
+
+val _ =
+ Outer_Syntax.command ("including", Keyword.prf_decl)
+ "include declarations from bundle in goal refinement"
+ (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.including_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)));
+
+
(* locales *)
val locale_val =
--- a/src/Pure/PIDE/document.ML Tue Mar 20 18:42:45 2012 +0100
+++ b/src/Pure/PIDE/document.ML Tue Mar 20 21:37:31 2012 +0100
@@ -445,7 +445,11 @@
fun init_theory deps node =
let
(* FIXME provide files via Scala layer, not master_dir *)
- val (master_dir, header) = Exn.release (get_header node);
+ val (dir, header) = Exn.release (get_header node);
+ val master_dir =
+ (case Url.explode dir of
+ Url.File path => path
+ | _ => Path.current);
val parents =
#imports header |> map (fn import =>
(case Thy_Info.lookup_theory import of (* FIXME more robust!? *)
@@ -453,7 +457,7 @@
| NONE =>
get_theory (Position.file_only import)
(snd (Future.join (the (AList.lookup (op =) deps import))))));
- in Thy_Load.begin_theory (Path.explode master_dir) header parents end;
+ in Thy_Load.begin_theory master_dir header parents end;
in
--- a/src/Pure/ROOT.ML Tue Mar 20 18:42:45 2012 +0100
+++ b/src/Pure/ROOT.ML Tue Mar 20 21:37:31 2012 +0100
@@ -224,6 +224,7 @@
use "Isar/named_target.ML";
use "Isar/expression.ML";
use "Isar/class_declaration.ML";
+use "Isar/bundle.ML";
use "simplifier.ML";
--- a/src/Tools/jEdit/src/document_model.scala Tue Mar 20 18:42:45 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Mar 20 21:37:31 2012 +0100
@@ -42,15 +42,18 @@
case Some(model) =>
model.deactivate()
buffer.unsetProperty(key)
+ buffer.propertiesChanged
}
}
def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
{
- exit(buffer)
+ Swing_Thread.require()
+ apply(buffer).map(_.deactivate)
val model = new Document_Model(session, buffer, name)
buffer.setProperty(key, model)
model.activate()
+ buffer.propertiesChanged
model
}
}
--- a/src/Tools/jEdit/src/plugin.scala Tue Mar 20 18:42:45 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 20 21:37:31 2012 +0100
@@ -185,21 +185,30 @@
if doc_view.isDefined
} yield doc_view.get
+ def exit_model(buffer: Buffer)
+ {
+ swing_buffer_lock(buffer) {
+ jedit_text_areas(buffer).foreach(Document_View.exit)
+ Document_Model.exit(buffer)
+ }
+ }
+
def init_model(buffer: Buffer)
{
swing_buffer_lock(buffer) {
val opt_model =
- document_model(buffer) match {
- case Some(model) => Some(model)
- case None =>
- val name = buffer_name(buffer)
- Thy_Header.thy_name(name) match {
- case Some(theory) =>
- val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
- Some(Document_Model.init(session, buffer, node_name))
- case None => None
+ {
+ val name = buffer_name(buffer)
+ Thy_Header.thy_name(name) match {
+ case Some(theory) =>
+ val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
+ document_model(buffer) match {
+ case Some(model) if model.name == node_name => Some(model)
+ case _ => Some(Document_Model.init(session, buffer, node_name))
}
+ case None => None
}
+ }
if (opt_model.isDefined) {
for (text_area <- jedit_text_areas(buffer)) {
if (document_view(text_area).map(_.model) != opt_model)
@@ -209,14 +218,6 @@
}
}
- def exit_model(buffer: Buffer)
- {
- swing_buffer_lock(buffer) {
- jedit_text_areas(buffer).foreach(Document_View.exit)
- Document_Model.exit(buffer)
- }
- }
-
def init_view(buffer: Buffer, text_area: JEditTextArea)
{
swing_buffer_lock(buffer) {
@@ -419,10 +420,10 @@
Isabelle.start_session()
case msg: BufferUpdate
- if msg.getWhat == BufferUpdate.LOADED =>
+ if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
if (Isabelle.session.is_ready) {
val buffer = msg.getBuffer
- if (buffer != null) Isabelle.init_model(buffer)
+ if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
delay_load(true)
}
--- a/src/Tools/jEdit/src/token_markup.scala Tue Mar 20 18:42:45 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Mar 20 21:37:31 2012 +0100
@@ -239,7 +239,6 @@
{
buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
buffer.setTokenMarker(isabelle_token_marker)
- buffer.propertiesChanged
}
}