str.isdigit is about 4x faster than using a regular expression ("\d+").
This is in the inner sorting code so speed matters.

$ python -m timeit -s 'import re; s = re.compile("^\d+$")' \
's.match(""); s.match("Hello World"); s.match("1234")'
1000000 loops, best of 3: 0.937 usec per loop

$ python -m timeit '"".isdigit(); "Hello World".isdigit(); "1234".isdigit()'
1000000 loops, best of 3: 0.218 usec per loop

Signed-off-by: Michael Hanselmann <hansmi@google.com>
Reviewed-by: Iustin Pop <iustin@google.com>