public class TheoremLoader
extends java.lang.Object
Note: this class is primarily an entry point and convenience for Theorem Loader users (batch or GUI.)
Constructor and Description |
---|
TheoremLoader(TlPreferences tlPreferences)
Main constructor for TheoremLoader.
|
Modifier and Type | Method and Description |
---|---|
void |
extractTheoremToMMTFolder(Theorem theorem,
LogicalSystem logicalSystem,
Messages messages)
Reads a theorem from the Logical System and writes it to the MMT Folder.
|
TlPreferences |
getTlPreferences() |
ProofWorksheet |
getUnifiedProofWorksheet(java.lang.String proofWorksheetText,
ProofAsst proofAsst,
java.lang.String filenameOrDataSourceId)
Unifies an mmj2 Proof Text area.
|
void |
loadTheoremsFromMMTFolder(LogicalSystem logicalSystem,
Messages messages)
Loads all MMT Theorems in the MMT Folder into the Logical System.
|
void |
loadTheoremsFromMMTFolder(java.lang.String theoremLabel,
LogicalSystem logicalSystem,
Messages messages)
Loads one theorem from the MMT Folder into the Logical System.
|
void |
storeInLogSysAndMMTFolder(ProofWorksheet proofWorksheet,
LogicalSystem logicalSystem,
Messages messages,
ProofAsst proofAsst)
Stores a unified ProofWorksheet in the Logical System and the MMT Folder.
|
void |
storeInMMTFolder(ProofWorksheet proofWorksheet,
LogicalSystem logicalSystem,
Messages messages,
ProofAsst proofAsst)
Stores a unified ProofWorksheet in the MMT Folder.
|
ProofWorksheet |
unifyPlusStoreInLogSysAndMMTFolder(java.lang.String proofWorksheetText,
LogicalSystem logicalSystem,
Messages messages,
ProofAsst proofAsst,
java.lang.String inputProofWorksheetFileName)
Unifies mmj2 Proof Text area and stores the theorem in the Logical System
and MMT Folder.
|
ProofWorksheet |
unifyPlusStoreInMMTFolder(java.lang.String proofWorksheetText,
LogicalSystem logicalSystem,
Messages messages,
ProofAsst proofAsst,
java.lang.String inputProofWorksheetFileName)
Unifies mmj2 Proof Text area and stores the theorem in the MMT Folder.
|
public TheoremLoader(TlPreferences tlPreferences)
tlPreferences
- TlPreferences object.public ProofWorksheet unifyPlusStoreInLogSysAndMMTFolder(java.lang.String proofWorksheetText, LogicalSystem logicalSystem, Messages messages, ProofAsst proofAsst, java.lang.String inputProofWorksheetFileName) throws TheoremLoaderException
proofWorksheetText
- text area holding an mmj2 Proof Worksheet.logicalSystem
- LogicalSystem object.messages
- Messages object.proofAsst
- ProofAsst object.inputProofWorksheetFileName
- String used for error reporting.TheoremLoaderException
- if data errors encountered, including the
case where the ProofWorksheet cannot be unified.public ProofWorksheet unifyPlusStoreInMMTFolder(java.lang.String proofWorksheetText, LogicalSystem logicalSystem, Messages messages, ProofAsst proofAsst, java.lang.String inputProofWorksheetFileName) throws TheoremLoaderException
proofWorksheetText
- text area holding an mmj2 Proof Worksheet.logicalSystem
- LogicalSystem object.messages
- Messages object.proofAsst
- ProofAsst object.inputProofWorksheetFileName
- String used for error reporting.TheoremLoaderException
- if data errors encountered, including the
case where the ProofWorksheet cannot be unified.public void storeInLogSysAndMMTFolder(ProofWorksheet proofWorksheet, LogicalSystem logicalSystem, Messages messages, ProofAsst proofAsst) throws TheoremLoaderException
proofWorksheet
- ProofWorksheet object already successfully unified.logicalSystem
- LogicalSystem object.messages
- Messages object.proofAsst
- ProofAsst object.TheoremLoaderException
- if data errors encountered, including the
case where the ProofWorksheet is not already unified.public void storeInMMTFolder(ProofWorksheet proofWorksheet, LogicalSystem logicalSystem, Messages messages, ProofAsst proofAsst) throws TheoremLoaderException
proofWorksheet
- ProofWorksheet object already successfully unified.logicalSystem
- LogicalSystem object.messages
- Messages object.proofAsst
- ProofAsst object.TheoremLoaderException
- if data errors encountered, including the
case where the ProofWorksheet is not already unified.public void loadTheoremsFromMMTFolder(LogicalSystem logicalSystem, Messages messages) throws TheoremLoaderException
Note: the current MMT Folder is obtained from the TlPreferences object.
logicalSystem
- LogicalSystem object.messages
- Messages object.TheoremLoaderException
- if data errors encountered.public void loadTheoremsFromMMTFolder(java.lang.String theoremLabel, LogicalSystem logicalSystem, Messages messages) throws TheoremLoaderException
Note: the input theoremLabel is used to construct the file name to be read from the MMT Folder.
theoremLabel
- label of the theorem to be loaded.logicalSystem
- LogicalSystem object.messages
- Messages object.TheoremLoaderException
- if data errors encountered.public void extractTheoremToMMTFolder(Theorem theorem, LogicalSystem logicalSystem, Messages messages) throws TheoremLoaderException
Note: the theorem Label is used to construct the file name to be written to the MMT Folder.
theorem
- Theorem to be written to the MMT Folder.logicalSystem
- LogicalSystem object.messages
- Messages object.TheoremLoaderException
- if data errors encountered.public ProofWorksheet getUnifiedProofWorksheet(java.lang.String proofWorksheetText, ProofAsst proofAsst, java.lang.String filenameOrDataSourceId) throws TheoremLoaderException
proofWorksheetText
- text of a ProofWorksheet.proofAsst
- ProofAsst objectfilenameOrDataSourceId
- text for diagnosticsTheoremLoaderException
- if there is an error in the proof.public TlPreferences getTlPreferences()