# HG changeset patch
# User immler@in.tum.de
# Date 1227089242 -3600
# Node ID 76435dd5183de8dcaa7c4b022c3ff290934e08df
# Parent  71e86ec7e159c2d671de5c2b9a9d76e9b2b87ac9
pass results to Scroller

diff -r 71e86ec7e159 -r 76435dd5183d src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Nov 18 22:15:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Wed Nov 19 11:07:22 2008 +0100
@@ -6,6 +6,8 @@
 package isabelle.jedit
 
 import isabelle.utils.EventSource
+import isabelle.IsabelleProcess.Result
+import isabelle.YXML.parse_failsafe
 
 import scala.collection.mutable.{ArrayBuffer, HashMap}
 
@@ -32,7 +34,7 @@
 
 object Renderer {
   
-  def render (message: Document): XHTMLPanel = {
+  def render (r: Result): XHTMLPanel = {
     val panel = new XHTMLPanel(new UserAgent())
     val fontResolver =
       panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
@@ -44,7 +46,9 @@
         fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
       panel.relayout()
     })
-    panel.setDocument(message, UserAgent.baseURL)
+    val tree = parse_failsafe(VFS.converter.decode(r.result))
+    val document = XML.document(tree)
+    panel.setDocument(document, UserAgent.baseURL)
     val sa = new SelectionActions
     sa.install(panel)
     panel
@@ -128,7 +132,7 @@
 
 class ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener {
 
-  val buffer:Unrendered[Document] = new MessageBuffer()
+  val buffer:Unrendered[Result] = new MessageBuffer()
   val cache:Rendered[XHTMLPanel] = new PanelCache(buffer)
 
   val subunits = 100
@@ -157,8 +161,8 @@
       }
     })
 
-  def add_message (message: Document) = {
-    buffer.addUnrendered(buffer.size, message)
+  def add_result (result: Result) = {
+    buffer.addUnrendered(buffer.size, result)
     vscroll.setMaximum (Math.max(1, buffer.size * subunits))
     infopanel.setIndicator(true)
     infopanel.setText(buffer.size.toString)
@@ -189,17 +193,17 @@
 
   
   // TODO: register
-  Plugin.plugin.prover.allInfo.add(add_message(_))
+  Plugin.plugin.prover.allInfo.add(add_result(_))
 }
 
 
 
 //containing the unrendered messages
-class MessageBuffer extends HashMap[Int,Document] with Unrendered[Document]{
-  override def addUnrendered (id: Int, m: Document) {
+class MessageBuffer extends HashMap[Int,Result] with Unrendered[Result]{
+  override def addUnrendered (id: Int, m: Result) {
     update(id, m)
   }
-  override def getUnrendered (id: Int): Option[Document] = {
+  override def getUnrendered (id: Int): Option[Result] = {
     if(id < size && id >= 0 && apply(id) != null) Some (apply(id))
     else None
   }
@@ -207,7 +211,7 @@
 }
 
 //containing the rendered messages
-class PanelCache (buffer: Unrendered[Document]) extends HashMap[Int, XHTMLPanel] with Rendered[XHTMLPanel]{
+class PanelCache (buffer: Unrendered[Result]) extends HashMap[Int, XHTMLPanel] with Rendered[XHTMLPanel]{
   override def getRendered (id: Int): Option[XHTMLPanel] = {
     //get message from buffer and render it if necessary
     if(!isDefinedAt(id)){
diff -r 71e86ec7e159 -r 76435dd5183d src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Nov 18 22:15:06 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Nov 19 11:07:22 2008 +0100
@@ -30,7 +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]
+  val allInfo = new EventSource[Result]
   var document = null : Document
   
   var workerThread = new Thread("isabelle.Prover: worker") {
@@ -83,7 +83,7 @@
   def handleResult(st : Command, r : Result, tree : XML.Tree) {
     def fireChange() = 
       inUIThread(() => commandInfo.fire(new CommandChangeInfo(st)))
-    allInfo.fire(st.document)
+    allInfo.fire(r)
     
     r.kind match {
       case IsabelleProcess.Kind.ERROR =>