public class ParseExceptionInFile extends ParseException implements HasLocation
ParseException
by a filename.
The filename is used to display the location of an error in the sources. Line and column number are not stored here explicitly but retrieved from the cause.
currentToken, eol, expectedTokenSequences, specialConstructor, tokenImage
Constructor and Description |
---|
ParseExceptionInFile(java.lang.String filename,
java.lang.String message,
java.lang.Throwable cause) |
ParseExceptionInFile(java.lang.String filename,
java.lang.Throwable cause) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getFilename() |
Location |
getLocation()
This method can be used to obtain the Location (1-based line and column!) of the exception.
|
add_escapes, getMessage
public ParseExceptionInFile(java.lang.String filename, java.lang.String message, java.lang.Throwable cause)
public ParseExceptionInFile(java.lang.String filename, java.lang.Throwable cause)
public java.lang.String getFilename()
@Nullable public Location getLocation() throws java.net.MalformedURLException
HasLocation
getLocation
in interface HasLocation
java.net.MalformedURLException
- if the URL for the location can not be createdCopyright © 2003-2019 The KeY-Project.