maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
--- a/src/Pure/System/session.scala Sat Aug 07 16:49:03 2010 +0200
+++ b/src/Pure/System/session.scala Sat Aug 07 17:24:46 2010 +0200
@@ -9,6 +9,7 @@
import scala.actors.TIMEOUT
+import scala.actors.Actor
import scala.actors.Actor._
@@ -259,7 +260,7 @@
- /** buffered command changes -- delay_first discipline **/
+ /** buffered command changes (delay_first discipline) **/
private lazy val command_change_buffer = actor
//{{{
@@ -307,36 +308,49 @@
}
- /* main methods */
+
+ /** editor history **/
+
+ private case class Edit_Document(edits: List[Document.Node_Text_Edit])
+
+ private val editor_history = new Actor
+ {
+ @volatile private var history = Change.init
+ def current_change(): Change = history
+
+ def act
+ {
+ loop {
+ react {
+ case Edit_Document(edits) =>
+ val old_change = history
+ val new_id = create_id()
+ val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
+ isabelle.Future.fork {
+ val old_doc = old_change.join_document
+ old_doc.await_assignment
+ Document.text_edits(Session.this, old_doc, new_id, edits)
+ }
+ val new_change = new Change(new_id, Some(old_change), edits, result)
+ history = new_change
+ new_change.result.map(_ => session_actor ! new_change)
+
+ case bad => System.err.println("editor_model: ignoring bad message " + bad)
+ }
+ }
+ }
+ }
+ editor_history.start
+
+
+
+ /** main methods **/
def started(timeout: Int, args: List[String]): Option[String] =
(session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
def stop() { session_actor ! Stop }
- def input(change: Change) { session_actor ! change }
-
-
-
- /** editor model **/ // FIXME subclass Editor_Session (!?)
-
- @volatile private var history = Change.init // owned by Swing thread (!??)
- def current_change(): Change = history
-
- def edit_document(edits: List[Document.Node_Text_Edit])
- {
- Swing_Thread.now {
- val old_change = current_change()
- val new_id = create_id()
- val result: Future[(List[Document.Edit[Command]], Document)] =
- Future.fork {
- val old_doc = old_change.join_document
- old_doc.await_assignment
- Document.text_edits(this, old_doc, new_id, edits)
- }
- val new_change = new Change(new_id, Some(old_change), edits, result)
- history = new_change
- new_change.result.map(_ => input(new_change))
- }
- }
+ def current_change(): Change = editor_history.current_change()
+ def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
}