# HG changeset patch
# User wenzelm
# Date 1260906299 -3600
# Node ID 30528e68f774c1b65a066bbc333fb9cf71b3d6bc
# Parent  3779c54a2d213739c14a8a4ef3b120122168b83e
some explicit Swing_Thread guards;

diff -r 3779c54a2d21 -r 30528e68f774 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Dec 15 20:20:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Dec 15 20:44:59 2009 +0100
@@ -26,6 +26,7 @@
 
   def init(session: Session, buffer: Buffer): Document_Model =
   {
+    Swing_Thread.assert()
     val model = new Document_Model(session, buffer)
     buffer.setProperty(key, model)
     model.activate()
@@ -34,6 +35,7 @@
 
   def apply(buffer: Buffer): Option[Document_Model] =
   {
+    Swing_Thread.assert()
     buffer.getProperty(key) match {
       case model: Document_Model => Some(model)
       case _ => None
@@ -42,6 +44,7 @@
 
   def exit(buffer: Buffer)
   {
+    Swing_Thread.assert()
     apply(buffer) match {
       case None => error("No document model for buffer: " + buffer)
       case Some(model) =>
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) =>
diff -r 3779c54a2d21 -r 30528e68f774 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 15 20:20:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 15 20:44:59 2009 +0100
@@ -36,11 +36,12 @@
 
     stopped = false
 
+    // FIXME lock buffer !??
     val data = new SideKickParsedData(buffer.getName)
     val root = data.root
     data.getAsset(root).setEnd(buffer.getLength)
 
-    Document_Model(buffer) match {
+    Swing_Thread.now { Document_Model(buffer) } match {
       case Some(model) =>
         val document = model.current_document()
         for (command <- document.commands if !stopped) {
diff -r 3779c54a2d21 -r 30528e68f774 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Dec 15 20:20:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Dec 15 20:44:59 2009 +0100
@@ -42,7 +42,7 @@
     loop {
       react {
         case cmd: Command =>
-          Document_Model(view.getBuffer) match {
+          Swing_Thread.now { Document_Model(view.getBuffer) } match {
             case None =>
             case Some(model) =>
               val body =