# HG changeset patch
# User wenzelm
# Date 1251919314 -7200
# Node ID 3e995f100ad2e62e9cff3b318e893db20b28d516
# Parent  3c0a8bece8b837eab4e824a4f4619d0579cce689
sealed Edit;
Change.edits: plain field, plain list -- no reverse;
TheoryView.edits: ListBuffer -- no reverse;
misc tuning;

diff -r 3c0a8bece8b8 -r 3e995f100ad2 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Sep 01 21:05:57 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Sep 02 21:21:54 2009 +0200
@@ -10,6 +10,7 @@
 
 import scala.actors.Actor
 import scala.actors.Actor._
+import scala.collection.mutable
 
 import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
 import isabelle.prover.{Prover, ProverEvents, Command}
@@ -108,14 +109,14 @@
     // changes in buffer must be ignored
     buffer.removeBufferListener(this)
 
-    def apply(c: Change) = c.map {
-      case Insert(start, added) => buffer.insert(start, added)
-      case Remove(start, removed) => buffer.remove(start, removed.length)
+    def apply(change: Change): Unit = change.edits.foreach {
+      case Insert(start, text) => buffer.insert(start, text)
+      case Remove(start, text) => buffer.remove(start, text.length)
     }
 
-    def unapply(c: Change) = c.toList.reverse.map {
-      case Insert(start, added) => buffer.remove(start, added.length)
-      case Remove(start, removed) => buffer.insert(start, removed)
+    def unapply(change: Change): Unit = change.edits.reverse.foreach {
+      case Insert(start, text) => buffer.remove(start, text.length)
+      case Remove(start, text) => buffer.insert(start, text)
     }
 
     // undo/redo changes
@@ -151,36 +152,40 @@
     buffer.addBufferListener(this)
   }
 
+
   /* sending edits to prover */
 
-  private var edits: List[Edit] = Nil
+  private val edits = new mutable.ListBuffer[Edit]   // owned by Swing/AWT thread
 
   private val col_timer = new Timer(300, new ActionListener() {
-    override def actionPerformed(e: ActionEvent) = commit
+    override def actionPerformed(e: ActionEvent) = commit()
   })
 
   col_timer.stop
   col_timer.setRepeats(true)
 
-  private def commit: Unit = synchronized {
+  private def commit() {
+    Swing_Thread.require()
     if (!edits.isEmpty) {
-      val change = new Change(Isabelle.system.id(), Some(current_change), edits)
+      val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
       _changes ::= change
       prover ! change
       current_change = change
+      edits.clear
     }
-    edits = Nil
     if (col_timer.isRunning())
       col_timer.stop()
   }
 
   private def delay_commit {
+    Swing_Thread.require()
     if (col_timer.isRunning())
       col_timer.restart()
     else
       col_timer.start()
   }
 
+
   /* BufferListener methods */
 
   override def contentInserted(buffer: JEditBuffer,
@@ -192,14 +197,14 @@
   override def preContentInserted(buffer: JEditBuffer,
     start_line: Int, offset: Int, num_lines: Int, length: Int)
   {
-    edits ::= Insert(offset, buffer.getText(offset, length))
+    edits += Insert(offset, buffer.getText(offset, length))
     delay_commit
   }
 
   override def preContentRemoved(buffer: JEditBuffer,
     start_line: Int, start: Int, num_lines: Int, removed_length: Int)
   {
-    edits ::= Remove(start, buffer.getText(start, removed_length))
+    edits += Remove(start, buffer.getText(start, removed_length))
     delay_commit
   }
 
@@ -211,8 +216,8 @@
 
   /* transforming offsets */
 
-  private def changes_to(doc: ProofDocument) =
-    edits ::: current_change.ancestors(_.id == doc.id).flatten(_.toList)
+  private def changes_to(doc: ProofDocument): List[Edit] =
+    edits.toList ::: List.flatten(current_change.ancestors(_.id == doc.id).map(_.edits))
 
   def from_current(doc: ProofDocument, pos: Int) =
     (pos /: changes_to(doc)) ((p, c) => c from_where p)
@@ -314,9 +319,12 @@
   lazy val change_receiver: Actor = actor {
     loop {
       react {
-        case ProverEvents.Activate =>
-          edits = List(Insert(0, buffer.getText(0, buffer.getLength)))
-          commit
+        case ProverEvents.Activate =>   // FIXME !?
+          Swing_Thread.now {
+            edits.clear
+            edits += Insert(0, buffer.getText(0, buffer.getLength))
+            commit()
+          }
         case c: Command =>
           actor{Isabelle.plugin.command_change.event(c)}
           if(current_document().commands.contains(c))
diff -r 3c0a8bece8b8 -r 3e995f100ad2 src/Tools/jEdit/src/proofdocument/Change.scala
--- a/src/Tools/jEdit/src/proofdocument/Change.scala	Tue Sep 01 21:05:57 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Change.scala	Wed Sep 02 21:21:54 2009 +0200
@@ -7,41 +7,42 @@
 
 package isabelle.proofdocument
 
-abstract class Edit {
+sealed abstract class Edit
+{
   val start: Int
   def from_where (x: Int): Int //where has x been before applying this edit
   def where_to(x: Int): Int //where will x be when we apply this edit
 }
 
-case class Insert(start: Int, added: String) extends Edit {
+case class Insert(start: Int, text: String) extends Edit
+{
   def from_where(x: Int) =
     if (start > x) x
-    else (x - added.length) max start
+    else (x - text.length) max start
 
   def where_to(x: Int) =
-    if (start <= x) x + added.length else x
+    if (start <= x) x + text.length else x
 }
 
-case class Remove(start: Int, removed: String) extends Edit {
+case class Remove(start: Int, text: String) extends Edit
+{
   def from_where(x: Int) =
-    if (start <= x) x + removed.length else x
+    if (start <= x) x + text.length else x
 
   def where_to(x: Int) =
     if (start > x) x
-    else (x - removed.length) max start
+    else (x - text.length) max start
 }
 // TODO: merge multiple inserts?
 
 class Change(
   val id: String,
   val parent: Option[Change],
-  edits: List[Edit]) extends Iterable[Edit]
+  val edits: List[Edit])
 {
-  override def elements = edits.reverse.elements
-
-  def ancestors(root_p: Change => Boolean): List[Change] =
-    if (root_p(this)) Nil
-    else this :: parent.map(_.ancestors(root_p)).getOrElse(Nil)
+  def ancestors(done: Change => Boolean): List[Change] =
+    if (done(this)) Nil
+    else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
   def ancestors: List[Change] = ancestors(_ => false)
 
   override def toString =
diff -r 3c0a8bece8b8 -r 3e995f100ad2 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Sep 01 21:05:57 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Sep 02 21:21:54 2009 +0200
@@ -62,20 +62,20 @@
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
 
+  
   /** token view **/
 
-  def text_changed(c: Change): (ProofDocument, StructureChange)  =
+  def text_changed(change: Change): (ProofDocument, StructureChange) =
   {
     def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
       val (doc, chgs) = doc_chgs
-      val (new_doc, chg) = doc.text_edit(edit, c.id)
+      val (new_doc, chg) = doc.text_edit(edit, change.id)
       (new_doc, chgs ++ chg)
     }
-    ((this, Nil: StructureChange) /: c) (edit_doc)
+    ((this, Nil: StructureChange) /: change.edits)(edit_doc)
   }
 
-  def text_edit(e: Edit, id: String):
-    (ProofDocument,StructureChange) =
+  def text_edit(e: Edit, id: String): (ProofDocument,StructureChange) =
   {
     case class TextChange(start: Int, added: String, removed: String)
     val change = e match {