eliminated Command.Status.REMOVE/REMOVED;
authorwenzelm
Tue, 27 Jan 2009 22:14:40 +0100
changeset 34507 018bad916757
parent 34506 bc22e49358f8
child 34508 422a43b76f77
eliminated Command.Status.REMOVE/REMOVED;
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)