de.uka.ilkd.key.java

Class ParseExceptionInFile

java.lang.Object

java.lang.Throwable

java.lang.Exception

recoder.ParserException

recoder.parser.ParseException

de.uka.ilkd.key.java.ParseExceptionInFile

All Implemented Interfaces:

java.io.Serializable

public class ParseExceptionInFile
extends ParseException

This exception extends recoder's 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.

Author:

mulbrich

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	filename

Fields inherited from class recoder.parser.ParseException

currentToken, eol, expectedTokenSequences, specialConstructor, tokenImage

Constructor Summary

Constructors

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)

Method Summary

Modifier and Type	Method and Description
java.lang.String	getFilename()

Methods inherited from class recoder.parser.ParseException

add_escapes, getMessage

Methods inherited from class java.lang.Throwable

addSuppressed, fillInStackTrace, getCause, getLocalizedMessage, getStackTrace, getSuppressed, initCause, printStackTrace, printStackTrace, printStackTrace, setStackTrace, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

filename

private final java.lang.String filename

Constructor Detail

ParseExceptionInFile

public ParseExceptionInFile(java.lang.String filename,
                            java.lang.String message,
                            java.lang.Throwable cause)

ParseExceptionInFile

public ParseExceptionInFile(java.lang.String filename,
                            java.lang.Throwable cause)

Method Detail

getFilename

public java.lang.String getFilename()