Toolbox & SANY could improve parse error message when proof step level exceeds 2^31

[ahelwer]

This is clearly a dubious case to handle but I will document it in the interest of completeness (maybe a good project for a first-time contributor?). The upper limit of a proof level accepted by SANY is 2^31-1 (2147483647), which is of course the largest positive number representable by a 32 bit signed integer. Consider the following TLA+ module where the proof step exceeds that number; I don't know why someone would do this, but I guess maybe they deserve a good error message:

---- MODULE Test ----
THEOREM TRUE
<2147483648> QED
====

The error message from running SANY on the command line is not perfect, but actually pretty good:

Fatal errors while parsing TLA+ spec in file .\Test.tla

java.lang.NumberFormatException: For input string: "2147483648"

However, in the toolbox there is only the following blank box: which could be improved.