public final class Main
extends java.lang.Object
This has been extracted from MainWindow to keep GUI and control further apart.
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 java.lang.String |
AUTO |
private static java.lang.String |
AUTO_LOADONLY |
private static ProofMacro |
autoMacro |
private static java.lang.String |
AUTOSAVE |
private static CommandLine |
cl
Object handling the parsing of commandline options
|
private static java.lang.String |
DEBUG |
private static java.lang.String |
EXAMPLES |
private static java.lang.String |
examplesDir |
private static java.lang.String |
EXPERIMENTAL |
private static boolean |
experimentalMode
Lists all features currently marked as experimental.
|
private static java.util.List<java.io.File> |
fileArguments
The file names provided on the command line
|
private static java.lang.String |
HELP
Command line options
|
static java.lang.String |
JFILE_FOR_AXIOMS |
static java.lang.String |
JFILE_FOR_DEFINITION |
static java.lang.String |
JKEY_PREFIX |
static java.lang.String |
JMAX_RULES |
static java.lang.String |
JPATH_OF_RESULT |
static java.lang.String |
JPRINT |
static java.lang.String |
JSAVE_RESULTS_TO_FILE |
static java.lang.String |
JTIMEOUT |
static java.lang.String |
JUSTIFY_RULES |
private static KeYDesktop |
keyDesktop
The
KeYDesktop used by KeY. |
private static java.lang.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 java.lang.String |
MACRO |
private static java.lang.String |
NO_JMLSPECS |
private static java.lang.String |
NO_PRUNING_CLOSED
This parameter disables the possibility to prune in closed branches.
|
private static java.lang.String |
RIFL |
private static java.io.File |
riflFileName
Path to a RIFL specification file.
|
private static java.lang.String |
SAVE_ALL_CONTRACTS |
private static boolean |
saveAllContracts
Save all contracts in selected location to automate the creation
of multiple ".key"-files
|
private static java.lang.String |
SHOW_PROPERTIES |
static boolean |
showExampleChooserIfExamplesDirIsDefined
This flag indicates if the example chooser should be shown
if
examplesDir is defined (not null ). |
private static java.lang.String |
TACLET_DIR |
private static java.lang.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 java.lang.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(java.util.List<java.io.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 java.lang.String |
getExamplesDir() |
static KeYDesktop |
getKeyDesktop()
Returns the
KeYDesktop to use. |
static java.io.File |
getWorkingDir()
Used by
KeYFileChooser (and potentially
others) to determine working directory. |
static boolean |
isExperimentalMode() |
static void |
loadCommandLineFiles(AbstractMediatorUserInterfaceControl ui,
java.util.List<java.io.File> fileArguments) |
static void |
main(java.lang.String[] args) |
private static java.util.List<java.io.File> |
preProcessInput(java.util.List<java.io.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,
java.lang.String offending,
int exitValue) |
static void |
setEnabledExperimentalFeatures(boolean state)
Deactivate experimental features.
|
static void |
setExamplesDir(java.lang.String newExamplesDir)
Defines the examples directory.
|
static void |
setKeyDesktop(KeYDesktop keyDesktop)
Sets the
KeYDesktop to use. |
private static void |
updateSplashScreen() |
private static final java.lang.String HELP
private static final java.lang.String SHOW_PROPERTIES
private static final java.lang.String AUTO
private static final java.lang.String LAST
private static final java.lang.String AUTO_LOADONLY
private static final java.lang.String AUTOSAVE
private static final java.lang.String EXPERIMENTAL
private static final java.lang.String NO_PRUNING_CLOSED
private static final java.lang.String DEBUG
private static final java.lang.String MACRO
private static final java.lang.String NO_JMLSPECS
private static final java.lang.String TACLET_DIR
public static final java.lang.String JUSTIFY_RULES
private static final java.lang.String SAVE_ALL_CONTRACTS
private static final java.lang.String TIMEOUT
private static final java.lang.String EXAMPLES
private static final java.lang.String RIFL
public static final java.lang.String JKEY_PREFIX
public static final java.lang.String JMAX_RULES
public static final java.lang.String JPATH_OF_RESULT
public static final java.lang.String JTIMEOUT
public static final java.lang.String JPRINT
public static final java.lang.String JSAVE_RESULTS_TO_FILE
public static final java.lang.String JFILE_FOR_AXIOMS
public static final java.lang.String JFILE_FOR_DEFINITION
private static final java.lang.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 java.lang.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 java.util.List<java.io.File> fileArguments
private static boolean experimentalMode
private static java.io.File 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(java.lang.String[] args)
public static void loadCommandLineFiles(AbstractMediatorUserInterfaceControl ui, java.util.List<java.io.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(java.util.List<java.io.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, java.lang.String offending, int exitValue)
public static java.io.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 java.util.List<java.io.File> preProcessInput(java.util.List<java.io.File> filesOnStartup)
public static java.lang.String getExamplesDir()
public static void setExamplesDir(java.lang.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.