src/Pure/PIDE/document.scala
changeset 70284 3e17c3a5fd39
parent 69633 3d91a7a58113
child 70539 30b3c58a1933
     1.1 --- a/src/Pure/PIDE/document.scala	Sun May 19 14:14:56 2019 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun May 19 18:10:45 2019 +0200
     1.3 @@ -651,7 +651,7 @@
     1.4      }
     1.5  
     1.6      val init: State =
     1.7 -      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
     1.8 +      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2
     1.9    }
    1.10  
    1.11    final case class State private(
    1.12 @@ -768,10 +768,15 @@
    1.13            st <- command_states(version, command).iterator
    1.14          } yield st.exports)
    1.15  
    1.16 -    def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
    1.17 +    def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
    1.18 +      : ((List[Node.Name], List[Command]), State) =
    1.19      {
    1.20        val version = the_version(id)
    1.21  
    1.22 +      val edited_set = edited.toSet
    1.23 +      val edited_nodes =
    1.24 +        (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
    1.25 +
    1.26        def upd(exec_id: Document_ID.Exec, st: Command.State)
    1.27            : Option[(Document_ID.Exec, Command.State)] =
    1.28          if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
    1.29 @@ -794,7 +799,7 @@
    1.30        val new_assignment = the_assignment(version).assign(update)
    1.31        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    1.32  
    1.33 -      (changed_commands, new_state)
    1.34 +      ((edited_nodes, changed_commands), new_state)
    1.35      }
    1.36  
    1.37      def is_assigned(version: Version): Boolean =