# HG changeset patch
# User wenzelm
# Date 1384956025 -3600
# Node ID 2ea4d717d15214d5e7b0cb2e1d736ff5c7879ff7
# Parent  842adea880a40ec9faebe1289e3e4cce509dab8e
tuned;

diff -r 842adea880a4 -r 2ea4d717d152 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Nov 20 12:24:54 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Nov 20 15:00:25 2013 +0100
@@ -73,9 +73,8 @@
   def document_views(buffer: Buffer): List[Document_View] =
     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
-      doc_view = document_view(text_area)
-      if doc_view.isDefined
-    } yield doc_view.get
+      doc_view <- document_view(text_area)
+    } yield doc_view
 
   def document_models(): List[Document_Model] =
     for {