package backend
This package maintains the interface between MMT content in persistent physical storage and MMT content loaded into memory.
The class Storage is the interface for individual physical storage containers. Most of the time this corresponds to a folder containing an archives.Archive.
Content is usually stored in OMDoc XML format, which is parsed by the XMLStreamer.
The class Backend maintains the registered storages and performs conversion between logical MMT URIs and physical locations.
The frontend.Controller owns an instance of Backend. Any referenced MMT URI is lazily and transparently loaded from the backend into memory and unloaded if MMT runs out of memory.
- Source
- package.scala
- Alphabetic
- By Inheritance
- backend
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
abstract
class
ArchiveCustomization extends AnyRef
Helper class to permit customizing archives
-
class
ArchiveNarrationStorage extends LocalCopy
Ï like LocalCopy but optimized for Archives
Ï like LocalCopy but optimized for Archives
custom HTML snippets are spliced into folder-documents
-
class
Backend extends Logger
the backend of a Controller
the backend of a Controller
holds a list of Storages and uses them to dereference MMT URIs,
- class DefaultCustomization extends ArchiveCustomization
-
class
LocalCopy extends Storage
a Storage that retrieves repository URIs from the local working copy
-
case class
LocalSystem(base: URI) extends Storage with Product with Serializable
a Storage that retrieves file URIs from the local system
-
class
MML extends ArchiveCustomization
Customization for Mizar
- case class NotApplicable(message: String = "") extends Error with Product with Serializable
- trait QueryTransformer extends FormatBasedExtension
-
class
RealizationArchive extends Storage with RealizationStorage
loads a realization from a Java Class Loader and dynamically creates a uom.RealizationInScala for it
-
trait
RealizationStorage extends AnyRef
a variant of a Storage that loads Scala objects from the class path
-
class
SourceFromReader extends Source
an awkward conversion from java.io.Reader to scala.io.Source needed in XMLStreamer because ParsingStream uses the former, but ConstructingParser the latter
-
abstract
class
Storage extends AnyRef
An abstraction over physical storage units that hold MMT content
-
class
TPTP extends ArchiveCustomization
TPTP customization
-
class
XMLReader extends Logger
A Reader parses XML/MMT and calls controller.add(e) on every found content element e
A Reader parses XML/MMT and calls controller.add(e) on every found content element e
The XML may contain CURIEs. However, all namespace prefixes must be declared on the toplevel omdoc element; other bindings are ignored.
-
class
XMLStreamer extends Parser
The parser for OMDoc XML.
The parser for OMDoc XML.
This class is in charge of streaming XML. To do so, it wraps around XMLReader, which does the actual parsing of XML elements into MMT data structures.
Value Members
-
object
DefaultRealizationLoader extends Storage with RealizationStorage
loads a rule from the default classpath
- object ReadXML
- object TrivialQueryTransformer extends QueryTransformer
-
object
XMLObjectParser extends ObjectParser
a straightforward ObjectParser that relegates to Obj.parse