public class MMTFolder
extends java.lang.Object
Constructor and Description |
---|
MMTFolder()
Default constructor for MMTFolder.
|
MMTFolder(java.io.File file)
Constructor for MMTFolder using File object.
|
MMTFolder(java.io.File filePath,
java.lang.String mmtFolderName)
Constructor for MMTFolder using pathname String.
|
Modifier and Type | Method and Description |
---|---|
MMTTheoremSet |
constructMMTTheoremSet(LogicalSystem logicalSystem,
Messages messages,
TlPreferences tlPreferences)
Builds the MMTTheoremSet object for an MMTFolder using all the files in
the folder with file type ".mmt".
|
MMTTheoremSet |
constructMMTTheoremSet(java.lang.String theoremLabel,
LogicalSystem logicalSystem,
Messages messages,
TlPreferences tlPreferences)
Builds an MMTTheoremSet object for a single theorem in a file in the
MMTFolder.
|
java.lang.String |
getAbsolutePath()
Returns the absolute pathname of the MMTFolder.
|
java.io.File |
getFolderFile()
Returns the File object for the MMTFolder.
|
static Serializer<MMTFolder> |
serializer(SessionStore store) |
MMTTheoremFile |
storeMMTTheoremFile(java.lang.String theoremLabel,
java.util.List<java.lang.StringBuilder> mmtTheoremLines)
Stores a theorem in the MMTFolder as a MMT Theorem file.
|
public MMTFolder()
public MMTFolder(java.io.File filePath, java.lang.String mmtFolderName) throws TheoremLoaderException
filePath
- path for mmtFolderName. May be null or absolute or
relative path name.mmtFolderName
- String containing absolute or relative pathname.TheoremLoaderException
- if mmtFolderName is null, is blank,
doesn't exist, is not a directory, or if there is a
SecurityException.public MMTFolder(java.io.File file) throws TheoremLoaderException
file
- File object.TheoremLoaderException
- if input file is null, doesn't exist, is
not a directory, or if there is a SecurityException.public static Serializer<MMTFolder> serializer(SessionStore store)
public java.io.File getFolderFile()
public MMTTheoremSet constructMMTTheoremSet(LogicalSystem logicalSystem, Messages messages, TlPreferences tlPreferences) throws TheoremLoaderException
logicalSystem
- LogicalSystem object.messages
- Messages object.tlPreferences
- TlPreferences object.TheoremLoaderException
- if the MMTFolder File object is null or if
there is an I/O error reading the directory.public MMTTheoremSet constructMMTTheoremSet(java.lang.String theoremLabel, LogicalSystem logicalSystem, Messages messages, TlPreferences tlPreferences) throws TheoremLoaderException
theoremLabel
- Metamath label of the theorem to load into the
MMTTheoremSet.logicalSystem
- LogicalSystem object.messages
- Messages object.tlPreferences
- TlPreferences object.TheoremLoaderException
- if the MMTFolder File object is null or if
the theorem label is null or an empty string, or if the given
theorem is not a valid MMT Theorem file in the directory
(i.e. not found), or if there is a security exception.public MMTTheoremFile storeMMTTheoremFile(java.lang.String theoremLabel, java.util.List<java.lang.StringBuilder> mmtTheoremLines) throws TheoremLoaderException
Note: the input mmtTheoremLines List does not contain newline characters. Those are created by the program in a platform neutral manner.
theoremLabel
- Metamath label of the theorem to store into the
MMTTheoremSet.mmtTheoremLines
- List of StringBuilder objects with one line (no
newline!) per StringBuilder object, already formatted into
Metamath .mm format.TheoremLoaderException
- if the MMTFolder File object is null or if
the theorem label is null or an empty string, or if there is
an I/O error during the attempt to create an MMTTheoremFile.public java.lang.String getAbsolutePath()