public class MemoryFileRepo extends AbstractFileRepo
CLASS_MATCHER, JAVA_MATCHER, KEY_MATCHER, REDUX_URL, RULES_URL, ZIP_MATCHER
Constructor and Description |
---|
MemoryFileRepo() |
Modifier and Type | Method and Description |
---|---|
java.io.OutputStream |
createOutputStream(java.nio.file.Path path)
This method can be used to write a file that has no counterpart outside to the FileRepo.
|
java.io.InputStream |
getInputStream(java.nio.file.Path path)
Provides access to a file on disk.
|
java.io.InputStream |
getInputStream(RuleSource ruleSource)
Provides access to the InputStream of a RuleSource.
|
java.io.InputStream |
getInputStream(java.net.URL url)
Provides access to the InputStream of a file identified by an URL.
|
java.io.InputStream |
getInputStreamInternal(java.nio.file.Path p)
Can be used to get a direct InputStream to a file stored in the FileRepo.
|
java.nio.file.Path |
getSaveName(java.nio.file.Path path)
Return the save name for a given file.
|
adaptFileRefs, addFile, createDirsAndCopy, dispose, getBaseDir, getBootclasspath, getClasspath, getJavaPath, getRegisteredProofs, isDisposed, isInBootClassPath, isInJavaPath, isInternalFile, isInternalResource, proofDisposed, proofDisposing, registerProof, saveProof, setBaseDir, setBootClassPath, setClassPath, setJavaPath
public java.io.InputStream getInputStream(java.nio.file.Path path) throws java.io.FileNotFoundException, java.io.IOException
FileRepo
null
if the path cannot be handled by this repository.getInputStream
in interface FileRepo
getInputStream
in class AbstractFileRepo
path
- the path of the filenull
java.io.FileNotFoundException
- if the file does not existjava.io.IOException
- on IO errors, e.g. if the user has no permission to read the filepublic java.io.InputStream getInputStream(RuleSource ruleSource) throws java.io.IOException
FileRepo
null
if the source cannot be handled by this repository.getInputStream
in interface FileRepo
getInputStream
in class AbstractFileRepo
ruleSource
- the RuleSourcenull
java.io.IOException
- on IO errorspublic java.io.InputStream getInputStream(java.net.URL url) throws java.io.IOException
FileRepo
null
if the url cannot be handled by this repository.url
- the URL of the filenull
java.io.IOException
- on IO errorspublic java.io.OutputStream createOutputStream(java.nio.file.Path path)
FileRepo
path
- the path of the file to store. The path must be relative to the base directory
of the proof package.public java.io.InputStream getInputStreamInternal(java.nio.file.Path p)
AbstractFileRepo
getInputStreamInternal
in class AbstractFileRepo
p
- the original path (outside the FileRepo) of the requested filepublic java.nio.file.Path getSaveName(java.nio.file.Path path)
AbstractFileRepo
getSaveName
in class AbstractFileRepo
path
- the given file (absolute or relative to the proof base directory)Copyright © 2003-2019 The KeY-Project.