# 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
   }
 }