public final class Source
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
NL |
Modifier and Type | Method and Description |
---|---|
void |
clearPositions()
Clear positions for this source.
|
static Source |
create(java.io.File file,
ErrorStream error)
Construct a source file.
|
java.io.File |
getFile()
Get the file denoting the source.
|
int |
getLength(int line,
int column)
Get number of characters from current position to end of line.
|
java.lang.String |
getLine(int i)
Get a line from the source.
|
int |
getLines()
Get number of lines of source.
|
int |
getOffset(int line,
int column)
Get offset of denoted position
|
SourcePosition[] |
getPositions()
Get positions for this source.
|
int |
getSize()
Get size of source.
|
java.lang.String |
getText()
Get the text of the source.
|
static boolean |
isClassSource(java.io.File file)
Determine whether file is a source file for a class.
|
boolean |
isModified()
Return true if text has been modified and should be retrieved.
|
static boolean |
isSource(java.io.File file)
Determine whether file is a source file.
|
static boolean |
isTheorySource(java.io.File file)
Determine whether file is a source file for a class.
|
SourcePosition |
newPosition(int line,
int column)
Construct position in this source.
|
void |
register(SourcePosition pos)
Register position for this source.
|
public static Source create(java.io.File file, ErrorStream error)
file
- the file denoting the source.error
- the stream for printing error messages.public static boolean isSource(java.io.File file)
file
- the file.public static boolean isClassSource(java.io.File file)
file
- the file.public static boolean isTheorySource(java.io.File file)
file
- the file.public java.io.File getFile()
public boolean isModified()
public java.lang.String getText()
public int getSize()
public int getLines()
public java.lang.String getLine(int i)
i
- the index of a line in the source.public SourcePosition newPosition(int line, int column)
line
- the line number.column
- the column number.public void register(SourcePosition pos)
pos
- a position for this source.public SourcePosition[] getPositions()
public void clearPositions()
public int getOffset(int line, int column)
line
- line indexcolumn
- column indexpublic int getLength(int line, int column)
line
- line indexcolumn
- column index