src/Tools/jEdit/src/prover/Prover.scala

   val commandInfo = new EventSource[CommandChangeInfo]
   val outputInfo = new EventSource[String]
   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 = {
       while (true) {
         val r = process.get_result

         
         if (r.kind == IsabelleProcess.Kind.EXIT)
           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))
           if (st == null || (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE))
           tree match {

 
   def stop() {
     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))
 
     document.structuralChanges.add(changes => {