public class KeYResourceManager
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private java.lang.String |
branch |
private static java.lang.String |
DEFAULT_VERSION |
private static KeYResourceManager |
instance
the unique instance
|
private static java.util.Set<java.lang.String> |
INVISIBLE_BRANCHES |
private java.lang.String |
sha1 |
private java.lang.String |
version |
Modifier | Constructor and Description |
---|---|
private |
KeYResourceManager() |
Modifier and Type | Method and Description |
---|---|
boolean |
copy(java.lang.Class<?> cl,
java.lang.String resourcename,
java.lang.String targetLocation,
boolean overwrite) |
boolean |
copyIfNotExists(java.lang.Class<?> cl,
java.lang.String resourcename,
java.lang.String targetLocation) |
boolean |
copyIfNotExists(java.lang.Object o,
java.lang.String resourcename,
java.lang.String targetLocation)
Copies the specified resource to targetLocation if such a file
does not exist yet.
|
java.lang.String |
getBranch()
returns the git branch from which this version has been derived
|
static KeYResourceManager |
getManager()
Return an instance of the ResourceManager
|
java.net.URL |
getResourceFile(java.lang.Class<?> cl,
java.lang.String resourcename)
loads a resource and returns its URL
|
java.net.URL |
getResourceFile(java.lang.Object o,
java.lang.String resourcename)
loads a resource and returns its URL
|
java.lang.String |
getSHA1()
returns the SHA 1 git code from which this version has been derived
|
java.lang.String |
getUserInterfaceTitle()
All KeY
UserInterfaceControl s should use a common
title string when they require one, for instance for a GUI window title
bar. |
java.lang.String |
getVersion()
returns a readable customizable version number
|
private java.lang.String |
readVersionString(java.net.URL url)
reads a version string or returns "x.z.y" in case of failures
|
boolean |
visibleBranch() |
private static final java.lang.String DEFAULT_VERSION
private static final java.util.Set<java.lang.String> INVISIBLE_BRANCHES
private static final KeYResourceManager instance
private java.lang.String version
private java.lang.String sha1
private java.lang.String branch
public static KeYResourceManager getManager()
private java.lang.String readVersionString(java.net.URL url)
public java.lang.String getSHA1()
public java.lang.String getBranch()
public boolean visibleBranch()
public java.lang.String getVersion()
public boolean copyIfNotExists(java.lang.Object o, java.lang.String resourcename, java.lang.String targetLocation)
o
- an Object the directory from where resourcename
is copied is determined by looking on the package where o.getClass()
is declaredresourcename
- String the name of the file to search (only relative
pathname to the path of the calling class)targetLocation
- target for copyingpublic boolean copyIfNotExists(java.lang.Class<?> cl, java.lang.String resourcename, java.lang.String targetLocation)
public boolean copy(java.lang.Class<?> cl, java.lang.String resourcename, java.lang.String targetLocation, boolean overwrite)
public java.net.URL getResourceFile(java.lang.Class<?> cl, java.lang.String resourcename)
cl
- the Class used to determine the resourceresourcename
- the String that contains the name of the resourcepublic java.net.URL getResourceFile(java.lang.Object o, java.lang.String resourcename)
o
- the Object used to determine the resourceresourcename
- the String that contains the name of the resourcepublic java.lang.String getUserInterfaceTitle()
UserInterfaceControl
s should use a common
title string when they require one, for instance for a GUI window title
bar.UserInterfaces