src/Tools/jEdit/src/plugin.scala
changeset 46997 395b7277ed76
parent 46918 1752164d916b
child 47058 34761733526c
--- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 17 17:36:10 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 17 17:44:29 2012 +0100
@@ -181,7 +181,7 @@
   def document_views(buffer: Buffer): List[Document_View] =
     for {
       text_area <- jedit_text_areas(buffer).toList
-      val doc_view = document_view(text_area)
+      doc_view = document_view(text_area)
       if doc_view.isDefined
     } yield doc_view.get