# HG changeset patch
# User wenzelm
# Date 1259943256 -3600
# Node ID 30fba76e6cc22bc34c2a77d11ba2028fa8615a57
# Parent  eb49306946f4e42eebd9f0f0d709ae584d80ead4
results: XML.Tree;

diff -r eb49306946f4 -r 30fba76e6cc2 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Sat Nov 14 16:53:49 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri Dec 04 17:14:16 2009 +0100
@@ -97,7 +97,7 @@
     doc.states.getOrElse(this, empty_cmd_state)
 
   def status(doc: ProofDocument) = cmd_state(doc).state.status
-  def result_document(doc: ProofDocument) = cmd_state(doc).result_document
+  def results(doc: ProofDocument) = cmd_state(doc).results
   def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
   def highlight(doc: ProofDocument) = cmd_state(doc).highlight
   def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
@@ -109,13 +109,12 @@
 {
   protected override var _state = new State(command)
 
-  def result_document: org.w3c.dom.Document =
-    XML.document(
-      command.state.results ::: state.results match {
-        case Nil => XML.Elem("message", Nil, Nil)
-        case List(elem) => elem
-        case elems => XML.Elem("messages", Nil, elems)
-      }, "style")
+  def results: XML.Tree =
+    (command.state.results ::: state.results) match {
+      case Nil => XML.Elem("message", Nil, Nil)
+      case List(elem) => elem
+      case elems => XML.Elem("messages", Nil, elems)
+    }
 
   def markup_root: Markup_Text =
     (command.state.markup_root /: state.markup_root.markup)(_ + _)