From 07d48df314b06c9a82fe8f5b61332b2497896fd7 Mon Sep 17 00:00:00 2001 From: Dave Halter Date: Sat, 1 Dec 2018 11:45:09 +0100 Subject: [PATCH] Make it possible to have higher precision with pstats displayed --- scripts/profile_output.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/scripts/profile_output.py b/scripts/profile_output.py index 135c8566..ff317dea 100755 --- a/scripts/profile_output.py +++ b/scripts/profile_output.py @@ -18,11 +18,26 @@ Options: import time import profile +import pstats from docopt import docopt import jedi +# Monkeypatch the time formatting function of profiling to make it easier to +# understand small time differences. +def f8(x): + ret = "%7.3f " % x + if ret == ' 0.000 ': + return "%6dµs" % (x * 10000000) + if ret.startswith(' 0.00'): + return "%8.4f" % x + return ret + + +pstats.f8 = f8 + + def run(code, index, infer=False): start = time.time() script = jedi.Script(code)