public class StoreInMMTFolderTLRequest extends java.lang.Object implements TLRequest
This class is basically just a name which is used by the ProofAsstGUI to identify the user's request, and a call to implement the request.
The input ProofWorksheet must be already successfully unified, or else a TheoremLoaderException is thrown. The ProofWorksheet is converted to Metamath .mm format and stored in the MMT Folder,
Constructor and Description |
---|
StoreInMMTFolderTLRequest() |
Modifier and Type | Method and Description |
---|---|
void |
doIt(TheoremLoader theoremLoader,
ProofWorksheet proofWorksheet,
LogicalSystem logicalSystem,
Messages messages,
ProofAsst proofAsst)
Implements the request to store a ProofWorksheet in the MMT Folder.
|
public void doIt(TheoremLoader theoremLoader, ProofWorksheet proofWorksheet, LogicalSystem logicalSystem, Messages messages, ProofAsst proofAsst) throws TheoremLoaderException
doIt
in interface TLRequest
theoremLoader
- TheoremLoader object.proofWorksheet
- ProofWorksheet object.logicalSystem
- LogicalSystem object.messages
- Messages object.proofAsst
- ProofAsst object.TheoremLoaderException
- if there are any data errors encountered
while performing the requested function.