# HG changeset patch
# User wenzelm
# Date 1259964460 -3600
# Node ID 94ef0ff39c211cde63d30b9d3cc3f932e4d91001
# Parent  83b553bd3fa30edd478467b21ecfbec01ce876fe
plain results, no markup here;

diff -r 83b553bd3fa3 -r 94ef0ff39c21 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Fri Dec 04 17:14:44 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri Dec 04 23:07:40 2009 +0100
@@ -109,12 +109,8 @@
 {
   protected override var _state = new State(command)
 
-  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 results: List[XML.Tree] =
+    command.state.results ::: state.results
 
   def markup_root: Markup_Text =
     (command.state.markup_root /: state.markup_root.markup)(_ + _)