--- 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)(_ + _)