src/Tools/jEdit/src/plugin.scala
changeset 44379 1079ab6b342b
parent 44238 36120feb70ed
child 44434 3b9b684bfa6f
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 14:15:52 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 16:12:23 2011 +0200
     1.3 @@ -199,6 +199,13 @@
     1.4    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
     1.5    def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
     1.6  
     1.7 +  def document_views(buffer: Buffer): List[Document_View] =
     1.8 +    for {
     1.9 +      text_area <- jedit_text_areas(buffer).toList
    1.10 +      val doc_view = document_view(text_area)
    1.11 +      if doc_view.isDefined
    1.12 +    } yield doc_view.get
    1.13 +
    1.14    def init_model(buffer: Buffer)
    1.15    {
    1.16      swing_buffer_lock(buffer) {