fixed some issues with multiple active buffers
authorimmler@in.tum.de
Thu, 27 Aug 2009 10:51:09 +0200
changeset 34681 74cc10b5ba51
parent 34680 1f1f6c95de64
child 34682 bcae80cc4170
fixed some issues with multiple active buffers
src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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)
       }