# HG changeset patch
# User immler@in.tum.de
# Date 1243434195 -7200
# Node ID aef72e071725505c15b2ac08bbb82967a82adaa7
# Parent  b86c54be2fe0bde572955f1ad8a212f55923533c
fixed delete markup

diff -r b86c54be2fe0 -r aef72e071725 src/Tools/jEdit/src/prover/Command.scala
--- 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
   }
diff -r b86c54be2fe0 -r aef72e071725 src/Tools/jEdit/src/prover/MarkupNode.scala
--- 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}