def ms_to_time(x):
    """Converts and integer number of miliseconds to a time string."""
    secs = x / 1000.0
    s = secs % 60
    m = int(secs / 60) % 60
    h = int(secs / 3600)
    rtn = []
    if h > 0: 
        rtn.append("{0:02}".format(h))
    if m > 0: 
        rtn.append("{0:02}".format(m))
    rtn.append("{0:06.3f}".format(s))
    return ":".join(rtn)