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