--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 10:51:09 2009 +0200
@@ -224,8 +224,8 @@
private def lines_of_command(cmd: Command) =
{
val document = current_document()
- (text_area.getLineOfOffset(to_current(document, cmd.start(document))),
- text_area.getLineOfOffset(to_current(document, cmd.stop(document)) - 1))
+ (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
+ buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
}
@@ -318,10 +318,14 @@
edits = List(Insert(0, buffer.getText(0, buffer.getLength)))
commit
case c: Command =>
+ if(current_document().commands.contains(c))
Swing_Thread.later {
- update_syntax(c)
- invalidate_line(c)
- phase_overview.repaint()
+ // repaint if buffer is active
+ if(text_area.getBuffer == buffer) {
+ update_syntax(c)
+ invalidate_line(c)
+ phase_overview.repaint()
+ }
}
case x => System.err.println("warning: change_receiver ignored " + x)
}