public class SrcStmt
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
int |
column
The column that a VarHyp, LogHyp, Theorem or Axiom starts at.
|
java.lang.String |
comment
Comment statement --
|
java.lang.String |
includeFileName
Include File Name from "$[" statement.
|
java.lang.String |
keyword
Every SrcStmt has a keyword, even a comment (char 1 = '$', always.)
|
java.lang.String |
label
VarHyp, LogHyp, Theorem and Axiom have labels.
|
BlockList |
proofBlockList
Theorem compressed proof block list.
|
java.util.List<java.lang.String> |
proofList
Only Theorem statements ($p) have proofList.
|
int |
seq
Every SrcStmt has a sequence number, even a comment.
|
java.util.List<java.lang.String> |
symList
symlist is the 2nd through nth symbols in the Metamath source statement.
|
java.lang.String |
typ
VarHyp, LogHyp, Theorem and Axiom have typ, which internally corresponds
to the first symbol of a Formula externally, is the first symbol
following the Metamath statement's keyword ($a, $p, etc.)
|
Constructor and Description |
---|
SrcStmt(int seqNbr,
java.lang.String keyword)
Construct using sequence number and MetaMath keyword.
|
public int seq
Note: this seq
is not necessarily the same value stored in
LogicalSystem
or whatever object implements SystemLoader
.
Both are sequential (ha), but LogicalSystem may use a multiplier or
transform the sequence number in some other way.
public java.lang.String label
public int column
public java.lang.String keyword
public java.lang.String typ
public java.util.List<java.lang.String> symList
DjVar, Var, Cnst, VarHyp, LogHyp, Theorem and Axiom have symList:
DjVar: at least 2 sym Strings Var & Cnst: at least 1 VarHyp: exactly 1, guaranteed :) Axiom, LogHyp & Theorem: zero or more
public java.util.List<java.lang.String> proofList
proofList is guaranteed to have at least one proofStep string (which will be label of a statement... or "?").
Note: if proofBlockList not null then proofList contains the labels inside the parenthesized portion of a compressed proof (but not the parentheses.)
public BlockList proofBlockList
Null value signifies proof is not compressed. Otherwise, contains 1 or more Strings containing Metamath compressed proof symbols (see Metamath.pdf Appendix B).
public java.lang.String comment
This is the entire comment excluding the start/end comment keywords. All other tokens are present, including the intervening whitespace newlines.
public java.lang.String includeFileName
Does not include the $[, $] tokens or the whitespace chunks, just the file name.