fixed delete markup

--- a/src/Tools/jEdit/src/prover/Command.scala	Wed May 27 15:46:06 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Wed May 27 16:23:15 2009 +0200
@@ -53,10 +53,10 @@
     if (st == Command.Status.UNPROCESSED) {
       state_results.clear
       // delete markup
-      markup_root.filter(_.info match {
+      markup_root = markup_root.filter(_.info match {
           case RootInfo() | OuterInfo(_) => true
           case _ => false
-        })
+        }).head
     }
     _status = st
   }

--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed May 27 15:46:06 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed May 27 16:23:15 2009 +0200
@@ -14,7 +14,7 @@
 import javax.swing.tree._
 
 abstract class MarkupInfo
-case class RootInfo extends MarkupInfo
+case class RootInfo() extends MarkupInfo
 case class OuterInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
 case class HighlightInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
 case class TypeInfo(type_kind: String) extends MarkupInfo {override def toString = type_kind}