1.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Jun 15 15:42:54 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jun 15 16:22:58 2011 +0200
     1.3 @@ -56,15 +56,6 @@
     1.4  
     1.5    private val key = "isabelle.document_model"
     1.6  
     1.7 -  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
     1.8 -  {
     1.9 -    Swing_Thread.require()
    1.10 -    val model = new Document_Model(session, buffer, thy_name)
    1.11 -    buffer.setProperty(key, model)
    1.12 -    model.activate()
    1.13 -    model
    1.14 -  }
    1.15 -
    1.16    def apply(buffer: Buffer): Option[Document_Model] =
    1.17    {
    1.18      Swing_Thread.require()
    1.19 @@ -84,6 +75,15 @@
    1.20          buffer.unsetProperty(key)
    1.21      }
    1.22    }
    1.23 +
    1.24 +  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
    1.25 +  {
    1.26 +    exit(buffer)
    1.27 +    val model = new Document_Model(session, buffer, thy_name)
    1.28 +    buffer.setProperty(key, model)
    1.29 +    model.activate()
    1.30 +    model
    1.31 +  }
    1.32  }
    1.33  
    1.34  

     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 15:42:54 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 16:22:58 2011 +0200
     2.3 @@ -31,15 +31,6 @@
     2.4  
     2.5    private val key = new Object
     2.6  
     2.7 -  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
     2.8 -  {
     2.9 -    Swing_Thread.require()
    2.10 -    val doc_view = new Document_View(model, text_area)
    2.11 -    text_area.putClientProperty(key, doc_view)
    2.12 -    doc_view.activate()
    2.13 -    doc_view
    2.14 -  }
    2.15 -
    2.16    def apply(text_area: JEditTextArea): Option[Document_View] =
    2.17    {
    2.18      Swing_Thread.require()
    2.19 @@ -59,6 +50,15 @@
    2.20          text_area.putClientProperty(key, null)
    2.21      }
    2.22    }
    2.23 +
    2.24 +  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
    2.25 +  {
    2.26 +    exit(text_area)
    2.27 +    val doc_view = new Document_View(model, text_area)
    2.28 +    text_area.putClientProperty(key, doc_view)
    2.29 +    doc_view.activate()
    2.30 +    doc_view
    2.31 +  }
    2.32  }
    2.33  
    2.34