# HG changeset patch
# User wenzelm
# Date 1233090880 -3600
# Node ID 018bad916757efa104ee0fc313d7042acdb6b5c6
# Parent  bc22e49358f8411db158a5c87ab9c05f830b08cc
eliminated Command.Status.REMOVE/REMOVED;

diff -r bc22e49358f8 -r 018bad916757 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jan 27 22:13:56 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jan 27 22:14:40 2009 +0100
@@ -148,8 +148,7 @@
 
   def repaint(cmd: Command) =
   {
-    val status = cmd.status
-    if (text_area != null && status != Command.Status.REMOVE && status != Command.Status.REMOVED) {
+    if (text_area != null) {
       val start = text_area.getLineOfOffset(to_current(cmd.start))
       val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
       text_area.invalidateLineRange(start, stop)