public final class Main extends Object
Modifier and Type | Class and Description |
---|---|
private static class |
Main.UiMode
The user interface modes KeY can operate in.
|
Modifier and Type | Field and Description |
---|---|
private static String |
AUTO |
private static String |
AUTO_LOADONLY |
private static ProofMacro |
autoMacro |
private static String |
AUTOSAVE |
private static CommandLine |
cl
Object handling the parsing of commandline options
|
private static String |
DEBUG |
private static String |
EXAMPLES |
private static String |
examplesDir |
private static String |
EXPERIMENTAL |
private static boolean |
experimentalMode
Lists all features currently marked as experimental.
|
private static List<File> |
fileArguments
The file names provided on the command line
|
private static String |
HELP
Command line options
|
static String |
JFILE_FOR_AXIOMS |
static String |
JFILE_FOR_DEFINITION |
static String |
JKEY_PREFIX |
static String |
JMAX_RULES |
static String |
JPATH_OF_RESULT |
static String |
JPRINT |
static String |
JSAVE_RESULTS_TO_FILE |
static String |
JTIMEOUT |
static String |
JUSTIFY_RULES |
private static KeYDesktop |
keyDesktop
The
KeYDesktop used by KeY. |
private static String |
LAST |
private static boolean |
loadOnly
Determines whether to actually prove or only load a problem when
uiMode is Main.UiMode.AUTO . |
private static boolean |
loadRecentFile
flag whether recent loaded file should be loaded on startup
|
private static String |
MACRO |
private static String |
NO_JMLSPECS |
private static String |
RIFL |
private static String |
riflFileName
Path to a RIFL specification file.
|
private static String |
SAVE_ALL_CONTRACTS |
private static boolean |
saveAllContracts
Save all contracts in selected location to automate the creation
of multiple ".key"-files
|
private static String |
SHOW_PROPERTIES |
static boolean |
showExampleChooserIfExamplesDirIsDefined
This flag indicates if the example chooser should be shown
if
examplesDir is defined (not null ). |
private static String |
TACLET_DIR |
private static String |
TIMEOUT |
private static Main.UiMode |
uiMode
Determines which
UserInterfaceControl is to be used. |
private static byte |
verbosity
Level of verbosity for command line outputs.
|
private static String |
VERBOSITY |
Constructor and Description |
---|
Main() |
Modifier and Type | Method and Description |
---|---|
private static CommandLine |
createCommandLine()
Register commandline options with command line object
|
private static AbstractMediatorUserInterfaceControl |
createUserInterface(List<File> fileArguments)
Initializes the
UserInterfaceControl to be used by KeY. |
static void |
ensureExamplesAvailable() |
private static void |
evaluateLemmataOptions(CommandLine options) |
static void |
evaluateOptions(CommandLine cl)
Evaluate the parsed commandline options
|
static String |
getExamplesDir() |
static KeYDesktop |
getKeyDesktop()
Returns the
KeYDesktop to use. |
static File |
getWorkingDir()
Used by
KeYFileChooser (and potentially
others) to determine working directory. |
static boolean |
isExperimentalMode() |
static void |
loadCommandLineFiles(AbstractMediatorUserInterfaceControl ui,
List<File> fileArguments) |
static void |
main(String[] args) |
private static List<File> |
preProcessInput(List<File> filesOnStartup)
Perform necessary actions before loading any problem files.
|
private static void |
printHeader()
Print a header text on to the console.
|
static void |
printUsageAndExit(boolean printUsage,
String offending,
int exitValue) |
static void |
setEnabledExperimentalFeatures(boolean state)
Deactivate experimental features.
|
static void |
setExamplesDir(String newExamplesDir)
Defines the examples directory.
|
static void |
setKeyDesktop(KeYDesktop keyDesktop)
Sets the
KeYDesktop to use. |
private static void |
updateSplashScreen() |
private static final String HELP
private static final String SHOW_PROPERTIES
private static final String AUTO
private static final String LAST
private static final String AUTO_LOADONLY
private static final String AUTOSAVE
private static final String EXPERIMENTAL
private static final String DEBUG
private static final String MACRO
private static final String NO_JMLSPECS
private static final String TACLET_DIR
public static final String JUSTIFY_RULES
private static final String SAVE_ALL_CONTRACTS
private static final String TIMEOUT
private static final String EXAMPLES
private static final String RIFL
public static final String JKEY_PREFIX
public static final String JMAX_RULES
public static final String JPATH_OF_RESULT
public static final String JTIMEOUT
public static final String JPRINT
public static final String JSAVE_RESULTS_TO_FILE
public static final String JFILE_FOR_AXIOMS
public static final String JFILE_FOR_DEFINITION
private static final String VERBOSITY
private static KeYDesktop keyDesktop
KeYDesktop
used by KeY. The default implementation is
replaced in Eclipse. For this reason the Desktop
should never
be used directly.private static byte verbosity
private static String examplesDir
private static Main.UiMode uiMode
UserInterfaceControl
is to be used.
By specifying AUTO
as command line argument this will be set
to Main.UiMode.AUTO
, but Main.UiMode.INTERACTIVE
is the default.private static boolean loadOnly
uiMode
is Main.UiMode.AUTO
.
This can be controlled from the command line by specifying the argument
AUTO_LOADONLY
instead of AUTO
.private static CommandLine cl
private static boolean loadRecentFile
private static boolean experimentalMode
private static String riflFileName
private static boolean saveAllContracts
private static ProofMacro autoMacro
public static boolean showExampleChooserIfExamplesDirIsDefined
This flag indicates if the example chooser should be shown
if examplesDir
is defined (not null
). It is set
in the Eclipse integration to false
, because it is required
to define the path to a different one without showing the chooser.
Conclusion: It must be possible to use KeY with a custom examples directory without show in the chooser on startup.
public static void main(String[] args)
public static void loadCommandLineFiles(AbstractMediatorUserInterfaceControl ui, List<File> fileArguments)
private static CommandLine createCommandLine()
public static void evaluateOptions(CommandLine cl)
commandline
- object clpublic static void setEnabledExperimentalFeatures(boolean state)
public static boolean isExperimentalMode()
private static void printHeader()
private static AbstractMediatorUserInterfaceControl createUserInterface(List<File> fileArguments)
UserInterfaceControl
to be used by KeY.
ConsoleUserInterfaceControl
will be used if uiMode
is
Main.UiMode.AUTO
and WindowUserInterfaceControl
otherwise.UserInterfaceControl
based on the value of
uiMode
public static void ensureExamplesAvailable()
private static void updateSplashScreen()
private static void evaluateLemmataOptions(CommandLine options)
public static void printUsageAndExit(boolean printUsage, String offending, int exitValue)
public static File getWorkingDir()
KeYFileChooser
(and potentially
others) to determine working directory. In case there is at least one
location (i.e. a file or directory) specified as command line argument,
working directory is determined based on first location that occurred in
the list of arguments. Otherwise, value of System.getProperty("user.home")
is used to determine working directory.File
object representing working directory.private static List<File> preProcessInput(List<File> filesOnStartup)
public static String getExamplesDir()
public static void setExamplesDir(String newExamplesDir)
newExamplesDir
- The new examples directory to use.public static KeYDesktop getKeyDesktop()
KeYDesktop
to use. Never use Desktop
directly because the KeYDesktop
is different in Eclipse.KeYDesktop
to use.public static void setKeyDesktop(KeYDesktop keyDesktop)
KeYDesktop
to use.keyDesktop
- The new KeYDesktop
to use.