--- 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))