tuned, following hints by IntelliJ IDEA;
authorwenzelm
Fri, 12 Aug 2022 14:33:50 +0200
changeset 75819 9f7abd148545
parent 75818 e71fbea76bd9
child 75820 d06cae2b407a
tuned, following hints by IntelliJ IDEA;
src/Pure/PIDE/document.scala
--- 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 = {