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

   private val buffer = text_area.getBuffer
   private val prover = Isabelle.prover_setup(buffer).get.prover
 
 
   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
   })
 

 
   /* activation */
 
   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)
         Isabelle.prover_setup(buffer).get.selected_state = cmd
     }

     text_area.addLeftOfScrollBar(phase_overview)
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
     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() {
     buffer.setTokenMarker(buffer.getMode.getTokenMarker)
     buffer.removeBufferListener(this)

   }
 
   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
             else pos - added.length + removed.length
           else pos

     }
 
   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) {
           if (shifted < start + removed.length) start
           else shifted + added.length - removed.length

   def from_current(document: isabelle.proofdocument.ProofDocument, pos: Int): Int =
     from_current(document.id, pos)
 
   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)
       text_area.invalidateLineRange(start, stop)
 

   /* TextAreaExtension methods */
 
   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
 
     val metrics = text_area.getPainter.getFontMetrics

 
     gfx.setColor(saved_color)
   }
 
   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) {
       document.token_start(cmd.tokens.first)
       cmd.type_at(offset - cmd.start(document))

   private def commit: Unit = synchronized {
     if (col != null) {
       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())
       col_timer.stop()
   }

   override def preContentInserted(buffer: JEditBuffer,
     start_line: Int, offset: Int, num_lines: Int, length: Int)
   {
     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
   }
 
   override def preContentRemoved(buffer: JEditBuffer,
     start_line: Int, start: Int, num_lines: Int, removed_length: Int)
   {
     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
       val diff = col.added.length - removed
       val (added, add_removed) =

           (offset max 0, diff - (offset max 0))
         else
           (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
   }
 
   override def bufferLoaded(buffer: JEditBuffer) { }