public class BookManager extends java.lang.Object implements TheoremLoaderCommitListener
BookManager keeps track of input Chapters and Sections from a .mm database as the data is input, while LogicalSystem controls assigning Section and MObjNbr data items to BookManager's Chapters and Sections. This is an important point: BookManager is called during the FileLoad process as each MObj is created so that the BookManager can assign SectionMObjNbrs in the correct order.
A "Section" is similar to Chapter except that it is contained within a Chapter and the identifying token prefix string is "=-=-".
In some cases there may not be a Section header within a Chapter, and in that case the Chapter title is used for the Section title and a default-Section must be automatically generated by the system.
Likewise, if a valid Chapter comment statement has not been found before Metamath objects or a Section comment statement are input, then a default Chapter with a default title is automatically generated by the system.
It is possible that neither Chapters or Sections are used by an input .mm database. In this case everything is loaded into a single default Chapter with four default Sections.
Note: Input Sections are physically split and assigned sequential
numbers based on the MObj content type as shown below. The Section numbers
are multiples of 1, 2, 3, or 4 as follows:
1 = Cnst or Var symbols
2 = VarHyp
3 = Syntax Axioms
4 = Theorems, Logic Axioms and LogHyps.
Thus, the first input Section is assigned Section numbers 1, 2, 3, and 4. The
2nd input Section is assigned Section numbers 5, 6, 7 and 8. And so on. These
numbers are assigned across Chapter boundaries -- meaning that Section
numbers do not reset to 1 at the beginning of each chapter.
Modifier and Type | Class and Description |
---|---|
class |
BookManager.SectionMObjIterator
Nested class which implements Iterable for a two-dimensional array of
MObjs by Section and MObjNbr within Section.
|
Constructor and Description |
---|
BookManager(boolean enabled,
java.lang.String provableLogicStmtTypeParm)
Sole constructor for BookManager.
|
Modifier and Type | Method and Description |
---|---|
void |
addNewChapter(java.lang.String chapterTitle)
Adds a new Chapter to the BookManager's collection.
|
void |
addNewSection(java.lang.String sectionTitle)
Adds a new Section to the current Chapter in the BookManager's collection
|
void |
assignChapterSectionNbrs(Axiom axiom)
Assigns Chapter and SectionNbrs to an axiom.
|
void |
assignChapterSectionNbrs(LogHyp logHyp)
Assigns Chapter and SectionNbrs to a logical hypothesis.
|
void |
assignChapterSectionNbrs(Sym sym)
Assigns Chapter and SectionNbrs to either a Cnst or a Var.
|
void |
assignChapterSectionNbrs(Theorem theorem)
Assigns Chapter and SectionNbrs to a theorem.
|
void |
assignChapterSectionNbrs(VarHyp varHyp)
Assigns Chapter and SectionNbrs to a VarHyp.
|
java.util.BitSet[] |
buildChapterDependencies(java.util.BitSet[] bs) |
void |
commit(MMTTheoremSet mmtTheoremSet)
Stores new MObj's from the TheoremLoader as part of a load operation.
|
static int |
convertOrigSectionNbr(int i) |
Chapter |
getChapter(int chapterNbr)
Returns the Chapter corresponding to a given Chapter Nbr.
|
java.util.BitSet[] |
getChapterDependencies(LogicalSystem logicalSystem) |
Chapter |
getChapterForSectionNbr(int sectionNbr)
Returns the Chapter corresponding to a given Section Nbr.
|
java.util.List<Chapter> |
getChapterList()
Returns the List of Chapters in the BookManager.
|
int |
getChapterMaxMObjSeq(Chapter chapter) |
int |
getChapterMinMObjSeq(Chapter chapter) |
java.lang.String[] |
getChapterValuesForSearch() |
java.util.BitSet[] |
getDirectChapterDependencies(LogicalSystem logicalsystem) |
java.util.BitSet[] |
getDirectSectionDependencies(LogicalSystem logicalsystem) |
static int |
getOrigSectionNbr(int i) |
Section |
getSection(int sectionNbr)
Returns the Section corresponding to a given Section Nbr.
|
java.util.BitSet[] |
getSectionDependencies(LogicalSystem logicalsystem) |
java.util.List<Section> |
getSectionList()
Returns the List of Sections in the BookManager.
|
int |
getSectionMaxMObjSeq(Section section) |
int |
getSectionMinMObjSeq(Section section) |
MObj[][] |
getSectionMObjArray(LogicalSystem logicalSystem)
Returns a two-dimensional array of MObjs by Section and MObjNbr within
Section.
|
java.lang.Iterable<MObj> |
getSectionMObjIterable(LogicalSystem logicalSystem)
Returns an Iterable over all of the MObjs assigned to Sections.
|
java.lang.String[][] |
getSectionValuesForSearch() |
int |
getTotalNbrMObjs()
Returns the count of all MObj objects assigned to Sections within the
BookManager.
|
void |
invalidateChapterSectionDependencies() |
boolean |
isEnabled()
Returns BookManager enabled flag, which indicates whether or not the
BookManager is in use within the currently system.
|
Chapter |
lookupChapterByTitle(java.lang.String s) |
Section |
lookupSectionByChapterAndTitle(Chapter chapter,
java.lang.String s,
int i) |
void |
recomputeAssrtNbrProofRefs(LogicalSystem logicalSystem) |
public BookManager(boolean enabled, java.lang.String provableLogicStmtTypeParm)
enabled
- Book Manager enabled? If not enabled then zero Chapter and
Section numbers are assigned and no data is retained.provableLogicStmtTypeParm
- String identifying theorems, logic
axioms and logical hypotheses (normally = "|-" in Metamath,
matched against the first symbol of the object's formula).public static int getOrigSectionNbr(int i)
public static int convertOrigSectionNbr(int i)
public void commit(MMTTheoremSet mmtTheoremSet)
BookManager is called to perform its updates en masse at the end of the TheoremLoader update. A failure of BookManager to complete the updates is deemed irreversible and severe, warranting a message to the user to manually restart mmj2.
commit
in interface TheoremLoaderCommitListener
mmtTheoremSet
- the set of MMTTheoremFile object added or updated by
TheoremLoader.public boolean isEnabled()
public Chapter getChapter(int chapterNbr)
chapterNbr
- Chapter number.public Chapter getChapterForSectionNbr(int sectionNbr)
sectionNbr
- Section number.public Section getSection(int sectionNbr)
Note: no processing occurs if BookManager is not enabled.
sectionNbr
- Section number.public void addNewChapter(java.lang.String chapterTitle)
Note: no processing occurs if BookManager is not enabled.
chapterTitle
- Chapter Title or descriptive String.public void addNewSection(java.lang.String sectionTitle)
If no prior Chapter has been input a default Chapter is automatically created.
Note that one call to addNewSection() actually creates the 4 Sections (Symbols, VarHyps, Syntax and Logic) that correspond to one input .mm database section.
Note: no processing occurs if BookManager is not enabled.
sectionTitle
- or descriptive String.public void assignChapterSectionNbrs(Axiom axiom)
If the Type Code of the Axiom is equal to the Provable Logic Statement Type code parameter then the input Axiom is assigned to the current "Logic" Section. Otherwise it is considered to be "Syntax".
This function is provided for use by the LogicalSystem during initial load of an input .mm database. If the MObj has already been assigned SectionMObjNbr then no update is performed (this is significant normally only for re-declared Vars because only Metamath Vars can be validly re-declared -- this happens with in-scope local Var declarations.) no update
Note: no processing occurs if BookManager is not enabled.
axiom
- newly created Axiom.public void assignChapterSectionNbrs(Theorem theorem)
Note: "syntax theorems" are assigned to the current "Logic" section, not "Syntax".
This function is provided for use by the LogicalSystem during initial load of an input .mm database. If the MObj has already been assigned SectionMObjNbr then no update is performed (this is significant normally only for re-declared Vars because only Metamath Vars can be validly re-declared -- this happens with in-scope local Var declarations.) no update
Note: no processing occurs if BookManager is not enabled.
theorem
- newly created Theorem.public void assignChapterSectionNbrs(LogHyp logHyp)
This function is provided for use by the LogicalSystem during initial load of an input .mm database. If the MObj has already been assigned SectionMObjNbr then no update is performed (this is significant normally only for re-declared Vars because only Metamath Vars can be validly re-declared -- this happens with in-scope local Var declarations.) no update
Note: no processing occurs if BookManager is not enabled.
logHyp
- newly created LogHyp.public void assignChapterSectionNbrs(VarHyp varHyp)
This function is provided for use by the LogicalSystem during initial load of an input .mm database. If the MObj has already been assigned SectionMObjNbr then no update is performed (this is significant normally only for re-declared Vars because only Metamath Vars can be validly re-declared -- this happens with in-scope local Var declarations.) no update
Note: no processing occurs if BookManager is not enabled.
varHyp
- newly created VarHyppublic void assignChapterSectionNbrs(Sym sym)
This function is provided for use by the LogicalSystem during initial load of an input .mm database. If the MObj has already been assigned SectionMObjNbr then no update is performed (this is significant normally only for re-declared Vars because only Metamath Vars can be validly re-declared -- this happens with in-scope local Var declarations.) no update
Note: no processing occurs if BookManager is not enabled.
sym
- newly created Sym.public int getTotalNbrMObjs()
public java.util.List<Chapter> getChapterList()
Note: if BookManager is not enabled, the List returned will not be null, it will be empty.
public Chapter lookupChapterByTitle(java.lang.String s)
public Section lookupSectionByChapterAndTitle(Chapter chapter, java.lang.String s, int i)
public java.lang.String[] getChapterValuesForSearch()
public java.lang.String[][] getSectionValuesForSearch()
public void invalidateChapterSectionDependencies()
public void recomputeAssrtNbrProofRefs(LogicalSystem logicalSystem)
public java.util.BitSet[] getChapterDependencies(LogicalSystem logicalSystem)
public java.util.BitSet[] getDirectChapterDependencies(LogicalSystem logicalsystem)
public java.util.BitSet[] buildChapterDependencies(java.util.BitSet[] bs)
public int getChapterMinMObjSeq(Chapter chapter)
public int getChapterMaxMObjSeq(Chapter chapter)
public int getSectionMinMObjSeq(Section section)
public int getSectionMaxMObjSeq(Section section)
public java.util.BitSet[] getSectionDependencies(LogicalSystem logicalsystem)
public java.util.BitSet[] getDirectSectionDependencies(LogicalSystem logicalsystem)
public java.util.List<Section> getSectionList()
Note: if BookManager is not enabled, the List returned will not be null, it will be empty.
public java.lang.Iterable<MObj> getSectionMObjIterable(LogicalSystem logicalSystem)
Note: if BookManager is not enabled, the Iterable returned will not be null, it will be empty.
logicalSystem
- the mmj2 LogicalSystem object.public MObj[][] getSectionMObjArray(LogicalSystem logicalSystem)
Note: if BookManager is not enabled, the array is empty and is allocated
as new MObj[0][]
.
logicalSystem
- the mmj2 LogicalSystem object.