# HG changeset patch
# User wenzelm
# Date 1308147778 -7200
# Node ID dba359c0ae3b66e3b18b039a85cf8b4f031291ab
# Parent  548a68eafaea2fb13d28acf487d270b543f240de
more robust init;

diff -r 548a68eafaea -r dba359c0ae3b src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jun 15 15:42:54 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jun 15 16:22:58 2011 +0200
@@ -56,15 +56,6 @@
 
   private val key = "isabelle.document_model"
 
-  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
-  {
-    Swing_Thread.require()
-    val model = new Document_Model(session, buffer, thy_name)
-    buffer.setProperty(key, model)
-    model.activate()
-    model
-  }
-
   def apply(buffer: Buffer): Option[Document_Model] =
   {
     Swing_Thread.require()
@@ -84,6 +75,15 @@
         buffer.unsetProperty(key)
     }
   }
+
+  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
+  {
+    exit(buffer)
+    val model = new Document_Model(session, buffer, thy_name)
+    buffer.setProperty(key, model)
+    model.activate()
+    model
+  }
 }
 
 
diff -r 548a68eafaea -r dba359c0ae3b src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 15:42:54 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 16:22:58 2011 +0200
@@ -31,15 +31,6 @@
 
   private val key = new Object
 
-  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
-  {
-    Swing_Thread.require()
-    val doc_view = new Document_View(model, text_area)
-    text_area.putClientProperty(key, doc_view)
-    doc_view.activate()
-    doc_view
-  }
-
   def apply(text_area: JEditTextArea): Option[Document_View] =
   {
     Swing_Thread.require()
@@ -59,6 +50,15 @@
         text_area.putClientProperty(key, null)
     }
   }
+
+  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
+  {
+    exit(text_area)
+    val doc_view = new Document_View(model, text_area)
+    text_area.putClientProperty(key, doc_view)
+    doc_view.activate()
+    doc_view
+  }
 }