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);
--- 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))))
}
--- 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) {
--- 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) =>
--- 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) =>
{
--- 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, _)
--- 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)
}
--- 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
--- 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
--- 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] =