public class PosConvertException extends ConvertException implements HasLocation
The source's name itself is not captured.
Constructor and Description |
---|
PosConvertException(java.lang.String message,
int line,
int column)
Instantiates a new exception with position information.
|
PosConvertException(java.lang.Throwable cause,
int line,
int column)
Instantiates a new exception with position information.
|
Modifier and Type | Method and Description |
---|---|
int |
getColumn()
Gets the column of the exception location.
|
int |
getLine()
Gets the line of the exception location.
|
Location |
getLocation()
This method can be used to obtain the Location (1-based line and column!) of the exception.
|
parseException, proofJavaException
public PosConvertException(java.lang.String message, int line, int column)
message
- the message, not nullline
- the line to point tocolumn
- the column to point topublic PosConvertException(java.lang.Throwable cause, int line, int column)
cause
- the exception causing this instance.line
- the line to point tocolumn
- the column to point topublic int getLine()
public int getColumn()
@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.