1.1 --- a/src/Pure/System/session.scala	Sun Aug 15 20:27:29 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sun Aug 15 21:03:13 2010 +0200
     1.3 @@ -290,56 +290,26 @@
     1.4  
     1.5    private val editor_history = new Actor
     1.6    {
     1.7 -    @volatile private var history = List(Document.Change.init)
     1.8 +    @volatile private var history = Document.History.init
     1.9  
    1.10      def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
    1.11 -    {
    1.12 -      val state_snapshot = current_state()
    1.13 -      val history_snapshot = history
    1.14 -
    1.15 -      val found_stable = history_snapshot.find(change =>
    1.16 -        change.is_finished && state_snapshot.is_assigned(change.current.join))
    1.17 -      require(found_stable.isDefined)
    1.18 -      val stable = found_stable.get
    1.19 -      val latest = history_snapshot.head
    1.20 -
    1.21 -      val edits =
    1.22 -        (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
    1.23 -            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
    1.24 -      lazy val reverse_edits = edits.reverse
    1.25 -
    1.26 -      new Document.Snapshot {
    1.27 -        val version = stable.current.join
    1.28 -        val node = version.nodes(name)
    1.29 -        val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.30 -        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    1.31 -        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.32 -        def lookup_command(id: Document.Command_ID): Option[Command] =
    1.33 -          state_snapshot.lookup_command(id)
    1.34 -        def state(command: Command): Command.State =
    1.35 -          try { state_snapshot.command_state(version, command) }
    1.36 -          catch { case _: Document.State.Fail => command.empty_state }
    1.37 -      }
    1.38 -    }
    1.39 +      history.snapshot(name, pending_edits, current_state())
    1.40  
    1.41      def act
    1.42      {
    1.43        loop {
    1.44          react {
    1.45            case Edit_Version(edits) =>
    1.46 -            val history_snapshot = history
    1.47 -            require(!history_snapshot.isEmpty)
    1.48 -
    1.49 -            val prev = history_snapshot.head.current
    1.50 +            val prev = history.tip.current
    1.51              val result =
    1.52                isabelle.Future.fork {
    1.53                  val previous = prev.join
    1.54                  val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
    1.55                  Thy_Syntax.text_edits(Session.this, previous, edits)
    1.56                }
    1.57 -            val new_change = new Document.Change(prev, edits, result)
    1.58 -            history ::= new_change
    1.59 -            new_change.current.map(_ => session_actor ! new_change)
    1.60 +            val change = new Document.Change(prev, edits, result)
    1.61 +            history += change
    1.62 +            change.current.map(_ => session_actor ! change)
    1.63              reply(())
    1.64  
    1.65            case bad => System.err.println("editor_model: ignoring bad message " + bad)