plain results, no markup here;
authorwenzelm
Fri, 04 Dec 2009 23:07:40 +0100
changeset 34746 94ef0ff39c21
parent 34745 83b553bd3fa3
child 34747 b316d05a66a4
plain results, no markup here;
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)(_ + _)