src/Tools/jEdit/src/plugin.scala
changeset 47868 395b7277ed76
parent 47800 1752164d916b
child 47929 34761733526c
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 17 17:36:10 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 17 17:44:29 2012 +0100
     1.3 @@ -181,7 +181,7 @@
     1.4    def document_views(buffer: Buffer): List[Document_View] =
     1.5      for {
     1.6        text_area <- jedit_text_areas(buffer).toList
     1.7 -      val doc_view = document_view(text_area)
     1.8 +      doc_view = document_view(text_area)
     1.9        if doc_view.isDefined
    1.10      } yield doc_view.get
    1.11