# HG changeset patch
# User wenzelm
# Date 1527362631 -7200
# Node ID 2bc4e5d9cca6ee62a6d192671dc47787c8a2fafb
# Parent  7ca0c23179e6b3486717476b2828dd71d7dced73
tuned;

diff -r 7ca0c23179e6 -r 2bc4e5d9cca6 src/Pure/PIDE/session.scala
--- 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