javaTok_substring - possibly faster substring() for javaTok etc.