src/Tools/jEdit/src/plugin.scala
changeset 44379 1079ab6b342b
parent 44238 36120feb70ed
child 44434 3b9b684bfa6f
--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 14:15:52 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 16:12:23 2011 +0200
@@ -199,6 +199,13 @@
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
 
+  def document_views(buffer: Buffer): List[Document_View] =
+    for {
+      text_area <- jedit_text_areas(buffer).toList
+      val doc_view = document_view(text_area)
+      if doc_view.isDefined
+    } yield doc_view.get
+
   def init_model(buffer: Buffer)
   {
     swing_buffer_lock(buffer) {