--- 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)