# HG changeset patch
# User wenzelm
# Date 1484216440 -3600
# Node ID e89f5ef32aa213942eac6d05a53833487554320b
# Parent  c3b42ac0cf813215f193245c500cc30837320b9a
tuned signature;

diff -r c3b42ac0cf81 -r e89f5ef32aa2 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Jan 12 11:17:05 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jan 12 11:20:40 2017 +0100
@@ -409,12 +409,18 @@
   def node_required: Boolean = _node_required
   def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
 
+  def document_view_iterator: Iterator[Document_View] =
+    for {
+      text_area <- JEdit_Lib.jedit_text_areas(buffer)
+      doc_view <- Document_View.get(text_area)
+    } yield doc_view
+
   override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
   {
     GUI_Thread.require {}
 
     (for {
-      doc_view <- PIDE.document_views(buffer).iterator
+      doc_view <- document_view_iterator
       range <- doc_view.perspective(snapshot).ranges.iterator
     } yield range).toList
   }
@@ -503,7 +509,7 @@
       reset_blob()
       reset_bibtex_entries()
 
-      for (doc_view <- PIDE.document_views(buffer))
+      for (doc_view <- document_view_iterator)
         doc_view.rich_text_area.active_reset()
 
       pending ++= edits
diff -r c3b42ac0cf81 -r e89f5ef32aa2 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Jan 12 11:17:05 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jan 12 11:20:40 2017 +0100
@@ -68,12 +68,6 @@
 
   /* document model and view */
 
-  def document_views(buffer: Buffer): List[Document_View] =
-    for {
-      text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
-      doc_view <- Document_View.get(text_area)
-    } yield doc_view
-
   def exit_models(buffers: List[Buffer])
   {
     GUI_Thread.now {