# HG changeset patch # User wenzelm # Date 1314286692 -7200 # Node ID 086bb10835528db0c0934583b95fd92636dc1d20 # Parent e8a87398f35d449f14b44c778b41e51b81289590 maintain last_execs assignment on Scala side; prefer tables over IDs instead of objects; diff -r e8a87398f35d -r 086bb1083552 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 25 16:44:06 2011 +0200 +++ b/src/Pure/PIDE/document.scala Thu Aug 25 17:38:12 2011 +0200 @@ -214,19 +214,21 @@ { class Fail(state: State) extends Exception - val init = State().define_version(Version.init, Map()).assign(Version.init.id, no_assign)._2 + val init = + State().define_version(Version.init, Map(), Map()).assign(Version.init.id, no_assign)._2 case class Assignment( - val assignment: Map[Command, Exec_ID], - val is_finished: Boolean = false) + val command_execs: Map[Command_ID, Exec_ID], + val last_execs: Map[String, Option[Command_ID]], + val is_finished: Boolean) { - def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment } - def assign(command_execs: List[(Command, Exec_ID)], - last_commands: List[(String, Option[Command])]): Assignment = + def check_finished: Assignment = { require(is_finished); this } + def assign(add_command_execs: List[(Command_ID, Exec_ID)], + add_last_execs: List[(String, Option[Command_ID])]): Assignment = { require(!is_finished) // FIXME maintain last_commands - Assignment(assignment ++ command_execs, true) + Assignment(command_execs ++ add_command_execs, last_execs ++ add_last_execs, true) } } } @@ -241,12 +243,14 @@ { private def fail[A]: A = throw new State.Fail(this) - def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State = + def define_version(version: Version, + command_execs: Map[Command_ID, Exec_ID], + last_execs: Map[String, Option[Command_ID]]): State = { val id = version.id if (versions.isDefinedAt(id) || disposed(id)) fail copy(versions = versions + (id -> version), - assignments = assignments + (id -> State.Assignment(former_assignment))) + assignments = assignments + (id -> State.Assignment(command_execs, last_execs, false))) } def define_command(command: Command): State = @@ -281,25 +285,19 @@ def assign(id: Version_ID, arg: Assign): (List[Command], State) = { val version = the_version(id) - val (edits, last_ids) = arg + val (command_execs, last_execs) = arg - var new_execs = execs - val assigned_execs = - for ((cmd_id, exec_id) <- edits) yield { - val st = the_command(cmd_id) - if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail - new_execs += (exec_id -> st) - (st.command, exec_id) + val new_execs = + (execs /: command_execs) { + case (execs1, (cmd_id, exec_id)) => + if (execs1.isDefinedAt(exec_id) || disposed(exec_id)) fail + execs1 + (exec_id -> the_command(cmd_id)) } - - val last_commands = - last_ids map { - case (name, Some(cmd_id)) => (name, Some(the_command(cmd_id).command)) - case (name, None) => (name, None) } - val new_assignment = the_assignment(version).assign(assigned_execs, last_commands) + val new_assignment = the_assignment(version).assign(command_execs, last_execs) val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) - (assigned_execs.map(_._1), new_state) + val commands = command_execs.map(p => the_command(p._1).command) + (commands, new_state) } def is_assigned(version: Version): Boolean = @@ -346,7 +344,10 @@ def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id) def state(command: Command): Command.State = - try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) } + try { + the_exec(the_assignment(version).check_finished.command_execs + .getOrElse(command.id, fail)) + } catch { case _: State.Fail => command.empty_state } def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) diff -r e8a87398f35d -r 086bb1083552 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Aug 25 16:44:06 2011 +0200 +++ b/src/Pure/System/session.scala Thu Aug 25 17:38:12 2011 +0200 @@ -215,8 +215,8 @@ global_state.change_yield( _.continue_history(Future.value(previous), text_edits, Future.value(version))) - val assignment = global_state().the_assignment(previous).get_finished - global_state.change(_.define_version(version, assignment)) + val assignment = global_state().the_assignment(previous).check_finished + global_state.change(_.define_version(version, assignment.command_execs, assignment.last_execs)) global_state.change_yield(_.assign(version.id, Document.no_assign)) prover.get.update_perspective(previous.id, version.id, name, perspective) @@ -268,12 +268,14 @@ val name = change.name val doc_edits = change.doc_edits - var former_assignment = global_state().the_assignment(previous).get_finished + val previous_assignment = global_state().the_assignment(previous).check_finished + + var command_execs = previous_assignment.command_execs for { (name, Document.Node.Edits(cmd_edits)) <- doc_edits // FIXME proper coverage!? (prev, None) <- cmd_edits removed <- previous.nodes(name).commands.get_after(prev) - } former_assignment -= removed + } command_execs -= removed.id def id_command(command: Command) { @@ -287,7 +289,7 @@ edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command } } - global_state.change(_.define_version(version, former_assignment)) + global_state.change(_.define_version(version, command_execs, previous_assignment.last_execs)) prover.get.edit_version(previous.id, version.id, doc_edits) } //}}}