# HG changeset patch
# User wenzelm
# Date 1246389770 -7200
# Node ID 4b797391859a5e8f31df21b75b02c08d409308f9
# Parent  42ab7ad9b07eda209a0dc71a0d28c0757187c21e
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;

diff -r 42ab7ad9b07e -r 4b797391859a src/Tools/jEdit/src/jedit/OptionPane.scala
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Sat Jun 27 00:19:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Tue Jun 30 21:22:50 2009 +0200
@@ -41,7 +41,7 @@
     if (Isabelle.Int_Property("font-size") != size)
     {
       Isabelle.Int_Property("font-size") = size
-      Swing.later { Isabelle.plugin.set_font(size) }
+      Swing_Thread.later { Isabelle.plugin.set_font(size) }
     }
   }
 }
diff -r 42ab7ad9b07e -r 4b797391859a src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat Jun 27 00:19:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jun 30 21:22:50 2009 +0200
@@ -101,7 +101,7 @@
     loop {
       react {
         case _ => {       // FIXME potentially blocking within loop/react!?!?!?!
-          Swing.now {
+          Swing_Thread.now {
             repaint_delay.delay_or_ignore()
             phase_overview.repaint_delay.delay_or_ignore()
           }
diff -r 42ab7ad9b07e -r 4b797391859a src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sat Jun 27 00:19:11 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 30 21:22:50 2009 +0200
@@ -138,7 +138,7 @@
                   case XML.Elem(Markup.READY, _, _)
                   if !initialized =>
                     initialized = true
-                    Swing.now { this ! ProverEvents.Activate }
+                    Swing_Thread.now { this ! ProverEvents.Activate }
 
                   // document edits
                   case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
@@ -262,20 +262,20 @@
     process.begin_document(document_id0, path)
   }
 
-  private def edit_document(old_id: String, document_id: String, changes: StructureChange) = Swing.now
-  {
-    val removes =
-      for (cmd <- changes.removed_commands) yield {
-        commands -= cmd.id
-        if (cmd.state_id != null) states -= cmd.state_id
-        changes.before_change.map(_.id).getOrElse(document_id0) -> None
-      }
-    val inserts =
-      for (cmd <- changes.added_commands) yield {
-        commands += (cmd.id -> cmd)
-        process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
-        (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id)
-      }
-    process.edit_document(old_id, document_id, removes.reverse ++ inserts)
-  }
+  private def edit_document(old_id: String, document_id: String, changes: StructureChange) =
+    Swing_Thread.now {
+      val removes =
+        for (cmd <- changes.removed_commands) yield {
+          commands -= cmd.id
+          if (cmd.state_id != null) states -= cmd.state_id
+          changes.before_change.map(_.id).getOrElse(document_id0) -> None
+        }
+      val inserts =
+        for (cmd <- changes.added_commands) yield {
+          commands += (cmd.id -> cmd)
+          process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
+          (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id)
+        }
+      process.edit_document(old_id, document_id, removes.reverse ++ inserts)
+    }
 }