equal
deleted
inserted
replaced
179 def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area) |
179 def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area) |
180 |
180 |
181 def document_views(buffer: Buffer): List[Document_View] = |
181 def document_views(buffer: Buffer): List[Document_View] = |
182 for { |
182 for { |
183 text_area <- jedit_text_areas(buffer).toList |
183 text_area <- jedit_text_areas(buffer).toList |
184 val doc_view = document_view(text_area) |
184 doc_view = document_view(text_area) |
185 if doc_view.isDefined |
185 if doc_view.isDefined |
186 } yield doc_view.get |
186 } yield doc_view.get |
187 |
187 |
188 def init_model(buffer: Buffer) |
188 def init_model(buffer: Buffer) |
189 { |
189 { |