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