private static String getLocation(String sf_, Token token_) {
            if (token_ != null)
                  return sf_ + ":" + token_.beginLine + ":" + token_.beginColumn;
                return sf_;
        }