--- a/src/Pure/PIDE/document.scala Fri Aug 12 14:26:17 2022 +0200
+++ b/src/Pure/PIDE/document.scala Fri Aug 12 14:33:50 2022 +0200
@@ -338,7 +338,7 @@
def source: String =
get_blob match {
case Some(blob) => blob.source
- case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
+ case None => command_iterator().map({ case (cmd, _) => cmd.source }).mkString
}
}
@@ -1099,7 +1099,7 @@
(for {
command <- commands.iterator
id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator
- } yield (id -> command)).toMap
+ } yield id -> command).toMap
}
def command_maybe_consolidated(version: Version, command: Command): Boolean = {