[quality][performance] Format performance numbers in the log

[kaiyue0329]

Issue: #6531

What it does

• formatted the performance numbers in the log to one decimal place.

Review checklist

• as an author, I have thoroughly tested my changes and carefully followed the review guidelines

Reminder for reviewers

• as a reviewer, I agree to behave in accordance with the review guidelines

[vince-fugnitto]

It fixes the issue 👍

I'm wondering, what do you think of having a utility method in @theia/core (the base extension), which would accept as arguments content and milliseconds which can be re-used when displaying metric results? This would mean that we would not need to re-implement the same code in different places with the same purpose.

Something like:

export function printMetric(content: string, milliseconds: number): void {
    console.log(`${content} took ${Math.round(milliseconds * 10) / 10} ms`);
}

[kittaakos]

would not need to re-implement the same code

We could use ms.