# HG changeset patch # User wenzelm # Date 1332275851 -3600 # Node ID 8e1b14bf01905646f20c8dd47a677b33d2a4c3e9 # Parent 6f8dfe6c1aea4987c1f346ae6de6ba7108d6d848# Parent 34761733526c42c7b26ed1b11ebc06a9cca4f91f merged diff -r 6f8dfe6c1aea -r 8e1b14bf0190 etc/isar-keywords-ZF.el --- 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" diff -r 6f8dfe6c1aea -r 8e1b14bf0190 etc/isar-keywords.el --- 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" diff -r 6f8dfe6c1aea -r 8e1b14bf0190 src/Pure/IsaMakefile --- 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 \ diff -r 6f8dfe6c1aea -r 8e1b14bf0190 src/Pure/Isar/bundle.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; + diff -r 6f8dfe6c1aea -r 8e1b14bf0190 src/Pure/Isar/isar_syn.ML --- 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 = diff -r 6f8dfe6c1aea -r 8e1b14bf0190 src/Pure/PIDE/document.ML --- 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 diff -r 6f8dfe6c1aea -r 8e1b14bf0190 src/Pure/ROOT.ML --- 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"; diff -r 6f8dfe6c1aea -r 8e1b14bf0190 src/Tools/jEdit/src/document_model.scala --- 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 } } diff -r 6f8dfe6c1aea -r 8e1b14bf0190 src/Tools/jEdit/src/plugin.scala --- 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) } diff -r 6f8dfe6c1aea -r 8e1b14bf0190 src/Tools/jEdit/src/token_markup.scala --- 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 } }