tuned signature: more operations;

--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 12:09:42 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 14:16:54 2023 +0100
@@ -51,6 +51,8 @@
     val elapsed: Time,
     val command_timings: List[Properties.T]
   ) {
+    def is_empty: Boolean = elapsed.is_zero && command_timings.isEmpty
+
     override def toString: String =
       session + (if (elapsed.is_relevant) " (" + elapsed.message_hms + " elapsed time)" else "")
   }