Pure/PIDE/document.scala

432         val version = future.join
433         versions.get(version.id) match {
434           case Some(version1) if !(version eq version1) => Future.value(version1)
466     def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
467       new Change(Some(previous), edits.reverse, version)
473     val version: Future[Version] = Future.value(Version.init))
477       version.is_finished
479     def truncate: Change = new Change(None, Nil, version)
484       val version1 = Version.purge_future(versions, version)
485       if ((previous eq previous1) && (version eq version1)) None
536     def version: Version
676     /*command-exec assignment for each version*/
697     def define_version(version: Version, assignment: State.Assignment): State =
699       val id = version.id
700       copy(versions = versions + (id -> version),
718     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
774     def node_exports(version: Version, node_name: Node.Name): Command.Exports =
777           command <- version.nodes(node_name).commands.iterator
778           st <- command_states(version, command).iterator
784       val version = the_version(id)
788         (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
809       val new_assignment = the_assignment(version).assign(update)
815     def is_assigned(version: Version): Boolean =
816       assignments.get(version.id) match {
822       change.is_finished && is_assigned(change.version.get_finished)
827       if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None
832       version: Future[Version]): State =
834       val change = Change.make(previous, edits, version)
842           val old_versions = dropped.map(change => change.version.get_finished)
860         (version_id, version) <- versions1.iterator
862         (_, node) <- version.nodes.iterator
890     def command_id_map(version: Version, commands: Iterable[Command])
893       require(is_assigned(version))
894       val assignment = the_assignment(version).check_finished
901     def command_maybe_consolidated(version: Version, command: Command): Boolean =
903       require(is_assigned(version))
905         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
915     private def command_states_self(version: Version, command: Command)
918       require(is_assigned(version))
920         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
933     def command_states(version: Version, command: Command): List[Command.State] =
935       val self = command_states_self(version, command)
940             (id, st) <- command_states_self(version, the_static_state(command_id).command)
948     def command_results(version: Version, command: Command): Command.Results =
949       Command.State.merge_results(command_states(version, command))
951     def command_markup(version: Version, command: Command, index: Command.Markup_Index,
953       Command.State.merge_markup(command_states(version, command), index, range, elements)
956       version: Version,
961       val node = version.nodes(node_name)
967           markup = command_markup(version, command, markup_index, command_range, elements)
977               version.nodes.commands_loading(node_name).headOption match {
982                   command_markup(version, command, markup_index, node_range, elements)
989     def node_initialized(version: Version, name: Node.Name): Boolean =
991       (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
993         case Some(command) => command_states(version, command).headOption.exists(_.initialized)
996     def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
998       version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _))
1000     def node_consolidated(version: Version, name: Node.Name): Boolean =
1003         val it = version.nodes(name).commands.reverse.iterator
1004         it.hasNext && command_states(version, it.next).exists(_.consolidated)
1036         val version: Version = stable.version.get_finished
1049         val node: Node = version.nodes(name)
1053             map(name => (name, version.nodes(name)))
1057           else version.nodes.commands_loading(node_name)
1069             val other_node = version.nodes(other_node_name)
1077           else version.nodes.commands_loading(other_node_name).headOption
1080           state.markup_to_XML(version, node_name, range, elements)
1088             (_, tree) <- state.command_results(version, command).iterator
1092           state.node_exports(version, node_name).iterator.map(_._2).toList
1105               val node = version.nodes(command.node_name)
1142             states = state.command_states(version, command)
1182           state.command_results(version, command)
1188           state.command_id_map(version, version.nodes(node_name).commands)
1194           "Snapshot(node = " + node_name.node + ", version = " + version.id +