public class MMTTheoremExportFormatter
extends java.lang.Object
The output Metamath .mm file text lines are formatted according to the Theorem Loader Preferences.
Note: output lines do not contain newlines.
Note: this code handles Theorems and ProofWorksheets, and in theory there could be subclasses involved, but it seemed ok to just put all of the formatting code in one spot here as a quick and dirty bit of coding.
Constructor and Description |
---|
MMTTheoremExportFormatter(TlPreferences tlPreferences)
Basic constructor.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<java.lang.StringBuilder> |
buildStringBuilderLineList(ProofWorksheet proofWorksheet)
Converts a ProofWorksheet into a list of StringBuilder lines formatted
into Metamath format.
|
java.util.List<java.lang.StringBuilder> |
buildStringBuilderLineList(Theorem theorem)
Converts a Theorem in the LogicalSystem into a list of StringBuilder
lines formatted into Metamath format.
|
public MMTTheoremExportFormatter(TlPreferences tlPreferences)
tlPreferences
- TlPreferences object.public java.util.List<java.lang.StringBuilder> buildStringBuilderLineList(Theorem theorem)
theorem
- Theorem in the Logical System.public java.util.List<java.lang.StringBuilder> buildStringBuilderLineList(ProofWorksheet proofWorksheet) throws TheoremLoaderException
proofWorksheet
- ProofWorksheet objectTheoremLoaderException
- if the ProofWorksheet is null or is not
unified.