src/Pure/General/time.ML

tuned comments;

(*  Title:      Pure/General/time.scala
    Author:     Makarius

Time based on nanoseconds (idealized), printed as milliseconds.
*)

signature TIME =
sig
  include TIME
  val min: time * time -> time
  val max: time * time -> time
  val scale: real -> time -> time
  val parse: string -> time
  val print: time -> string
  val message: time -> string
end;

structure Time: TIME =
struct

open Time;

fun min (t1, t2) = if t1 < t2 then t1 else t2;
fun max (t1, t2) = if t1 > t2 then t1 else t2;

fun scale s t = Time.fromNanoseconds (Real.ceil (s * Real.fromInt (Time.toNanoseconds t)));

fun parse s =
  (case Time.fromString s of
    SOME t => t
  | NONE => raise Fail ("Bad time " ^ quote s));

fun print t =
  if t < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - t)
  else Time.toString t;

fun message t = print t ^ "s";

end;