public static final class OriginTermLabel.FileOrigin extends OriginTermLabel.Origin
Modifier and Type | Field and Description |
---|---|
java.net.URI |
fileName
The file the term originates from.
|
int |
line
The line in the file the term originates from.
|
specType
Constructor and Description |
---|
FileOrigin(OriginTermLabel.SpecType specType,
java.lang.String fileName,
int line)
Creates a new
OriginTermLabel.Origin . |
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object obj) |
int |
hashCode() |
java.lang.String |
toString() |
compareTo
public final java.net.URI fileName
public final int line
public FileOrigin(OriginTermLabel.SpecType specType, java.lang.String fileName, int line)
OriginTermLabel.Origin
.specType
- the spec type the term originates from.fileName
- the file the term originates from.line
- the line in the file.public java.lang.String toString()
toString
in class OriginTermLabel.Origin
public int hashCode()
hashCode
in class OriginTermLabel.Origin
public boolean equals(java.lang.Object obj)
equals
in class OriginTermLabel.Origin
Copyright © 2003-2019 The KeY-Project.