# HG changeset patch
# User wenzelm
# Date 1230465567 -3600
# Node ID a245f6cc3105208899ff1484a8954681f49c55c7
# Parent  f2e13329cc49bc79ebdc598ecfc5cb55b94b2fb9
replaced inUIThread by scala-style swing/swing_async combinators;

diff -r f2e13329cc49 -r a245f6cc3105 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sat Dec 27 15:20:46 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Dec 28 12:59:27 2008 +0100
@@ -39,8 +39,16 @@
   val allInfo = new EventSource[Result]
   var document = null : Document
 
+
+  def swing(body: => Unit) =
+    SwingUtilities.invokeAndWait(new Runnable { def run = body })
+
+  def swing_async(body: => Unit) =
+    SwingUtilities.invokeLater(new Runnable { def run = body })
+
+
   def fireChange(c : Command) =
-    inUIThread(() => commandInfo.fire(new CommandChangeInfo(c)))
+    swing { commandInfo.fire(new CommandChangeInfo(c)) }
 
   var workerThread = new Thread("isabelle.Prover: worker") {
     override def run() : Unit = {
@@ -54,15 +62,15 @@
           return
         else if (r.kind == IsabelleProcess.Kind.STDOUT 
                  || r.kind == IsabelleProcess.Kind.STDIN)
-          inUIThread(() => outputInfo.fire(r.result))
+          swing { outputInfo.fire(r.result) }
         else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
           initialized = true
-          inUIThread(() => 
+          swing {
             if (document != null) {
               document.activate()
               activated.fire(())
             }
-          )
+          }
         }
         else {
           val tree = parse_failsafe(isabelle_symbols.decode(r.result))
@@ -161,12 +169,6 @@
     process.kill
   }
   
-  private def inUIThread(runnable : () => Unit) {
-    SwingUtilities invokeAndWait new Runnable() {
-      override def run() { runnable () }
-    }
-  }
-  
   def setDocument(text : Text, path : String) {
     this.document = new Document(text, this)
     process.ML("ThyLoad.add_path " + encode_string(path))