public class KeYResourceManager
extends java.lang.Object
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
|
boolean |
visibleBranch() |
public static KeYResourceManager getManager()
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
Copyright © 2003-2019 The KeY-Project.