# HG changeset patch
# User immler@in.tum.de
# Date 1237549617 -3600
# Node ID e3ca0658fb6a21cf49724c9632ceb4ed413e8bfc
# Parent  50ae42f01d451f5be9fa5b2c8c96cb552a3161ca
changes of text with unique id

diff -r 50ae42f01d45 -r e3ca0658fb6a src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Fri Mar 20 11:57:21 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Fri Mar 20 12:46:57 2009 +0100
@@ -76,7 +76,9 @@
     val context = new IndexLineContext(line, previous)
     val start = buffer.getLineStartOffset(line)
     val stop = start + line_segment.count
-    
+
+    val (current_document, current_version) = synchronized (prover.document, prover.document_id)
+   
     def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
     def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
 
diff -r 50ae42f01d45 -r e3ca0658fb6a src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri Mar 20 11:57:21 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri Mar 20 12:46:57 2009 +0100
@@ -42,6 +42,9 @@
 class TheoryView (text_area: JEditTextArea, document_actor: Actor)
     extends TextAreaExtension with BufferListener {
 
+  private var id_count = 0;
+  private def id(): Int = synchronized {id_count += 1; id_count}
+  
   private val buffer = text_area.getBuffer
   private val prover = Isabelle.prover_setup(buffer).get.prover
   buffer.addBufferListener(this)
@@ -89,7 +92,7 @@
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
     buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
     update_styles
-    document_actor ! new Text.Change(0,buffer.getText(0, buffer.getLength),0)
+    document_actor ! new Text.Change(id(), 0,buffer.getText(0, buffer.getLength),0)
   }
 
   def deactivate() = {
@@ -107,8 +110,10 @@
     scala.actors.Actor.loop {
       scala.actors.Actor.react {
         case _ => {
+          Swing.now {
             repaint_delay.delay_or_ignore()
             phase_overview.repaint_delay.delay_or_ignore()
+          }
         }
       }
     }
@@ -225,12 +230,12 @@
   {
     val text = buffer.getText(offset, length)
     if (col == null)
-      col = new Text.Change(offset, text, 0)
+      col = new Text.Change(id(), offset, text, 0)
     else if (col.start <= offset && offset <= col.start + col.added.length)
-      col = new Text.Change(col.start, col.added + text, col.removed)
+      col = new Text.Change(col.id, col.start, col.added + text, col.removed)
     else {
       commit
-      col = new Text.Change(offset, text, 0)
+      col = new Text.Change(id(), offset, text, 0)
     }
     delay_commit
   }
@@ -239,10 +244,10 @@
     start_line: Int, start: Int, num_lines: Int, removed: Int) =
   {
     if (col == null)
-      col = new Text.Change(start, "", removed)
+      col = new Text.Change(id(), start, "", removed)
     else if (col.start > start + removed || start > col.start + col.added.length) {
       commit
-      col = new Text.Change(start, "", removed)
+      col = new Text.Change(id(), start, "", removed)
     }
     else {
 /*      val offset = start - col.start
@@ -254,7 +259,7 @@
           (diff - (offset min 0), offset min 0)
       col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
       commit
-      col = new Text.Change(start, "", removed)
+      col = new Text.Change(id(), start, "", removed)
     }
     delay_commit
   }
diff -r 50ae42f01d45 -r e3ca0658fb6a src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Fri Mar 20 11:57:21 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Fri Mar 20 12:46:57 2009 +0100
@@ -50,7 +50,7 @@
 
   def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword)
   def activate: (ProofDocument, StructureChange) = {
-    val (doc, change) = text_changed(new Text.Change(0, content, content.length))
+    val (doc, change) = text_changed(new Text.Change(0, 0, content, content.length))
     return (doc.mark_active, change)
   }
   def set_command_keyword(f: String => Boolean): ProofDocument =
diff -r 50ae42f01d45 -r e3ca0658fb6a src/Tools/jEdit/src/proofdocument/Text.scala
--- a/src/Tools/jEdit/src/proofdocument/Text.scala	Fri Mar 20 11:57:21 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala	Fri Mar 20 12:46:57 2009 +0100
@@ -1,5 +1,5 @@
 /*
- * Text as event source
+ * Changes in text as event
  *
  * @author Johannes Hölzl, TU Munich
  */
@@ -8,7 +8,7 @@
 
 
 object Text {
-  case class Change(start: Int, val added: String, val removed: Int) {
+  case class Change(id: Int, start: Int, val added: String, val removed: Int) {
     override def toString = "start: " + start + " added: " + added + " removed: " + removed
   }
 }
\ No newline at end of file