public interface SystemLoader
Interface, initially for mmj.lang.LogicalSystem and passed to mmj.mmio.Systemizer. Allows a different Logical System to be substituted. A different use is possible, such as dumping the parsed .mm file statements somewhere else. Systemizer has no need to know anything about LogicalSystem except where to send the data.
Modifier and Type | Method and Description |
---|---|
Axiom |
addAxiom(java.lang.String labelS,
java.lang.String typS,
java.util.List<java.lang.String> symList)
Add Axiom to Logical System.
|
Cnst |
addCnst(java.lang.String id)
Add Cnst to Logical System.
|
DjVars |
addDjVars(java.lang.String djVar1S,
java.lang.String djVar2S)
Add DjVars (Disjoint Variables Restriction) to Logical System.
|
LogHyp |
addLogHyp(java.lang.String labelS,
java.lang.String typS,
java.util.List<java.lang.String> symList)
Add LogHyp (Logical Hypothesis) to Logical System.
|
void |
addNewChapter(java.lang.String chapterTitle)
Add new Chapter.
|
void |
addNewSection(java.lang.String sectionTitle)
Add new Section.
|
Theorem |
addTheorem(java.lang.String labelS,
int column,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<java.lang.String> proofList,
BlockList proofBlockList,
Messages messages)
Add Theorem to Logical System.
|
Theorem |
addTheorem(java.lang.String labelS,
int column,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<java.lang.String> proofList,
Messages messages)
Add Theorem to Logical System.
|
Var |
addVar(java.lang.String id)
Add Var to Logical System.
|
VarHyp |
addVarHyp(java.lang.String labelS,
java.lang.String typS,
java.lang.String varS)
Add VarHyp to Logical System.
|
void |
beginScope()
Begin a new (nested) scope level for the Logical System.
|
void |
cacheTypesettingCommentForGMFF(java.lang.String comment)
Cache Metamath comment containing typesetting definitions for use by
GMFF.
|
void |
endScope()
Ends a (nested) scope level for the Logical System.
|
void |
finalizeEOF(Messages messages,
boolean prematureEOF)
EOF processing for Logical System after file loaded.
|
boolean |
isBookManagerEnabled()
Is BookManager enabled?
|
Cnst addCnst(java.lang.String id) throws MMJException
id
- Constant's symbol string to be added to the Logical System.MMJException
- if duplicate symbol, etc.Var addVar(java.lang.String id) throws MMJException
id
- Var's symbol string to be added to the Logical System.MMJException
- if duplicate symbol, etc.VarHyp addVarHyp(java.lang.String labelS, java.lang.String typS, java.lang.String varS) throws MMJException
labelS
- String label of variable hypothesistypS
- String Metamath constant character (type code)varS
- String Metamath variable characterMMJException
- if duplicate symbol, etc. (see
mmj.lang.LangConstants.java
)DjVars addDjVars(java.lang.String djVar1S, java.lang.String djVar2S) throws MMJException
djVar1S
- disjoint variable symbol string 1djVar2S
- disjoint variable symbol string 2MMJException
- if duplicate vars, etc. (see
mmj.lang.LangConstants.java
)LogHyp addLogHyp(java.lang.String labelS, java.lang.String typS, java.util.List<java.lang.String> symList) throws MMJException
labelS
- logical hypothesis label stringtypS
- logical hypothesis type code (symbol) stringsymList
- list containing expression symbol strings (zero or more
symbols).MMJException
- if duplicate label, undefined vars, etc.Axiom addAxiom(java.lang.String labelS, java.lang.String typS, java.util.List<java.lang.String> symList) throws MMJException
labelS
- axiom label stringtypS
- axiom type code (symbol) stringsymList
- list containing axiom expression symbol strings (zero or
more symbols).MMJException
- if duplicate label, undefined vars, etc.Theorem addTheorem(java.lang.String labelS, int column, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<java.lang.String> proofList, Messages messages) throws MMJException
labelS
- axiom label stringcolumn
- the column at which the "$p" line startstypS
- axiom type code (symbol) stringsymList
- list containing axiom expression symbol strings (zero or
more symbols).proofList
- list containing proof step symbol strings (1 or more
symbols -- which may be "?" if a step is unknown).messages
- for error reportingMMJException
- if duplicate label, undefined vars, etc.Theorem addTheorem(java.lang.String labelS, int column, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<java.lang.String> proofList, BlockList proofBlockList, Messages messages) throws MMJException
This variant is invoked when the input contains a compressed proof.
labelS
- axiom label stringcolumn
- the column at which the "$p" line startstypS
- axiom type code (symbol) stringsymList
- list containing axiom expression symbol strings (zero or
more symbols).proofList
- list containing the contents of the parenthesized
portion of a compressed proof (does not include the
parentheses)proofBlockList
- list containing one or more blocks of compressed
proof symbols.messages
- for error reportingMMJException
- if duplicate label, undefined vars, etc.void beginScope()
ScopeDef
void endScope() throws MMJException
MMJException
- if scope is already at the global scope level.ScopeDef
void finalizeEOF(Messages messages, boolean prematureEOF) throws MMJException
messages
- Messages object to error reporting.prematureEOF
- signals LoadLimit requested by user has been reached,
so stop loading even if in the middle of a scope level.MMJException
- if scope is NOT at the global scope level UNLESS
premature EOF signalled. (see
mmj.lang.LangConstants.java
)boolean isBookManagerEnabled()
If BookManager is enabled then Chapters and Sections will be stored.
void addNewChapter(java.lang.String chapterTitle)
See mmj.lang.BookManager.java for more info.
chapterTitle
- Title of chapter or blank or empty String.void addNewSection(java.lang.String sectionTitle)
See mmj.lang.BookManager.java for more info.
sectionTitle
- Title of section or blank or empty String.void cacheTypesettingCommentForGMFF(java.lang.String comment)
Note: comment is from mmj.mmio.SrcStmt so it does not contain the "$(" and "$)" start/end comment id tokens which are standard to Metamath comments.
Note: per agreement with Norm, the "$t" token identifying typesetting definitions in a comment is the first non-whitespace token after the "$(" in the comment.
comment
- Typesetting definition comment ("$t) from Metamath file
minus the "$(" and "$)" tokens.