src/Pure/General/timing.scala
changeset 71785 39613d6e2021
parent 67858 cba5c5657378
child 72015 6c6609fd898c
equal deleted inserted replaced
71784:8a5da740e388 71785:39613d6e2021
    58 
    58 
    59   def message_resources: String =
    59   def message_resources: String =
    60   {
    60   {
    61     val factor_text =
    61     val factor_text =
    62       factor match {
    62       factor match {
    63         case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f))
    63         case Some(f) => String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
    64         case None => ""
    64         case None => ""
    65       }
    65       }
    66     if (resources.seconds >= 3.0)
    66     if (resources.seconds >= 3.0)
    67       elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text
    67       elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text
    68     else
    68     else