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