public interface SvcCallback
Modifier and Type | Method and Description |
---|---|
void |
go(Messages messages,
OutputBoss outputBoss,
LogicalSystem logicalSystem,
VerifyProofs verifyProofs,
Grammar grammar,
WorkVarManager workVarManager,
ProofAsstPreferences proofAsstPreferences,
ProofAsst proofAsst,
TlPreferences tlPreferences,
TheoremLoader theoremLoader,
java.io.File svcFolder,
java.util.Map<java.lang.String,java.lang.String> svcArgs)
Method go is called by mmj2 after initialization and a RunParm command is
encountered triggering a SvcCallback.
|
void go(Messages messages, OutputBoss outputBoss, LogicalSystem logicalSystem, VerifyProofs verifyProofs, Grammar grammar, WorkVarManager workVarManager, ProofAsstPreferences proofAsstPreferences, ProofAsst proofAsst, TlPreferences tlPreferences, TheoremLoader theoremLoader, java.io.File svcFolder, java.util.Map<java.lang.String,java.lang.String> svcArgs)
The "mmj2 Service" feature adds a new "svc" package to mmj2 and provides a foundation for other, non-mmj2 code to access Metamath data and mmj2 facilities. The primary use envisioned is extracting Metamath data, as the mmj2 Service feature provides easy access to the critical ingredient: formula parse trees!
Access to mmj2 facilities is made available for "caller" and "callee" programs. In both scenarios the BatchMMJ2 program is used to initialize mmj2 with a loaded .mm file which is validated, parsed, etc. Callers actually call BatchMMJ2 passing a "SvcCallback" object which is called by mmj2 once initialization is complete (when the "SvcCall" RunParm is processed.) "Callee" programs simply write a class which implements the SvcCallback interface -- just as "caller" programs do -- but instead of directly calling BatchMMJ2, the user specifies the name of their SvcCallback- implementing class via a "SvcCallback" RunParm.
Whether accessing mmj2 as a "caller" or "callee", complete access to mmj2's main facilities is provided in the SvcCallback.go interface method. The "go()" method is passed references to the biggie mmj2 objects, including ProofAsst, Grammar, VerifyProofs, etc.
Within the SvcCallback.go() method the user-code can execute calls to mmj2 methods but must single-thread the accesses as mmj2 is not, in general, written for total multi- threaded access throughout (some code could be multi-threaded but not all.)
When finished accessing the mmj2 Services, the user-code simply needs to execute a "return" from the SvcCallback.go() method.
New RunParms added to mmj2 for use with BatchMMJ2 (see mmj.util.SvcBoss) are SvcFolder, SvcCallbackClass, SvcArg, and SvcCall. The SrvArg RunParm provides a way for the user-code to obtain Key-Value parameter pairs via the input RunParms file; they are loaded by BatchMMJ2 (with minimal validation) into a HashMap and passed via the SvcCallback.go() method.
More information about these new RunParms is provided in the mmj2jar\AnnotatedRunParms.txt documentation file.
Review sample code and (w/"compile and go" .bat jobs) in
doc\mmj2ServiceSample "callee" and "caller" mode programs are at:
\doc\mmj2Service\TSvcCallbackCallee.java \doc\mmj2Service\TSvcCallbackCaller.javaNote: In "callee" mode, if a "fatal" or severe error is encountered, triggering an IllegalArgumentException will instantly terminate the mmj2 process.
Likewise, in "caller" mode "fatal" errors can result during start-up,
typically resulting in IllegalArgumentException errors being thrown, and
then caught by BatchFramework
and resulting ultimately in a
non-zero return-code from
BatchMMJ2.generateSvcCallback(String[],SvcCallback). So...if
the "caller" mode program gets a non-zero returncode from the
BatchMMJ2.generateSvcCallback() call then that means that either a) mmj2
had a "fatal" error during start-up, or b) that the SvcCallback was
triggered, and one of the user programs threw an exception, such as
IllegalArgumentException, which flowed back to mmj2 and caused the
non-zero return-code.
messages
- mmj.lang.Messages object.outputBoss
- mmj.util.OutputBosslogicalSystem
- mmj.lang.LogicalSystemverifyProofs
- mmj.verify.VerifyProofsgrammar
- mmj.verify.GrammarworkVarManager
- mmj.lang.WorkVarManagerproofAsstPreferences
- mmj.pa.ProofAsstPreferencesproofAsst
- mmj.pa.ProofAssttlPreferences
- mmj.tl.TlPreferencestheoremLoader
- mmj.tl.TheoremLoadersvcFolder
- home Folder for use by Svc (specified via RunParm).svcArgs
- Map of Svc key/value pair arguments (specified via
RunParm).