# HG changeset patch
# User wenzelm
# Date 1262363375 -3600
# Node ID ac35eee85f5c7a9770b1b08dd8adf82cc8c36817
# Parent  2f3ea37c5958c2d1569ecdb64831fd6d12a1c281
renamed current_document to recent_document (might be a bit older than current_change);
Change: explicit future value of Document.Change instead of implicit lookup in Session database;
Document_Model: apply Document.text_edits here (as future);

diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -10,6 +10,8 @@
 
 import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, Document, Session}
 
+import scala.actors.Future
+import scala.actors.Futures._
 import scala.actors.Actor, Actor._
 import scala.collection.mutable
 
@@ -60,7 +62,8 @@
 
   private val document_0 = session.begin_document(buffer.getName)
 
-  private val change_0 = new Change(document_0.id, None, Nil)  // FIXME !?
+  private val change_0 =
+    new Change(document_0.id, None, Nil, future { (document_0, Nil) })  // FIXME more robust history start
   private var _changes = List(change_0)   // owned by Swing thread
   def changes = _changes
   private var current_change = change_0
@@ -69,10 +72,18 @@
 
   private val edits_delay = Swing_Thread.delay_last(300) {
     if (!edits.isEmpty) {
-      val change = new Change(session.create_id(), Some(current_change), edits.toList)
-      _changes ::= change
-      session.input(change)
-      current_change = change
+      val new_id = session.create_id()
+      val eds = edits.toList
+      val change1 = current_change
+      val result: Future[Document.Result] = future {
+        val old_doc = change1.document
+        Document.text_edits(session, old_doc, new_id, eds)
+      }
+      result()  // FIXME !?!?!?
+      val change2 = new Change(new_id, Some(change1), eds, result)
+      _changes ::= change2
+      session.input(change2)
+      current_change = change2
       edits.clear
     }
   }
@@ -100,10 +111,13 @@
 
   /* history of changes */
 
-  private def doc_or_pred(c: Change): Document =
-    session.document(c.id).getOrElse(doc_or_pred(c.parent.get))
-
-  def current_document() = doc_or_pred(current_change)
+  def recent_document(): Document =
+  {
+    def find(change: Change): Document =
+      if (change.result.isSet || !change.parent.isDefined) change.document
+      else find(change.parent.get)
+    find(current_change)
+  }
 
 
   /* transforming offsets */
@@ -120,7 +134,7 @@
 
   def lines_of_command(cmd: Command): (Int, Int) =
   {
-    val document = current_document()
+    val document = recent_document()
     (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
      buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
   }
diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -82,7 +82,7 @@
     loop {
       react {
         case command: Command =>
-          if (model.current_document().commands.contains(command))
+          if (model.recent_document().commands.contains(command))
             Swing_Thread.now {
               update_syntax(command)
               invalidate_line(command)
@@ -104,7 +104,7 @@
     override def paintValidLine(gfx: Graphics2D,
       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
     {
-      val document = model.current_document()
+      val document = model.recent_document()
       def from_current(pos: Int) = model.from_current(document, pos)
       def to_current(pos: Int) = model.to_current(document, pos)
       val saved_color = gfx.getColor
@@ -127,7 +127,7 @@
 
     override def getToolTipText(x: Int, y: Int): String =
     {
-      val document = model.current_document()
+      val document = model.recent_document()
       val offset = model.from_current(document, text_area.xyToOffset(x, y))
       document.command_at(offset) match {
         case Some(cmd) =>
@@ -152,7 +152,7 @@
   private val caret_listener = new CaretListener
   {
     override def caretUpdate(e: CaretEvent) {
-      val doc = model.current_document()
+      val doc = model.recent_document()
       doc.command_at(e.getDot) match {
         case Some(cmd)
           if (doc.token_start(cmd.tokens.first) <= e.getDot &&
@@ -249,7 +249,7 @@
     override def paintComponent(gfx: Graphics)
     {
       super.paintComponent(gfx)
-      val doc = model.current_document()
+      val doc = model.recent_document()
       val buffer = model.buffer
 
       for (command <- doc.commands) {
diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -41,7 +41,7 @@
 	{
     Document_Model(buffer) match {
       case Some(model) =>
-        val document = model.current_document()
+        val document = model.recent_document()
         val offset = model.from_current(document, original_offset)
         document.command_at(offset) match {
           case Some(command) =>
diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -43,7 +43,7 @@
 
     Swing_Thread.now { Document_Model(buffer) } match {
       case Some(model) =>
-        val document = model.current_document()
+        val document = model.recent_document()
         for (command <- document.commands if !stopped) {
           root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
               {
diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -110,7 +110,7 @@
     val start = model.buffer.getLineStartOffset(line)
     val stop = start + line_segment.count
 
-    val document = model.current_document()
+    val document = model.recent_document()
     def to: Int => Int = model.to_current(document, _)
     def from: Int => Int = model.from_current(document, _)
 
diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -40,7 +40,7 @@
             case Some(model) =>
               val body =
                 if (cmd == null) Nil  // FIXME ??
-                else cmd.results(model.current_document)
+                else cmd.results(model.recent_document)
               html_panel.render(body)
           }
 
diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/proofdocument/change.scala
--- a/src/Tools/jEdit/src/proofdocument/change.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/change.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -8,6 +8,9 @@
 package isabelle.proofdocument
 
 
+import scala.actors.Future
+
+
 sealed abstract class Edit
 {
   val start: Int
@@ -40,15 +43,17 @@
 
 
 class Change(
-  val id: String,
+  val id: Isar_Document.Document_ID,
   val parent: Option[Change],
-  val edits: List[Edit])
+  val edits: List[Edit],
+  val result: Future[Document.Result])
 {
+  // FIXME iterator
   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 =
-    "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")"
+  def document: Document = result()._1
+  def document_edits: List[Document.Structure_Edit] = result()._2
 }
\ No newline at end of file
diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/proofdocument/document.scala
--- a/src/Tools/jEdit/src/proofdocument/document.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -9,7 +9,10 @@
 package isabelle.proofdocument
 
 
+import scala.actors.Future
+import scala.actors.Futures._
 import scala.actors.Actor._
+import scala.collection.mutable
 
 import java.util.regex.Pattern
 
@@ -35,7 +38,22 @@
   def empty(id: Isar_Document.Document_ID): Document =
     new Document(id, Linear_Set(), Map(), Linear_Set(), Map())
 
-  type StructureChange = List[(Option[Command], Option[Command])]
+  type Structure_Edit = (Option[Command], Option[Command])
+  type Structure_Change = List[Structure_Edit]
+  type Result = (Document, List[Structure_Edit])
+
+  def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
+    edits: List[Edit]): Result =
+  {
+    val changes = new mutable.ListBuffer[Structure_Edit]
+    val new_doc = (old_doc /: edits)((doc1: Document, edit: Edit) =>
+      {
+        val (doc2, chgs) = doc1.text_edit(session, edit, new_id)  // FIXME odd multiple use of id
+        changes ++ chgs
+        doc2
+      })
+    (new_doc, changes.toList)
+  }
 }
 
 
@@ -47,8 +65,6 @@
     var states: Map[Command, Command])   // FIXME immutable, eliminate!?
   extends Session.Entity
 {
-  import Document.StructureChange
-
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
 
@@ -66,7 +82,7 @@
               } {
                 session.lookup_entity(cmd_id) match {
                   case Some(cmd: Command) =>
-                    val state = cmd.finish_static(state_id)
+                    val state = cmd.finish_static(state_id)   // FIXME more explicit typing
                     session.register_entity(state)
                     states += (cmd -> state)  // FIXME !?
                     session.command_change.event(cmd)   // FIXME really!?
@@ -87,17 +103,7 @@
 
   /** token view **/
 
-  def text_changed(session: Session, change: Change): (Document, StructureChange) =
-  {
-    def edit_doc(doc_chgs: (Document, StructureChange), edit: Edit) = {
-      val (doc, chgs) = doc_chgs
-      val (new_doc, chg) = doc.text_edit(session, edit, change.id)
-      (new_doc, chgs ++ chg)
-    }
-    ((this, Nil: StructureChange) /: change.edits)(edit_doc)
-  }
-
-  def text_edit(session: Session, e: Edit, id: String): (Document, StructureChange) =
+  def text_edit(session: Session, e: Edit, id: String): Document.Result =
   {
     case class TextChange(start: Int, added: String, removed: String)
     val change = e match {
@@ -179,14 +185,14 @@
   /** command view **/
 
   private def token_changed(
-    session: Session,
-    new_id: String,
-    before_change: Option[Token],
-    inserted_tokens: List[Token],
-    after_change: Option[Token],
-    new_tokens: List[Token],
-    new_token_start: Map[Token, Int]):
-  (Document, StructureChange) =
+      session: Session,
+      new_id: String,
+      before_change: Option[Token],
+      inserted_tokens: List[Token],
+      after_change: Option[Token],
+      new_tokens: List[Token],
+      new_token_start: Map[Token, Int]):
+    Document.Result =
   {
     val new_tokenset = Linear_Set[Token]() ++ new_tokens
     val cmd_before_change = before_change match {
@@ -278,7 +284,7 @@
   val commands_offsets = {
     var last_stop = 0
     (for (c <- commands) yield {
-      val r = c -> (last_stop,c.stop(this))
+      val r = c -> (last_stop, c.stop(this))
       last_stop = c.stop(this)
       r
     }).toArray
diff -r 2f3ea37c5958 -r ac35eee85f5c src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Fri Jan 01 17:29:35 2010 +0100
@@ -80,9 +80,9 @@
 
     def handle_change(change: Change)
     {
-      val old = document(change.parent.get.id).get
-      val (doc, changes) = old.text_changed(this, change)
+      require(change.parent.isDefined)
 
+      val (doc, changes) = change.result()  // FIXME clarify future vs. actor arrangement
       val id_changes = changes map {
         case (c1, c2) =>
           (c1.map(_.id).getOrElse(""),
@@ -95,8 +95,8 @@
             })
       }
       register(doc)
-      documents += (doc.id -> doc)
-      prover.edit_document(old.id, doc.id, id_changes)
+      documents += (doc.id -> doc)  // FIXME remove
+      prover.edit_document(change.parent.get.document.id, doc.id, id_changes)
 
       document_change.event(doc)
     }
@@ -221,6 +221,7 @@
 
   /* main methods */
 
+  // FIXME private?
   def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
 
   def start(timeout: Int, args: List[String]): Option[String] =