public class KeYCrossReferenceSourceFileRepository extends DefaultSourceFileRepository
DefaultSourceFileRepository
creates references
to possibly non-existing files which we do not want. Thus, we leave the location
already present.JAVA_FILENAME_FILTER
serviceConfiguration
Constructor and Description |
---|
KeYCrossReferenceSourceFileRepository(ServiceConfiguration config) |
Modifier and Type | Method and Description |
---|---|
protected DataLocation |
createDataLocation(CompilationUnit cu)
return the data location that is already stored in the compilation unit.
|
addProgressListener, cleanUp, findSourceFile, getAllCompilationUnitsFromPath, getAllCompilationUnitsFromPath, getCompilationUnit, getCompilationUnitFromFile, getCompilationUnitFromLocation, getCompilationUnits, getCompilationUnitsFromFiles, getKnownCompilationUnits, getOutputPath, getSearchPathList, information, initialize, isUpToDate, modelChanged, print, printAll, propertyChange, removeProgressListener
getServiceConfiguration
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getServiceConfiguration
public KeYCrossReferenceSourceFileRepository(ServiceConfiguration config)
protected DataLocation createDataLocation(CompilationUnit cu)
createDataLocation
in class DefaultSourceFileRepository
cu
- Compilation unit to create the location for.SpecDataLocation.UNKNOWN_LOCATION
:
location(cu)