public class Systemizer
extends java.lang.Object
SystemLoader
interface with SrcStmt
objects from
Statementizer
.
Notes:
SrcStmt
objects -- transparently with respect to SystemLoader
.
SystemLoader
of that
condition.
Constructor and Description |
---|
Systemizer() |
Modifier and Type | Method and Description |
---|---|
Messages |
getMessages()
Get
Messages object |
SystemLoader |
getSystemLoader()
Get SystemLoader, as-is.
|
void |
init(Messages messages,
SystemLoader systemLoader,
int loadEndpointStmtNbr,
java.lang.String loadEndpointStmtLabel,
boolean loadComments,
boolean loadProofs)
Initialize (or re-initialize) a
Systemizer from a
Messages object and a SystemLoader object. |
Messages |
load(java.io.File filePath,
java.io.Reader readerIn,
java.lang.String sourceId)
Loads MetaMath source file via
SystemLoader . |
Messages |
load(java.io.File filePath,
java.lang.String fileNameIn)
Clone of Load function using fileNameIn instead of readerIn.
|
Messages |
load(java.io.File filePath,
java.lang.String fileNameIn,
java.lang.String sourceId)
Clone of Load function using fileNameIn instead of readerIn
|
public void init(Messages messages, SystemLoader systemLoader, int loadEndpointStmtNbr, java.lang.String loadEndpointStmtLabel, boolean loadComments, boolean loadProofs)
Systemizer
from a
Messages
object and a SystemLoader
object.messages
- -- repository of error and info messages that provides a
limit on the number of errors output before processing is
halted.systemLoader
- -- a SystemLoader initialized with any customizing
parameters and ready to be loaded with data.loadProofs
- If true then Metamath proofs are loaded into
LogicalSystem, otherwise just a "?" proof is stored with each
Theorem.loadComments
- If true then Metamath comments (at least, for
Theorems) will be loaded.loadEndpointStmtLabel
- last Metamath statement label to load.loadEndpointStmtNbr
- maximum number of Metamath statements to be
loaded.public SystemLoader getSystemLoader()
public Messages getMessages()
Messages
objectMessages
objectpublic Messages load(java.io.File filePath, java.io.Reader readerIn, java.lang.String sourceId) throws java.io.IOException
SystemLoader
.
Note: multiple files can be loaded in serial fashion.
filePath
- -- File object holding directory path for readerIn. Used
to look up Metamath include files. May be null, or absolute
path, or relative.readerIn
- -- may be StringReader or BufferedReader but
PushbackReader and LineNumberReader are not helpful choices.)
Will be closed at EOF.sourceId
- -- caption such as filename or test ID. May be empty
string if N/A. Used solely for diagnostic/testing messages.Messages
object, which can be tested to see if any error
messages were generatedjava.io.IOException
- if I/O errorMessages.getErrorMessageCnt()
public Messages load(java.io.File filePath, java.lang.String fileNameIn, java.lang.String sourceId) throws MMIOException
filePath
- -- File object holding directory path for fileNameIn --
and used to look up Metamath include files. May be null, or
absolute path, or relative.fileNameIn
- -- input .mm file name String.sourceId
- -- test such as filename or test ID. May be empty string
if N/A. Used solely for diagnostic/testing messages.Messages
object, which can be tested to see if any error
messages were generatedMMIOException
- if file requested has already been loaded or does
not exist.public Messages load(java.io.File filePath, java.lang.String fileNameIn) throws MMIOException
filePath
- -- File object holding directory path for fileNameIn --
and used to look up Metamath include files. May be null, or
absolute path, or relative.fileNameIn
- -- input .mm file name String.Messages
object, which can be tested to see if any error
messages were generatedMMIOException
- if file requested has already been loaded.MMIOException
- if file requested does not exist.