diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -32,7 +32,7 @@
             case a :: bs => (a, bs)
             case _ => throw new XML.XML_Body(body)
           }
-        Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
+        Some(triple(long, list(string), list(decode_upd))(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
@@ -310,7 +310,7 @@
   def define_commands_bulk(commands: List[Command])
   {
     val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
-    irregular.foreach(define_command(_))
+    irregular.foreach(define_command)
     regular match {
       case Nil =>
       case List(command) => define_command(command)