# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID 74cc10b5ba5133e7f983c1ba8d6e3bbd4141ed9e
# Parent  1f1f6c95de643817f7de8e17013611d4a6436b7a
fixed some issues with multiple active buffers

diff -r 1f1f6c95de64 -r 74cc10b5ba51 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)
       }