--- 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(_)
--- 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
}
--- 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 =
--- 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