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