current version in theoryview/buffer

--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Jul 08 13:29:44 2009 +0200
@@ -106,14 +106,13 @@
     val start = buffer.getLineStartOffset(line)
     val stop = start + line_segment.count
 
-    val document = prover.document
     val theory_view = Isabelle.prover_setup(buffer).get.theory_view
+    val document = theory_view.current_document()
     def to: Int => Int = theory_view.to_current(document.id, _)
     def from: Int => Int = theory_view.from_current(document.id, _)
 
+    var command = document.find_command_at(from(start))
     var next_x = start
-
-    var command = document.find_command_at(from(start))
     while (command != null && command.start(document) < from(stop)) {
       for {
         markup <- command.highlight_node.flatten

--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Wed Jul 08 13:29:44 2009 +0200
@@ -48,8 +48,8 @@
     if (!prover.isDefined || !theory_view_opt.isDefined) null
     else if (prover.get == null || theory_view_opt.get == null) null
     else {
-      val document = prover.get.document
       val theory_view = theory_view_opt.get
+      val document = theory_view.current_document()
       val offset = theory_view.from_current(document, original_offset)
       val cmd = document.find_command_at(offset)
       if (cmd != null) {

--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Wed Jul 08 13:29:44 2009 +0200
@@ -32,7 +32,7 @@
 
     val prover_setup = Isabelle.plugin.prover_setup(buffer)
     if (prover_setup.isDefined) {
-      val document = prover_setup.get.prover.document
+      val document = prover_setup.get.theory_view.current_document()
       for (command <- document.commands)
         data.root.add(command.markup_root.swing_node(document))
 

--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Jul 08 13:29:44 2009 +0200
@@ -79,9 +79,9 @@
 
 	override def paintComponent(gfx : Graphics) {
 		super.paintComponent(gfx)
-
 		val buffer = textarea.getBuffer
-    val document = prover.document
+    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
+    val document = theory_view.current_document()
     for (c <- document.commands)
       paintCommand(c, buffer, document, gfx)
 

--- 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
   }

--- a/src/Tools/jEdit/src/proofdocument/Text.scala	Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala	Wed Jul 08 13:29:44 2009 +0200
@@ -8,7 +8,12 @@
 
 
 object Text {
-  case class Change(id: String, start: Int, val added: String, val removed: String) {
+  case class Change(
+    base_id: String,
+    id: String,
+    start: Int,
+    added: String,
+    removed: String) {
     override def toString = "start: " + start + " added: " + added + " removed: " + removed
   }
 }
\ No newline at end of file

--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Jul 08 13:29:43 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Jul 08 13:29:44 2009 +0200
@@ -23,8 +23,6 @@
 
 object ProverEvents {
   case class Activate
-  case class SetEventBus(bus: EventBus[StructureChange])
-  case class SetIsCommandKeyword(is_command_keyword: String => Boolean)
 }
 
 class Prover(isabelle_system: Isabelle_System, logic: String) extends Actor
@@ -47,12 +45,13 @@
     mutable.SynchronizedMap[IsarDocument.State_ID, Command]
   private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
     mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
-  private var document_versions =
-    List(ProofDocument.empty.set_command_keyword(command_decls.contains))
-  private val document_id0 = ProofDocument.empty.id
+  private val document_0 =
+    ProofDocument.empty.set_command_keyword(command_decls.contains)
+  private var document_versions = List(document_0)
 
   def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
-  def document = document_versions.head
+  def document(id: IsarDocument.Document_ID) =
+    document_versions.find(_.id == id).getOrElse(document_0)
 
   private var initialized = false
 
@@ -91,7 +90,7 @@
   
   private def handle_result(result: Isabelle_Process.Result)
   {
-    def command_change(c: Command) = this ! c
+    def command_change(c: Command) = change_receiver ! c
     val (running, command) =
       result.props.find(p => p._1 == Markup.ID) match {
         case None => (false, null)
@@ -231,38 +230,34 @@
     loop {
       react {
         case change: Text.Change => {
-            val old = document
+            val old = document(change.base_id)
             val (doc, structure_change) = old.text_changed(change)
             document_versions ::= doc
-            edit_document(old.id, doc.id, structure_change)
+            edit_document(old, doc, structure_change)
         }
-        case command: Command => {
-            //state of command has changed
-            change_receiver ! command
-        }
+        case x => System.err.println("warning: ignored " + x)
       }
     }
   }
   
   def set_document(change_receiver: Actor, path: String) {
     this.change_receiver = change_receiver
-    process.begin_document(document_id0, path)
+    process.begin_document(document_0.id, path)
   }
 
-  private def edit_document(old_id: String, document_id: String, changes: StructureChange) =
-    Swing_Thread.now {
-      val removes =
-        for (cmd <- changes.removed_commands) yield {
-          commands -= cmd.id
-          if (cmd.state_id != null) states -= cmd.state_id
-          changes.before_change.map(_.id).getOrElse(document_id0) -> None
-        }
-      val inserts =
-        for (cmd <- changes.added_commands) yield {
-          commands += (cmd.id -> cmd)
-          process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
-          (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id)
-        }
-      process.edit_document(old_id, document_id, removes.reverse ++ inserts)
-    }
+  private def edit_document(old: ProofDocument, doc: ProofDocument, changes: StructureChange) = {
+    val removes =
+      for (cmd <- changes.removed_commands) yield {
+        commands -= cmd.id
+        if (cmd.state_id != null) states -= cmd.state_id
+        changes.before_change.map(_.id).getOrElse(document_0.id) -> None
+      }
+    val inserts =
+      for (cmd <- changes.added_commands) yield {
+        commands += (cmd.id -> cmd)
+        process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
+        (doc.commands.prev(cmd).map(_.id).getOrElse(document_0.id)) -> Some(cmd.id)
+      }
+    process.edit_document(old.id, doc.id, removes.reverse ++ inserts)
+  }
 }