src/Tools/jEdit/src/document_view.scala
changeset 43397 dba359c0ae3b
parent 43393 f4141da52e92
child 43404 c8369f3d88a1
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 15:42:54 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 16:22:58 2011 +0200
     1.3 @@ -31,15 +31,6 @@
     1.4  
     1.5    private val key = new Object
     1.6  
     1.7 -  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
     1.8 -  {
     1.9 -    Swing_Thread.require()
    1.10 -    val doc_view = new Document_View(model, text_area)
    1.11 -    text_area.putClientProperty(key, doc_view)
    1.12 -    doc_view.activate()
    1.13 -    doc_view
    1.14 -  }
    1.15 -
    1.16    def apply(text_area: JEditTextArea): Option[Document_View] =
    1.17    {
    1.18      Swing_Thread.require()
    1.19 @@ -59,6 +50,15 @@
    1.20          text_area.putClientProperty(key, null)
    1.21      }
    1.22    }
    1.23 +
    1.24 +  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
    1.25 +  {
    1.26 +    exit(text_area)
    1.27 +    val doc_view = new Document_View(model, text_area)
    1.28 +    text_area.putClientProperty(key, doc_view)
    1.29 +    doc_view.activate()
    1.30 +    doc_view
    1.31 +  }
    1.32  }
    1.33  
    1.34