public class TypesetDefCommentParser
extends java.lang.Object
TypesetDefCommentParser
parses, validates and loads Map
collections with typesetting data from Metamath Comment statements identified
by a $t
as the first token after the Comment ID token $(
.
Almost all necessary specifications for processing Metamath typesetting
information is contained in the Metamath.pdf
book, with the following
exceptions:
$t
token up to the terminating $)
token. (Double-Slash C-style comments are not treated as comments.)
$t
Comment statements is of the form: '
keyword xxxStuffxxx;'.
htmldef
, althtmldef
, and latexdef
-- these
keywords are input parameters, not hardcoded -- but other definitions may be
added in the future and GMFF must be able to correctly bypass these
definitions.
Note that the input Metamath Comment statements processed by
TypesetDefCommentParser
are stripped of their delimiting $(
and $)
tokens prior to input. This is a result of the way that mmj2
parses input files and stores Metamath Comments in mmj.mmio.SrcStmt
.
TypesetDefCommentParser
is coded as a separate class in order to
provide modularity, not because there are separate instances of it.
GMFFManager
instantiates it and then calls
doIt(String typesetDefComment)
for each Metamath $t
Comment
statement to be processed.
Another curious/strange aspect of processing is that mmj2 accumulates
Metamath typesetting Comment statements in the GMFFManager
via
mmj.mmio.Systemizer
method loadComment()
but the typesetting
Comments are not processed unless and until the user or a RunParm command
invokes GMFF's typsetting services -- at which point GMFFManager
invokes TypesetDefCommentParser
.
Constructor and Description |
---|
TypesetDefCommentParser(java.util.List<GMFFExporterTypesetDefs> exporterTypesetDefsList,
Messages messages)
The only constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
doIt(java.lang.String typesetDefComment)
Parses, validates and loads
Map collections with symbol
typesetting definitions with keywords matching the constructor
exporterTypesetDefsList list. |
public TypesetDefCommentParser(java.util.List<GMFFExporterTypesetDefs> exporterTypesetDefsList, Messages messages) throws GMFFException
exporterTypesetDefsList
- List of
GMFFExporterTypesetDefs
which are to be selected for
processing and loaded with data.
messages
- The mmj2 Messages object.
GMFFException
- if an error occurredpublic void doIt(java.lang.String typesetDefComment) throws GMFFException
Map
collections with symbol
typesetting definitions with keywords matching the constructor
exporterTypesetDefsList
list.typesetDefComment
- Metamath $t
Comment statement stripped
of its $(
beginning and $)
ending tokens.GMFFException
- if parse or validation errors encountered.