# HG changeset patch
# User wenzelm
# Date 1660307630 -7200
# Node ID 9f7abd148545df48746afe245f6699fabeafaa37
# Parent  e71fbea76bd96526847bb124a11a5b5181e56f2b
tuned, following hints by IntelliJ IDEA;

diff -r e71fbea76bd9 -r 9f7abd148545 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 = {