Hmm, it looks like a duration (seconds from start to end), not "date/time notation" as noted in the function description. Why is is called scorm_format_date_time()?
If that function does dates it would normally convert it to unix timestamp and use our string formatting, but I guess this is not the case. Sorry for the confusion.
Our standard way is to do format_time(), so I guess it could work if we just get then rounded number of seconds from the SCORM format and use standard API.
We could also add the milliseconds if really necessary to core API.
To David: there is some old caching in format_time() that should not be there because the string subsystem should be a lot faster now, I suppose we could use the second params for milliseconds now instead...