# HG changeset patch
# User wenzelm
# Date 1384891145 -3600
# Node ID 761be40990f100b1e7b4509851c56d7e391c84ae
# Parent  744ea0025e11d19ebfa00d41a9b474a43a141bc8
tuned signature;

diff -r 744ea0025e11 -r 761be40990f1 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 20:53:43 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 20:59:05 2013 +0100
@@ -19,21 +19,12 @@
 
   override def session: Session = PIDE.session
 
-  def document_models(): List[Document_Model] =
-    for {
-      buffer <- JEdit_Lib.jedit_buffers().toList
-      model <- PIDE.document_model(buffer)
-    } yield model
-
-  def document_blobs(): Document.Blobs =
-    document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
-
   override def flush()
   {
     Swing_Thread.require()
 
-    val edits = document_models().flatMap(_.flushed_edits())
-    if (!edits.isEmpty) session.update(document_blobs(), edits)
+    val edits = PIDE.document_models().flatMap(_.flushed_edits())
+    if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
   }
 
   private val delay_flush =
diff -r 744ea0025e11 -r 761be40990f1 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Nov 19 20:53:43 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Nov 19 20:59:05 2013 +0100
@@ -77,6 +77,15 @@
       if doc_view.isDefined
     } yield doc_view.get
 
+  def document_models(): List[Document_Model] =
+    for {
+      buffer <- JEdit_Lib.jedit_buffers().toList
+      model <- document_model(buffer)
+    } yield model
+
+  def document_blobs(): Document.Blobs =
+    document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
+
   def exit_models(buffers: List[Buffer])
   {
     Swing_Thread.now {
@@ -113,7 +122,7 @@
             model_edits ::: edits
           }
         }
-      session.update(PIDE.editor.document_blobs(), init_edits)
+      session.update(document_blobs(), init_edits)
     }
   }