# HG changeset patch
# User wenzelm
# Date 1529576537 -7200
# Node ID 1be1b7620a42fe81187748b28da7e81487dd3cb8
# Parent  b6e48841d0a5cb75a48896b33cdb4a92fea9de33
tuned signature -- facilitate testing;

diff -r b6e48841d0a5 -r 1be1b7620a42 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Jun 21 00:01:21 2018 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jun 21 12:22:17 2018 +0200
@@ -36,6 +36,13 @@
         if model.isInstanceOf[File_Model]
       } yield (node_name, model.asInstanceOf[File_Model])
 
+    def document_blobs: Document.Blobs =
+      Document.Blobs(
+        (for {
+          (node_name, model) <- models.iterator
+          blob <- model.get_blob
+        } yield (node_name -> blob)).toMap)
+
     def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
       : (Buffer_Model, State) =
     {
@@ -77,6 +84,8 @@
   def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
+  def document_blobs(): Document.Blobs = state.value.document_blobs
+
 
   /* bibtex */
 
@@ -218,12 +227,7 @@
 
     state.change_result(st =>
       {
-        val doc_blobs =
-          Document.Blobs(
-            (for {
-              (node_name, model) <- st.models.iterator
-              blob <- model.get_blob
-            } yield (node_name -> blob)).toMap)
+        val doc_blobs = st.document_blobs
 
         val buffer_edits =
           (for {