src/Tools/jEdit/src/jedit/TheoryView.scala

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Jul 08 13:29:44 2009 +0200
@@ -54,6 +54,8 @@
 
 
   private var col: Text.Change = null
+  private var doc_id: IsarDocument.Document_ID = prover.document(null).id
+  def current_document() = prover.document(doc_id)
 
   private val col_timer = new Timer(300, new ActionListener() {
     override def actionPerformed(e: ActionEvent) = commit
@@ -70,7 +72,7 @@
 
   private val selected_state_controller = new CaretListener {
     override def caretUpdate(e: CaretEvent) = {
-      val doc = prover.document
+      val doc = current_document()
       val cmd = doc.find_command_at(e.getDot)
       if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
           Isabelle.prover_setup(buffer).get.selected_state != cmd)
@@ -85,12 +87,9 @@
     buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
     buffer.addBufferListener(this)
 
-    val MAX = TheoryView.MAX_CHANGE_LENGTH
-    for (i <- 0 to buffer.getLength / MAX) {
-      prover ! new isabelle.proofdocument.Text.Change(
-        Isabelle.system.id(), i * MAX,
-        buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), "")
-    }
+    col = Text.Change(doc_id, Isabelle.system.id(), 0,
+      buffer.getText(0, buffer.getLength), "")
+    commit
   }
 
   def deactivate() {
@@ -124,7 +123,7 @@
   def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int =
     changes match {
       case Nil => pos
-      case Text.Change(id, start, added, removed) :: rest_changes => {
+      case Text.Change(_, id, start, added, removed) :: rest_changes => {
         val shifted =
           if (start <= pos)
             if (pos < start + added.length) start
@@ -138,7 +137,7 @@
   def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int =
     changes match {
       case Nil => pos
-      case Text.Change(id, start, added, removed) :: rest_changes => {
+      case Text.Change(_, id, start, added, removed) :: rest_changes => {
         val shifted = _to_current(from_id, rest_changes, pos)
         if (id == from_id) pos
         else if (start <= shifted) {
@@ -159,7 +158,7 @@
 
   def repaint(cmd: Command) =
   {
-    val document = prover.document
+    val document = current_document()
     if (text_area != null) {
       val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document)))
       val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1)
@@ -202,7 +201,7 @@
   override def paintValidLine(gfx: Graphics2D,
     screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   {
-    val document = prover.document
+    val document = current_document()
     def from_current(pos: Int) = this.from_current(document.id, pos)
     def to_current(pos: Int) = this.to_current(document.id, pos)
     val saved_color = gfx.getColor
@@ -222,7 +221,7 @@
   }
 
   override def getToolTipText(x: Int, y: Int) = {
-    val document = prover.document
+    val document = current_document()
     val offset = from_current(document.id, text_area.xyToOffset(x, y))
     val cmd = document.find_command_at(offset)
     if (cmd != null) {
@@ -240,12 +239,13 @@
       def split_changes(c: Text.Change): List[Text.Change] = {
         val MAX = TheoryView.MAX_CHANGE_LENGTH
         if (c.added.length <= MAX) List(c)
-        else Text.Change(c.id, c.start, c.added.substring(0, MAX), c.removed) ::
-          split_changes(new Text.Change(id(), c.start + MAX, c.added.substring(MAX), c.removed))
+        else Text.Change(c.base_id, c.id, c.start, c.added.substring(0, MAX), c.removed) ::
+          split_changes(new Text.Change(c.id, id(), c.start + MAX, c.added.substring(MAX), ""))
       }
       val new_changes = split_changes(col)
       changes = new_changes.reverse ::: changes
       new_changes map (document_actor ! _)
+      doc_id = new_changes.last.id
     }
     col = null
     if (col_timer.isRunning())
@@ -271,12 +271,12 @@
   {
     val text = buffer.getText(offset, length)
     if (col == null)
-      col = new Text.Change(id(), offset, text, "")
+      col = new Text.Change(doc_id, id(), offset, text, "")
     else if (col.start <= offset && offset <= col.start + col.added.length)
-      col = new Text.Change(col.id, col.start, col.added + text, col.removed)
+      col = new Text.Change(doc_id, col.id, col.start, col.added + text, col.removed)
     else {
       commit
-      col = new Text.Change(id(), offset, text, "")
+      col = new Text.Change(doc_id, id(), offset, text, "")
     }
     delay_commit
   }
@@ -286,10 +286,10 @@
   {
     val removed = buffer.getText(start, removed_length)
     if (col == null)
-      col = new Text.Change(id(), start, "", removed)
+      col = new Text.Change(doc_id, id(), start, "", removed)
     else if (col.start > start + removed_length || start > col.start + col.added.length) {
       commit
-      col = new Text.Change(id(), start, "", removed)
+      col = new Text.Change(doc_id, id(), start, "", removed)
     }
     else {
 /*      val offset = start - col.start
@@ -301,7 +301,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(id(), start, "", removed)
+      col = new Text.Change(doc_id, id(), start, "", removed)
     }
     delay_commit
   }