1.1 --- a/src/Pure/System/session.scala Sat Aug 07 16:49:03 2010 +0200
1.2 +++ b/src/Pure/System/session.scala Sat Aug 07 17:24:46 2010 +0200
1.3 @@ -9,6 +9,7 @@
1.4
1.5
1.6 import scala.actors.TIMEOUT
1.7 +import scala.actors.Actor
1.8 import scala.actors.Actor._
1.9
1.10
1.11 @@ -259,7 +260,7 @@
1.12
1.13
1.14
1.15 - /** buffered command changes -- delay_first discipline **/
1.16 + /** buffered command changes (delay_first discipline) **/
1.17
1.18 private lazy val command_change_buffer = actor
1.19 //{{{
1.20 @@ -307,36 +308,49 @@
1.21 }
1.22
1.23
1.24 - /* main methods */
1.25 +
1.26 + /** editor history **/
1.27 +
1.28 + private case class Edit_Document(edits: List[Document.Node_Text_Edit])
1.29 +
1.30 + private val editor_history = new Actor
1.31 + {
1.32 + @volatile private var history = Change.init
1.33 + def current_change(): Change = history
1.34 +
1.35 + def act
1.36 + {
1.37 + loop {
1.38 + react {
1.39 + case Edit_Document(edits) =>
1.40 + val old_change = history
1.41 + val new_id = create_id()
1.42 + val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
1.43 + isabelle.Future.fork {
1.44 + val old_doc = old_change.join_document
1.45 + old_doc.await_assignment
1.46 + Document.text_edits(Session.this, old_doc, new_id, edits)
1.47 + }
1.48 + val new_change = new Change(new_id, Some(old_change), edits, result)
1.49 + history = new_change
1.50 + new_change.result.map(_ => session_actor ! new_change)
1.51 +
1.52 + case bad => System.err.println("editor_model: ignoring bad message " + bad)
1.53 + }
1.54 + }
1.55 + }
1.56 + }
1.57 + editor_history.start
1.58 +
1.59 +
1.60 +
1.61 + /** main methods **/
1.62
1.63 def started(timeout: Int, args: List[String]): Option[String] =
1.64 (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
1.65
1.66 def stop() { session_actor ! Stop }
1.67
1.68 - def input(change: Change) { session_actor ! change }
1.69 -
1.70 -
1.71 -
1.72 - /** editor model **/ // FIXME subclass Editor_Session (!?)
1.73 -
1.74 - @volatile private var history = Change.init // owned by Swing thread (!??)
1.75 - def current_change(): Change = history
1.76 -
1.77 - def edit_document(edits: List[Document.Node_Text_Edit])
1.78 - {
1.79 - Swing_Thread.now {
1.80 - val old_change = current_change()
1.81 - val new_id = create_id()
1.82 - val result: Future[(List[Document.Edit[Command]], Document)] =
1.83 - Future.fork {
1.84 - val old_doc = old_change.join_document
1.85 - old_doc.await_assignment
1.86 - Document.text_edits(this, old_doc, new_id, edits)
1.87 - }
1.88 - val new_change = new Change(new_id, Some(old_change), edits, result)
1.89 - history = new_change
1.90 - new_change.result.map(_ => input(new_change))
1.91 - }
1.92 - }
1.93 + def current_change(): Change = editor_history.current_change()
1.94 + def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
1.95 }