# HG changeset patch # User immler@in.tum.de # Date 1227019261 -3600 # Node ID e0679b361a0e60ddbc9e302ee16a275a515f3090 # Parent b58404f41b686fb9359b775d70eb383c05f27f94 register to buffer all messages diff -r b58404f41b68 -r e0679b361a0e src/Tools/jEdit/src/jedit/ScrollerDockable.scala --- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Tue Nov 18 15:01:00 2008 +0100 +++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Tue Nov 18 15:41:01 2008 +0100 @@ -5,6 +5,8 @@ package isabelle.jedit +import isabelle.utils.EventSource + import scala.collection.mutable.{ArrayBuffer, HashMap} import java.awt.{ BorderLayout, Adjustable } @@ -96,8 +98,10 @@ var y:Int = getHeight + pixeloffset while (y >= 0 && n >= 0){ val panel = place_message (n, y) - panel.setBorder(javax.swing.border.LineBorder.createBlackLineBorder) - y = y - panel.getHeight + if(panel != null) { + panel.setBorder(javax.swing.border.LineBorder.createBlackLineBorder) + y = y - panel.getHeight + } n = n - 1 } } @@ -181,21 +185,8 @@ } - // TODO: register somewhere - // here only 'emulation of message stream' - Plugin.plugin.stateUpdate.add(state => { - var i = 0 - if(state != null) new Thread{ - override def run() { - while (i < 10000) { - add_message(state.document) - i += 1 - /*try {Thread.sleep(3)} - catch{case _ =>}*/ - } - } - }.start - }) + // TODO: register + Plugin.plugin.prover.allInfo.add(add_message(_)) } diff -r b58404f41b68 -r e0679b361a0e src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Tue Nov 18 15:01:00 2008 +0100 +++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Nov 18 15:41:01 2008 +0100 @@ -30,6 +30,7 @@ val activated = new EventSource[Unit] val commandInfo = new EventSource[CommandChangeInfo] val outputInfo = new EventSource[String] + val allInfo = new EventSource[org.w3c.dom.Document] var document = null : Document var workerThread = new Thread("isabelle.Prover: worker") { @@ -82,6 +83,7 @@ def handleResult(st : Command, r : Result, tree : XML.Tree) { def fireChange() = inUIThread(() => commandInfo.fire(new CommandChangeInfo(st))) + allInfo.fire(st.document) r.kind match { case IsabelleProcess.Kind.ERROR => @@ -97,7 +99,7 @@ case IsabelleProcess.Kind.PRIORITY => st.addResult(tree) fireChange() - + case IsabelleProcess.Kind.WARNING => st.addResult(tree) fireChange()