public class BatchMMJ2 extends BatchFramework
Please refer to mmj.util.CommandLineArguments.java
for details about
the command line arguments used.
batchFrameworkInitialized, bossList, commandLineArguments, currentRunParmCommand, displayMMJ2FailPopupWindow, gmffBoss, grammarBoss, logicalSystemBoss, macroBoss, mmj2FailPopupWindow, outputBoss, paths, proofAsstBoss, runParmCnt, runParmFile, storeBoss, svcBoss, theoremLoaderBoss, tmffBoss, verifyProofBoss, workVarBoss
Constructor and Description |
---|
BatchMMJ2()
Default Constructor.
|
Modifier and Type | Method and Description |
---|---|
static void |
checkVersion() |
int |
generateSvcCallback(java.lang.String[] args,
SvcCallback svcCallback)
Secondary entry point for BatchMMJ2 to trigger a callback to the
designated object.
|
static void |
main(java.lang.String[] args)
Main function interfacing to Java environment, running the BatchMMJ2
functions.
|
executeRunParmCommand, getRunParmFileAbsolutePath, initializeBatchFramework, printCommentRunParmLine, printExecutableRunParmLine, runIt
public static void main(java.lang.String[] args)
args
- see class description.public int generateSvcCallback(java.lang.String[] args, SvcCallback svcCallback)
To use this entry point insert the following code, or something like it, in your program:
BatchMMJ2 batchMMJ2 = new BatchMMJ2(); String[] myArgs = {"RunParms.txt"}; MyMMJSvcCallback mySvcCallback = new MyMMJSvcCallback(); batchMMJ2.generateSvcCallback(myArgs, mySvcCallback);See mmj2 for info about the content of the RunParms file, as well as the description for this class for information about other args.
The call to generateSvcCallback will run the BatchMMJ2 process in the normal way, and if there are no errors and a RunParm is encountered specifying execution of a SvcCallback, your SvcCallback's "go" method will be invoked.
From that point on your SvcCallback can utilize mmj2 objects as a "service" -- for example, you can unload the Metamath objects to s-expressions. Simply return from your SvcCallback.go() method to terminate.
NOTE: It is not necessary to use this entry point. A SvcCallback class can be specified via mmj2 RunParm. If that is done then a "callback" can be generated via RunParm command, which, in effect, would make your callback a subroutine of BatchMMJ2. You would just need to ensure that your class is in the Java Classpath in use when BatchMMJ2 is run.
NOTE: The SvcCallback parameter passed in here will be overridden by a RunParm SvcCallback -- but the "Clear" RunParm does not erase a SvcCallback parameter passed via setSvcCallback (contrary to the behavior of "Clear" elsewhere.)
args
- see class description.svcCallback
- your concrete instantiation of the mmj SvcCallback
interface.public static void checkVersion() throws java.lang.IllegalArgumentException
java.lang.IllegalArgumentException