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