--- a/src/Pure/PIDE/session.scala Sat May 26 19:40:02 2018 +0200
+++ b/src/Pure/PIDE/session.scala Sat May 26 21:23:51 2018 +0200
@@ -386,9 +386,8 @@
prover.get.define_command(command)
}
}
- change.doc_edits foreach {
- case (_, edit) =>
- edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
+ for { (_, edit) <- change.doc_edits } {
+ edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) })
}
val assignment = global_state.value.the_assignment(change.previous).check_finished