diff -r 3779c54a2d21 -r 30528e68f774 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Dec 15 20:20:07 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Dec 15 20:44:59 2009 +0100 @@ -40,6 +40,7 @@ def init(model: Document_Model, text_area: TextArea): Document_View = { + Swing_Thread.assert() val doc_view = new Document_View(model, text_area) text_area.putClientProperty(key, doc_view) doc_view.activate() @@ -48,6 +49,7 @@ def apply(text_area: TextArea): Option[Document_View] = { + Swing_Thread.assert() text_area.getClientProperty(key) match { case doc_view: Document_View => Some(doc_view) case _ => None @@ -56,6 +58,7 @@ def exit(text_area: TextArea) { + Swing_Thread.assert() apply(text_area) match { case None => error("No document view for text area: " + text_area) case Some(doc_view) =>