Skip navigation links
mmj.lang

Class BookManager

    • Constructor Detail

      • BookManager

        public BookManager(boolean enabled,
                           java.lang.String provableLogicStmtTypeParm)
        Sole constructor for BookManager.
        Parameters:
        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).
    • Method Detail

      • getOrigSectionNbr

        public static int getOrigSectionNbr(int i)
      • convertOrigSectionNbr

        public static int convertOrigSectionNbr(int i)
      • commit

        public void commit(MMTTheoremSet mmtTheoremSet)
        Stores new MObj's from the TheoremLoader as part of a load operation.

        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.

        Specified by:
        commit in interface TheoremLoaderCommitListener
        Parameters:
        mmtTheoremSet - the set of MMTTheoremFile object added or updated by TheoremLoader.
      • isEnabled

        public boolean isEnabled()
        Returns BookManager enabled flag, which indicates whether or not the BookManager is in use within the currently system.
        Returns:
        BookManager enabled flag.
      • getChapter

        public Chapter getChapter(int chapterNbr)
        Returns the Chapter corresponding to a given Chapter Nbr.
        Parameters:
        chapterNbr - Chapter number.
        Returns:
        Chapter or null if no such chapter exists.
      • getChapterForSectionNbr

        public Chapter getChapterForSectionNbr(int sectionNbr)
        Returns the Chapter corresponding to a given Section Nbr.
        Parameters:
        sectionNbr - Section number.
        Returns:
        Chapter or null if no such section exists.
      • getSection

        public Section getSection(int sectionNbr)
        Returns the Section corresponding to a given Section Nbr.

        Note: no processing occurs if BookManager is not enabled.

        Parameters:
        sectionNbr - Section number.
        Returns:
        Chapter or null if no such section exists or BookManager is not enabled.
      • addNewChapter

        public void addNewChapter(java.lang.String chapterTitle)
        Adds a new Chapter to the BookManager's collection.

        Note: no processing occurs if BookManager is not enabled.

        Parameters:
        chapterTitle - Chapter Title or descriptive String.
      • addNewSection

        public void addNewSection(java.lang.String sectionTitle)
        Adds a new Section to the current Chapter in the BookManager's collection

        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.

        Parameters:
        sectionTitle - or descriptive String.
      • assignChapterSectionNbrs

        public void assignChapterSectionNbrs(Axiom axiom)
        Assigns Chapter and SectionNbrs to an 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.

        Parameters:
        axiom - newly created Axiom.
      • assignChapterSectionNbrs

        public void assignChapterSectionNbrs(Theorem theorem)
        Assigns Chapter and SectionNbrs to a 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.

        Parameters:
        theorem - newly created Theorem.
      • assignChapterSectionNbrs

        public void assignChapterSectionNbrs(LogHyp logHyp)
        Assigns Chapter and SectionNbrs to a logical hypothesis.

        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.

        Parameters:
        logHyp - newly created LogHyp.
      • assignChapterSectionNbrs

        public void assignChapterSectionNbrs(VarHyp varHyp)
        Assigns Chapter and SectionNbrs to a 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.

        Parameters:
        varHyp - newly created VarHyp
      • assignChapterSectionNbrs

        public void assignChapterSectionNbrs(Sym sym)
        Assigns Chapter and SectionNbrs to either a Cnst or a Var.

        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.

        Parameters:
        sym - newly created Sym.
      • getTotalNbrMObjs

        public int getTotalNbrMObjs()
        Returns the count of all MObj objects assigned to Sections within the BookManager.
        Returns:
        total number of MObjs added so far.
      • getChapterList

        public java.util.List<Chapter> getChapterList()
        Returns the List of Chapters in the BookManager.

        Note: if BookManager is not enabled, the List returned will not be null, it will be empty.

        Returns:
        List of Chapters.
      • lookupChapterByTitle

        public Chapter lookupChapterByTitle(java.lang.String s)
      • lookupSectionByChapterAndTitle

        public Section lookupSectionByChapterAndTitle(Chapter chapter,
                                                      java.lang.String s,
                                                      int i)
      • getChapterValuesForSearch

        public java.lang.String[] getChapterValuesForSearch()
      • getSectionValuesForSearch

        public java.lang.String[][] getSectionValuesForSearch()
      • invalidateChapterSectionDependencies

        public void invalidateChapterSectionDependencies()
      • recomputeAssrtNbrProofRefs

        public void recomputeAssrtNbrProofRefs(LogicalSystem logicalSystem)
      • getChapterDependencies

        public java.util.BitSet[] getChapterDependencies(LogicalSystem logicalSystem)
      • getDirectChapterDependencies

        public java.util.BitSet[] getDirectChapterDependencies(LogicalSystem logicalsystem)
      • buildChapterDependencies

        public java.util.BitSet[] buildChapterDependencies(java.util.BitSet[] bs)
      • getChapterMinMObjSeq

        public int getChapterMinMObjSeq(Chapter chapter)
      • getChapterMaxMObjSeq

        public int getChapterMaxMObjSeq(Chapter chapter)
      • getSectionMinMObjSeq

        public int getSectionMinMObjSeq(Section section)
      • getSectionMaxMObjSeq

        public int getSectionMaxMObjSeq(Section section)
      • getSectionDependencies

        public java.util.BitSet[] getSectionDependencies(LogicalSystem logicalsystem)
      • getDirectSectionDependencies

        public java.util.BitSet[] getDirectSectionDependencies(LogicalSystem logicalsystem)
      • getSectionList

        public java.util.List<Section> getSectionList()
        Returns the List of Sections in the BookManager.

        Note: if BookManager is not enabled, the List returned will not be null, it will be empty.

        Returns:
        List of Sections.
      • getSectionMObjIterable

        public java.lang.Iterable<MObj> getSectionMObjIterable(LogicalSystem logicalSystem)
        Returns an Iterable over all of the MObjs assigned to Sections.

        Note: if BookManager is not enabled, the Iterable returned will not be null, it will be empty.

        Parameters:
        logicalSystem - the mmj2 LogicalSystem object.
        Returns:
        List of Sections.
      • getSectionMObjArray

        public MObj[][] getSectionMObjArray(LogicalSystem logicalSystem)
        Returns a two-dimensional array of MObjs by Section and MObjNbr within Section.

        Note: if BookManager is not enabled, the array is empty and is allocated as new MObj[0][].

        Parameters:
        logicalSystem - the mmj2 LogicalSystem object.
        Returns:
        two-dimensional array of MObjs by Section and MObjNbr within Section.