public class ProofWorksheetParser
extends java.lang.Object
implements java.io.Closeable
The big shortcoming that it has right now, which may not be big depending on your plans, is that an input ProofWorksheet with structural errors or other severe errors, throws an exception and leaves the input stream stuck in the middle of the worksheet tokens. An enhancement might be to add a routine to chunk through the input stream and bypass tokens until a proof worksheet "Footer" is found, and then grab the *next* token, which could be used to initiate and parse the following ProofWorksheet. However, at this time, batches of ProofWorksheets are used only in testing, so no energy has been expended in bypassing an errored ProofWorksheet's remaining tokens.
Constructor and Description |
---|
ProofWorksheetParser(java.io.File proofFile,
java.lang.String proofTextSource,
ProofAsstPreferences proofAsstPreferences,
LogicalSystem logicalSystem,
Grammar grammar,
Messages messages,
MacroManager macroManager)
Constructor.
|
ProofWorksheetParser(java.io.Reader proofTextReader,
java.lang.String proofTextSource,
ProofAsstPreferences proofAsstPreferences,
LogicalSystem logicalSystem,
Grammar grammar,
Messages messages,
MacroManager macroManager)
Constructor.
|
ProofWorksheetParser(java.lang.String proofText,
java.lang.String proofTextSource,
ProofAsstPreferences proofAsstPreferences,
LogicalSystem logicalSystem,
Grammar grammar,
Messages messages,
MacroManager macroManager)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
close() |
boolean |
hasNext()
Checks to see if another ProofWorksheet is available.
|
ProofWorksheet |
next()
Returns the next ProofWorksheet from the input source for situations when
input cursor position not available.
|
ProofWorksheet |
next(int inputCursorPos,
StepRequest stepRequest)
Returns the next ProofWorksheet from the input source.
|
public ProofWorksheetParser(java.io.Reader proofTextReader, java.lang.String proofTextSource, ProofAsstPreferences proofAsstPreferences, LogicalSystem logicalSystem, Grammar grammar, Messages messages, MacroManager macroManager) throws java.io.IOException, MMIOException
proofTextReader
- Reader of ProofWorksheet tokensproofTextSource
- Comment for debugging/testingproofAsstPreferences
- variable settingslogicalSystem
- the loaded Metamath datagrammar
- the mmj.verify.Grammar objectmessages
- the mmj.lang.Messages object used to store error and
informational messages.macroManager
- the mmj.pa.MacroManager objectjava.io.IOException
- if an error occurredMMIOException
- if an error occurredpublic ProofWorksheetParser(java.lang.String proofText, java.lang.String proofTextSource, ProofAsstPreferences proofAsstPreferences, LogicalSystem logicalSystem, Grammar grammar, Messages messages, MacroManager macroManager) throws java.io.IOException, MMIOException
proofText
- String containing ProofWorksheet tokensproofTextSource
- Comment for debugging/testingproofAsstPreferences
- variable settingslogicalSystem
- the loaded Metamath datagrammar
- the mmj.verify.Grammar objectmessages
- the mmj.lang.Messages object used to store error and
informational messages.macroManager
- the mmj.pa.MacroManager objectjava.io.IOException
- if an error occurredMMIOException
- if an error occurredpublic ProofWorksheetParser(java.io.File proofFile, java.lang.String proofTextSource, ProofAsstPreferences proofAsstPreferences, LogicalSystem logicalSystem, Grammar grammar, Messages messages, MacroManager macroManager) throws java.io.IOException, MMIOException
proofFile
- File object specifying ProofWorksheet token file for
input.proofTextSource
- Comment for debugging/testingproofAsstPreferences
- variable settingslogicalSystem
- the loaded Metamath datagrammar
- the mmj.verify.Grammar objectmessages
- the mmj.lang.Messages object used to store error and
informational messages.macroManager
- the mmj.pa.MacroManager objectjava.io.IOException
- if an error occurredMMIOException
- if an error occurredpublic void close() throws java.io.IOException
close
in interface java.io.Closeable
close
in interface java.lang.AutoCloseable
java.io.IOException
public boolean hasNext()
public ProofWorksheet next() throws java.io.IOException, MMIOException, ProofAsstException
java.io.IOException
- if an error occurredMMIOException
- if an error occurredProofAsstException
- if an error occurredpublic ProofWorksheet next(int inputCursorPos, StepRequest stepRequest) throws java.io.IOException, MMIOException, ProofAsstException
inputCursorPos
- offset plus one of Caret in Proof TextArea;stepRequest
- may be null, or StepSelector Search or Choice request
and will be loaded into the ProofWorksheet.java.io.IOException
- if an error occurredMMIOException
- if an error occurredProofAsstException
- if an error occurred