equal
deleted
inserted
replaced
649 new Assignment(command_execs1, true) |
649 new Assignment(command_execs1, true) |
650 } |
650 } |
651 } |
651 } |
652 |
652 |
653 val init: State = |
653 val init: State = |
654 State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2 |
654 State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2 |
655 } |
655 } |
656 |
656 |
657 final case class State private( |
657 final case class State private( |
658 /*reachable versions*/ |
658 /*reachable versions*/ |
659 versions: Map[Document_ID.Version, Version] = Map.empty, |
659 versions: Map[Document_ID.Version, Version] = Map.empty, |
766 for { |
766 for { |
767 command <- version.nodes(node_name).commands.iterator |
767 command <- version.nodes(node_name).commands.iterator |
768 st <- command_states(version, command).iterator |
768 st <- command_states(version, command).iterator |
769 } yield st.exports) |
769 } yield st.exports) |
770 |
770 |
771 def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) = |
771 def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) |
|
772 : ((List[Node.Name], List[Command]), State) = |
772 { |
773 { |
773 val version = the_version(id) |
774 val version = the_version(id) |
|
775 |
|
776 val edited_set = edited.toSet |
|
777 val edited_nodes = |
|
778 (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList |
774 |
779 |
775 def upd(exec_id: Document_ID.Exec, st: Command.State) |
780 def upd(exec_id: Document_ID.Exec, st: Command.State) |
776 : Option[(Document_ID.Exec, Command.State)] = |
781 : Option[(Document_ID.Exec, Command.State)] = |
777 if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st) |
782 if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st) |
778 |
783 |
792 (commands2, execs2) |
797 (commands2, execs2) |
793 } |
798 } |
794 val new_assignment = the_assignment(version).assign(update) |
799 val new_assignment = the_assignment(version).assign(update) |
795 val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) |
800 val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) |
796 |
801 |
797 (changed_commands, new_state) |
802 ((edited_nodes, changed_commands), new_state) |
798 } |
803 } |
799 |
804 |
800 def is_assigned(version: Version): Boolean = |
805 def is_assigned(version: Version): Boolean = |
801 assignments.get(version.id) match { |
806 assignments.get(version.id) match { |
802 case Some(assgn) => assgn.is_finished |
807 case Some(assgn) => assgn.is_finished |