public class MMTTheoremSet extends java.lang.Object implements java.lang.Iterable<TheoremStmtGroup>
Constructor and Description |
---|
MMTTheoremSet(java.io.File[] fileArray,
LogicalSystem logicalSystem,
Messages messages,
TlPreferences tlPreferences)
Constructs the MMTTheoremSet using an array of Files, which may be
obtained from the MMTFolder.
|
MMTTheoremSet(MMTTheoremFile mmtTheoremFile,
LogicalSystem logicalSystem,
Messages messages,
TlPreferences tlPreferences)
Constructs the MMTTheoremSet using a single input MMTTheoremFile.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<Theorem> |
buildSortedAssrtListOfAdds(java.util.Comparator<? super Theorem> comparator)
Returns a List of Theorems in the MMTTheoremSet which were added to the
LogicalSystem during the load process.
|
java.util.List<TheoremStmtGroup> |
buildSortedListOfAdds(java.util.Comparator<? super TheoremStmtGroup> comparator)
Returns a List of the TheoremStmtGroups in the MMTTheoremSet which were
added to the LogicalSystem during the load process.
|
java.util.Iterator<TheoremStmtGroup> |
iterator()
Returns an Iterator over TheoremStmtGroup objects contained in the
MMTTheoremSet theoremStmtGroupTbl.
|
void |
updateLogicalSystem()
Updates the LogicalSystem using the contents of the MMTTheoremSet.
|
public MMTTheoremSet(java.io.File[] fileArray, LogicalSystem logicalSystem, Messages messages, TlPreferences tlPreferences) throws TheoremLoaderException
Validation of the input theorems is performed.
fileArray
- array of Files designating MMTTheoremFiles to be loaded
into the MMTTheoremSet.logicalSystem
- LogicalSystem object.messages
- Messages object.tlPreferences
- TlPreferences object.TheoremLoaderException
- if there are any errors reading the input
files or if there are validation errors.public MMTTheoremSet(MMTTheoremFile mmtTheoremFile, LogicalSystem logicalSystem, Messages messages, TlPreferences tlPreferences) throws TheoremLoaderException
Validation of the input theorem is performed.
mmtTheoremFile
- MMTTheoremFile to be loaded into the MMTTheoremSet.logicalSystem
- LogicalSystem object.messages
- Messages object.tlPreferences
- TlPreferences object.TheoremLoaderException
- if there are any errors reading the input
files or if there are validation errors.public java.util.List<TheoremStmtGroup> buildSortedListOfAdds(java.util.Comparator<? super TheoremStmtGroup> comparator)
Note: this method is called by mmj.lang.BookManager.java during "commit()" processing at the end of the TheoremLoader load process.
comparator
- Comparator for TheoremStmtGroup.public java.util.List<Theorem> buildSortedAssrtListOfAdds(java.util.Comparator<? super Theorem> comparator)
Note: this method is called by mmj.pa.ProofAsst.java during "commit()" processing at the end of the TheoremLoader load process.
comparator
- Comparator for mmj.lang.Assrt.public java.util.Iterator<TheoremStmtGroup> iterator()
Note: this is used in LogicalSystem and SeqAssigner during rollback() processing (fyi).
iterator
in interface java.lang.Iterable<TheoremStmtGroup>
public void updateLogicalSystem() throws TheoremLoaderException
If errors are encountered during the update, logicalSystem.theoremLoaderRollback() is called to reverse any previous updates.
Likewise, if no errors are encountered during the update, logicalSystem.theoremLoaderCommit() is called to finalize the updates.
FYI, this is called by TheoremLoader.
TheoremLoaderException
- if any errors are encountered during the
update process.java.lang.IllegalArgumentException
- if either rollback or commit of the
updates fail.