diff -r 87ebf5a50283 -r 42267c650205 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Apr 01 23:19:12 2022 +0200
@@ -679,7 +679,7 @@
     def command_results(range: Text.Range): Command.Results =
       Command.State.merge_results(
         select[List[Command.State]](range, Markup.Elements.full,
-          command_states => { case _ => Some(command_states) }).flatMap(_.info))
+          command_states => _ => Some(command_states)).flatMap(_.info))
 
     def command_results(command: Command): Command.Results =
       state.command_results(version, command)