Pure/PIDE/document.scala

420         val version = future.join
421         versions.get(version.id) match {
422           case Some(version1) if !(version eq version1) => Future.value(version1)
454     def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
455       new Change(Some(previous), edits.reverse, version)
461     val version: Future[Version] = Future.value(Version.init))
465       version.is_finished
467     def truncate: Change = new Change(None, Nil, version)
472       val version1 = Version.purge_future(versions, version)
473       if ((previous eq previous1) && (version eq version1)) None
524     def version: Version
663     /*command-exec assignment for each version*/
684     def define_version(version: Version, assignment: State.Assignment): State =
686       val id = version.id
687       copy(versions = versions + (id -> version),
705     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
761       val version = the_version(id)
782       val new_assignment = the_assignment(version).assign(update)
788     def is_assigned(version: Version): Boolean =
789       assignments.get(version.id) match {
795       change.is_finished && is_assigned(change.version.get_finished)
800       if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None
805       version: Future[Version]): State =
807       val change = Change.make(previous, edits, version)
815           val old_versions = dropped.map(change => change.version.get_finished)
833         (version_id, version) <- versions1.iterator
835         (_, node) <- version.nodes.iterator
863     def command_state_eval(version: Version, command: Command): Option[Command.State] =
865       require(is_assigned(version))
867         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
875     private def command_states_self(version: Version, command: Command)
878       require(is_assigned(version))
880         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
893     def command_states(version: Version, command: Command): List[Command.State] =
895       val self = command_states_self(version, command)
900             (id, st) <- command_states_self(version, the_static_state(command_id).command)
908     def command_results(version: Version, command: Command): Command.Results =
909       Command.State.merge_results(command_states(version, command))
911     def command_markup(version: Version, command: Command, index: Command.Markup_Index,
913       Command.State.merge_markup(command_states(version, command), index, range, elements)
916       version: Version,
921       val node = version.nodes(node_name)
927           markup = command_markup(version, command, markup_index, command_range, elements)
937               version.nodes.commands_loading(node_name).headOption match {
942                   command_markup(version, command, markup_index, node_range, elements)
949     def node_initialized(version: Version, name: Node.Name): Boolean =
951       (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
953         case Some(command) => command_states(version, command).headOption.exists(_.initialized)
956     def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
959         version.nodes(name).commands.reverse.iterator.forall(command =>
960           command_state_eval(version, command) match {
966     def node_consolidated(version: Version, name: Node.Name): Boolean =
969         val it = version.nodes(name).commands.reverse.iterator
970         it.hasNext && command_states(version, it.next).exists(_.consolidated)
1002         val version: Version = stable.version.get_finished
1015         val node: Node = version.nodes(name)
1019           else version.nodes.commands_loading(node_name)
1031             val other_node = version.nodes(other_node_name)
1039           else version.nodes.commands_loading(other_node_name).headOption
1042           state.markup_to_XML(version, node_name, range, elements)
1050             (_, tree) <- state.command_results(version, command).iterator
1057               st <- state.command_states(version, command).iterator
1071               val node = version.nodes(command.node_name)
1108             states = state.command_states(version, command)
1148           state.command_results(version, command)
1154           "Snapshot(node = " + node_name.node + ", version = " + version.id +