Interface | Description |
---|---|
TheoremLoaderCommitListener |
Interface for Theorem Loader update commits.
|
TLRequest |
Implements a user request for a TheoremLoader operation on a ProofWorksheet.
|
Class | Description |
---|---|
MMTFileFilter |
MMTFileFilter is used by the Theorem Loader to select theorem files from the
MMT Folder.
|
MMTFolder |
MMTFolder is a helper class for the Theorem Loader.
|
MMTTheoremExportFormatter |
Converts a thing into a list Metamath-formatted file lines.
|
MMTTheoremFile |
MMTTheoremFile is a little helper class for MMT Theorem files.
|
MMTTheoremSet |
MMTTheoremSet represents a set of MMTTheoremStmtGroup objects to be loaded
into the Logical System.
|
StoreInMMTFolderTLRequest |
StoreInMMTFolderTLRequest implements a user request for a TheoremLoader
operation.
|
TheoremLoader |
The Theorem Loader facility's main control module.
|
TheoremStmtGroup |
TheoremStmtGroup represents the contents of a MMTTheoremFile as well as state
variables pertaining to work performed loading the theorem into the
LogicalSystem.
|
TlConstants |
(Most) Constants used in mmj.tl classes
|
TlPreferences |
Holds user settings/preferences used by the Theorem Loader.
|
Enum | Description |
---|---|
TlConstants.DjVarsOption |
Exception | Description |
---|---|
TheoremLoaderException |
Thrown by package mmj.tl methods when a theorem load error is detected.
|