tuned signature;
authorwenzelm
Wed, 01 Mar 2023 21:04:28 +0100
changeset 77462 b474d39ddfee
parent 77461 a553e419e9dc
child 77463 4e8bec105ce5
tuned signature;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 20:59:37 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 21:04:28 2023 +0100
@@ -103,18 +103,18 @@
   ) {
     def sessions_structure: Sessions.Structure = build_deps.sessions_structure
 
-    def sources_shasum(session: String): SHA1.Shasum = sessions(session).sources_shasum
+    def sources_shasum(name: String): SHA1.Shasum = sessions(name).sources_shasum
 
-    def old_command_timings(session: String): List[Properties.T] =
-      sessions.get(session) match {
+    def old_command_timings(name: String): List[Properties.T] =
+      sessions.get(name) match {
         case Some(session_context) =>
           Properties.uncompress(session_context.old_command_timings_blob, cache = store.cache)
         case None => Nil
       }
 
-    def do_store(session: String): Boolean =
-      build_heap || Sessions.is_pure(session) ||
-      sessions.valuesIterator.exists(_.ancestors.contains(session))
+    def do_store(name: String): Boolean =
+      build_heap || Sessions.is_pure(name) ||
+      sessions.valuesIterator.exists(_.ancestors.contains(name))
   }