| java.lang.Object
 de.uka.ilkd.key.parser.Location
| Location | | final public class Location (Code) | | This class represents a location in a file. It consists of a
filename, a line number and a column number. The filename may be
null, if the file is unknown (e.g. standard input). The class is
mainly used for parser exceptions.
author:
Hubert Schmid |
| Constructor Summary | |
| public | Location(String filename, int line, int column)
Parameters:
filename - the filename may be null. |
| Location | | public Location(String filename, int line, int column)(Code) | |
Parameters:
filename - the filename may be null. |
| getColumn | | public int getColumn()(Code) | | |
| getFilename | | public String getFilename()(Code) | | the filename may be null |
| getLine | | public int getLine()(Code) | | |
| toString | | public String toString()(Code) | | Internal string representation. Do not rely on format!
|
|
|