Packages

package api

This is the main package of the MMT API.

It holds subpackages for all data structures, data containers, and the central algorithms and services.

Classes directly defined in the package

Some minor classes that are used throughout MMT are defined in this package, in particular:

  • MMT URIs in the class Path and Namespace
  • processing and content errors in the class Error

The package also contains root classes for certain types that are subclassed throughout the package. Most importantly:

  • StructuralElement: structure-level (= named) parts in the data structures for the MMT language: documents, theories, constants, ...
  • MMTTask: tasks for a single object: parsing, checking, ...
  • Rule: object-level part of the MMT language that is written in Scala

Subpackages

Data structures for the MMT language

The data structures for the MMT languages are defined in 4 packages corresponding to the 4 levels: - documents: Documents and all other NarrativeElements - modules: Modules (= the toplevel declarations), in particular Theorys and Views - symbols: all Declarations inside modules, in particular Constants - objects: all anonymous Objects (e.g., formulas, functions, etc.), in particular Contexts and Terms

The former 3 levels are jointly called 'structural' levels. All elements subclass StructuralElement, have an MMT URI, and carry an MMT URI referring to their parent in the MMT abstract syntax tree.

Structural elements are extensible (via DerivedModules and DerivedDeclarations), and the package patterns defines declaration patterns as a built-in extension.

All structural elements are mutable and implement the ContainerElement interface for changing their children. Objects, by contrast, are represented as immutable inductive types.(except for carrying metadata.Metadata and objects.ClientProperties). The boundary between structural elements and objects is mediated by ComponentContainers: these are mutable, owned by structural elements, and maintain objects.

A few auxiliary data structures shifted to separate packages: - opaque: external (i.e., informal, computation) content - informal: partially outdated informal data structures - metadata: metadata annotations to all structural elements or objects

The MMT main class and its internal state

The package frontend contains the class Controller, which owns all state relevant for running MMT. Typically, each application creates a single instance of this class. The package also defines several other essential classes, most importantly MMT's extension (=plug-in, add-on) interfaces via the Extension class.

The package libraries maintains the instances of MMT language data structures, in particular the Library class. Controller owns a Library, which stores all structural elements that have been loaded into memory.

User interfaces

The package frontend also contains the main executable classes, in particular the Shell class.

The package gui collects all classes for building graphical user interfaces. This includes auxiliary classes for use in IDE plugins.

The package web collects all classes for the HTTP interface of MMT.

Physical storage of the MMT language files

The package archives defines MMT Archives (= projects) as well as classes for building and working with archives. The latter include in particular the BuildManager and BuildTarget. Build targets include Importers and [Exporter]]s that translate between MMT and other formats.

The package backend defines classes for maintaining archives and translating between the MMT URIs of structural elements and their physical storage locations.

The central algorithms for processing MMT content

The processing model of MMT consists of several major algorithms. - parser: read strings into MMT data structures - checking: check and refine MMT data structures - uom: pure computation on MMT data structures - proving: theorem proving on MMT data structures (in very early state)) - execution: imperative computation (in very, very early state) - presentation: rendering MMT data structures in user-facing formats (including HTML+presentation MathML)

All algorithms are defined in Extensions coupled with default implementations. Moreover, all algorithms are split into two separate levels, one for structural elements and objects. See LeveledExtension.

The package notations maintains the common code for parsing and presentation.

The package valuebases maintains mathematical databases as a part of MMT.

Other algorithms on the MMT data structures

The package ontology contains a relational, semantic web-style ontology and query engine for it.

The package moc contains change management.

The package refactoring contains refactoring principles.

General purpose utility functions

The package utils defines general purpose APIs for files, URIs, HTML building, etc.

Source
package.scala
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. api
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. trait AbstractObjectContainer extends ComponentContainer
  2. trait AbstractTermContainer extends AbstractObjectContainer
  3. case class AddError(s: String) extends Error with Product with Serializable

    errors that occur when adding a knowledge item

  4. case class AddMessage(thy: Term, inFormat: String, decl: String) extends StructureMessage with Product with Serializable

    adding a declaration to a theory

    adding a declaration to a theory

    thy

    the theory to which the declaration is added

    inFormat

    the format used for interpreting the declaration (see checking.Interpreter)

    decl

    the declaration to add

  5. sealed abstract class AddPosition extends AnyRef

    see add methods of MutableElementContainer, Controller, Library

  6. case class After(name: LocalName) extends AddPosition with Product with Serializable
  7. case class BackendError(s: String, p: Path) extends Error with Product with Serializable

    errors that occur when the backend believes it should find an applicable resource but cannot

  8. case class Before(name: LocalName) extends AddPosition with Product with Serializable
  9. class BooleanClientProperty[-C <: ClientProperties] extends ClientProperty[C, Boolean]

    apply/unapply methods that encapsulate functionality for attaching a Boolean clientProperty to a Term

  10. class BooleanTermProperty extends BooleanClientProperty[Obj]
  11. case class CPath(parent: ComponentParent, component: ComponentKey) extends Path with Product with Serializable
  12. case class Checked(element: StructuralElement) extends MMTInterpretationProgress with Product with Serializable

    sent by structure checker after checking

  13. trait ClientProperties extends AnyRef

    a trait to be mixed into declarations or objects it provides a stateful key-value map for storing arbitrary information

    a trait to be mixed into declarations or objects it provides a stateful key-value map for storing arbitrary information

    This trait introduces state into the stateless Obj case classes and should be used cautiously. For example, x match {case x => x} preserves all client properties while x match {case OMS(p) => OMS(p)} deletes all client properties. Software components should only access properties they put themselves or that are explicitly guaranteed by other components.

    While a bad idea in most situations, client properties are very useful occasionally. Example applications:

    • UOM uses a property to remember whether a Term has been simplified already
    • UOM uses a property to remember what kind of change a simplification has produced
  14. class ClientProperty[-C <: ClientProperties, A] extends AnyRef

    convenience to create get and put methods for objects with ClientProperties

  15. case class ComplexStep(path: MPath) extends LNStep with Product with Serializable

    an include declaration; ComplexStep(fromPath) acts as the name of an unnamed structure

  16. trait ComponentContainer extends AnyRef

    A ComponentContainer holds the data keyed by a DeclarationComponent

  17. abstract class ComponentKey extends AnyRef

    A ComponentKey identifies a DeclarationComponent.

  18. sealed trait ComponentParent extends Path

    A path that is not a CPath (and thus may have a component)

  19. case class ConfigurationError(id: String) extends Error with Product with Serializable

    errors that occur when a configuration entry is missing

  20. trait ContainerElement[S <: StructuralElement] extends StructuralElement with MutableElementContainer[S]
  21. trait Content extends HasMetaData with ClientProperties

    The trait Content is mixed into any class that can be rendered.

  22. trait ContentElement extends StructuralElement

    A ContentElement is any knowledge item that is used to represent mathematical content.

    A ContentElement is any knowledge item that is used to represent mathematical content.

    These are the core MMT items such as modules, and symbols. This includes virtual knowledge items.

  23. trait ContentError extends AnyRef

    errors in user content

  24. sealed trait ContentPath extends Path with ComponentParent

    A path to a module or symbol

  25. case class DPath(uri: URI) extends Path with ComponentParent with SlashFunctions[DPath] with QuestionMarkFunctions[MPath] with Product with Serializable

    A DPath represents an MMT document level path.

    A DPath represents an MMT document level path.

    uri

    the URI of the document (may not contain query or fragment)

  26. case class DeclarationComponent(key: ComponentKey, value: ComponentContainer) extends NamedElement with Product with Serializable

    A component of a declaration, e.g., the type of a Constant (akin to XML attributes)

  27. trait DefaultLookup[S <: NamedElement] extends AnyRef
  28. trait DefaultMutability[S <: NamedElement] extends AnyRef

    straightforward update methods for classes that store their elements in a list-like variable

  29. case class DeleteError(s: String) extends Error with Product with Serializable

    errors that occur when deleting a knowledge item

  30. case class DeleteMessage(path: Path) extends StructureMessage with Product with Serializable

    adding a declaration to a theory

    adding a declaration to a theory

    path

    the URI of the declaration to delete

  31. case class Elaborated(element: StructuralElement) extends MMTInterpretationProgress with Product with Serializable

    sent by structure simplifier after simplifying

  32. case class ElaborationOf(source: ContentPath) extends Origin with Product with Serializable

    obtained by elaborating a declaration

  33. trait ElementContainer[+S <: NamedElement] extends AnyRef
  34. abstract class Error extends Exception

    The superclass of all Errors generated by MMT

  35. class ErrorContainer extends ErrorHandler

    stores errors in a list

  36. abstract class ErrorHandler extends AnyRef

    the type of continuation functions for error handling

    the type of continuation functions for error handling

    An ErrorHandler is passed in most situations in which a component (in particular archives.BuildTargets) might produce a non-fatal error.

  37. class ErrorLogger extends ErrorHandler

    reports errors

  38. case class ErrorResponse(message: String) extends Response with Product with Serializable
  39. class ErrorWriter extends OpenCloseHandler

    writes errors to a file in XML syntax

  40. case class EvaluateMessage(context: Option[Context], inFormat: String, in: String, outFormat: String) extends ObjectMessage with Product with Serializable

    exhaustively simplify a term in to a term out postcondition: thy |- in = out

  41. case class ExecutionError(msg: String) extends Error with Product with Serializable

    run time error thrown by executing invalid program

  42. abstract class ExtensionError extends Error

    base class for errors that are thrown by an extension

  43. class FilteringErrorHandler extends ErrorHandler

    Filters errors before passing them to the another error handler

  44. class FinalTermContainer extends AbstractTermContainer

    a dummy container for a stateless term

  45. case class GeneralError(s: String) extends Error with Product with Serializable

    other errors

  46. case class GeneratedBy(by: AnyRef) extends Origin with Product with Serializable

    generated by some agent

  47. case class GetError(s: String) extends Error with Product with Serializable

    errors that occur when retrieving a knowledge item

  48. case class GetMessage(path: Path, outFormat: String) extends StructureMessage with Product with Serializable

    adding a declaration to a theory

    adding a declaration to a theory

    path

    the URI of the declaration to retrieve

    outFormat

    the format used for presenting the declaration (see presentation.Presenter)

  49. case class GlobalName(module: MPath, name: LocalName) extends Path with ContentPath with SlashFunctions[GlobalName] with Product with Serializable

    A GlobalName represents the MMT URI of a symbol-level declaration.

    A GlobalName represents the MMT URI of a symbol-level declaration. This includes induced declarations.

  50. case class HeaderInfo(feature: String, path: Path, attributes: List[Any]) extends Product with Serializable

    all information that defines the nature of this element a change to this information is so fundamental that it should be treated like a delete-add, not an update event

  51. case class HeapLookupError(name: LocalName) extends Error with Product with Serializable
  52. case class ImplementationError(s: String) extends Error with Product with Serializable

    errors that are not supposed to occur, e.g., when input violates the precondition of a method

  53. case class InferMessage(context: Option[Context], inFormat: String, in: String, outFormat: String) extends ObjectMessage with Product with Serializable

    infer the type of a given term postcondition: thy |- in : out

  54. abstract class Invalid extends Error with ContentError

    errors that occur when checking a knowledge item (generated by the Checker classes)

  55. case class InvalidElement(elem: StructuralElement, s: String) extends Invalid with ContentError with Product with Serializable

    errors that occur when structural elements are invalid

  56. case class InvalidObject(obj: Obj, s: String) extends Invalid with Product with Serializable

    errors that occur when objects are invalid

  57. case class InvalidUnit(unit: CheckingUnit, history: History, msg: String) extends Invalid with Product with Serializable

    errors that occur when judgements do not hold

  58. abstract class LNStep extends AnyRef

    a step in a LocalName

  59. class ListContainer[S <: NamedElement] extends ElementContainer[S] with DefaultLookup[S]
  60. case class LocalName(steps: List[LNStep]) extends SlashFunctions[LocalName] with Product with Serializable

    A LocalName represents a local MMT symbol-level declarations (relative to a module).

    A LocalName represents a local MMT symbol-level declarations (relative to a module).

    steps

    the list of (in MMT: slash-separated) components

  61. case class LocalRef(segments: List[String], absolute: Boolean) extends Product with Serializable

    A LocalRef represents a possibly relative LocalName

    A LocalRef represents a possibly relative LocalName

    segments

    the list of (slash-separated) components

    absolute

    a flag whether the reference is absolute (i.e., starts with a slash)

  62. case class LookupError(name: LocalName, context: Context) extends Error with Product with Serializable
  63. trait MMTInterpretationProgress extends MMTTaskProgress
  64. trait MMTTask extends Killable

    killing a task signals that all processing of the task should be stopped

  65. trait MMTTaskProgress extends AnyRef

    parent of all messages indicating progress when carrying out an MMTTask

  66. abstract class MMTTaskProgressListener extends AnyRef

    see MMTTask

  67. case class MPath(parent: DPath, name: LocalName) extends Path with ContentPath with SlashFunctions[MPath] with QuestionMarkFunctions[GlobalName] with Product with Serializable

    An MPath represents an MMT module level path.

    An MPath represents an MMT module level path.

    parent

    the path of the parent document

    name

    the name of the module

  68. case class Materialized(from: Term) extends Origin with Product with Serializable

    materialized module

  69. sealed abstract class Message extends AnyRef

    messages define the abstract syntax of a protocol for communicating between content processing systems

    messages define the abstract syntax of a protocol for communicating between content processing systems

    The classes use string arguments (as opposed to Declaration and Term) together with format strings.

    It exposes the main content-related commands that can be sent to MMT. In particular, messages can be passed to MMT via HTTP using web.MessageHandler

  70. class MultipleErrorHandler extends OpenCloseHandler

    combines the actions of multiple handlers

  71. trait MutableElementContainer[S <: NamedElement] extends ElementContainer[S]
  72. class MutableRuleSet extends RuleSet

    standard implementation of using set of rules hashed by their head

  73. trait NamedElement extends AnyRef
  74. case class NamespaceMap(base: Path, prefixes: List[(String, URI)] = Nil) extends Product with Serializable
  75. trait NarrativeElement extends StructuralElement

    A NarrativeElement is any OMDoc element that is used to represent narration and document structure.

    A NarrativeElement is any OMDoc element that is used to represent narration and document structure.

    These include documents and cross-references.

  76. abstract class NotationComponentKey extends ComponentKey

    components that are notations

  77. abstract class ObjComponentKey extends ComponentKey

    components that are MMT objects

  78. sealed abstract class ObjectMessage extends Message

    messages that call algorithms on MMT objects they may create state changes only indirectly by recording the result of the algorithm in the current theory

  79. case class ObjectResponse(result: String, tp: String) extends Response with Product with Serializable
  80. abstract class OpenCloseHandler extends ErrorHandler

    an error handler that needs opening and closing

  81. abstract class Origin extends AnyRef

    describes the origin of a generated knowledge item

  82. case class OtherComponent(s: String) extends ComponentKey with Product with Serializable

    custom component, e.g., in a info.kwarc.mmt.api.symbols.DerivedDeclaration

  83. abstract class ParametricRule extends SemanticObject

    parametric rules can be instantiated to obtain rules

  84. case class ParseError(s: String) extends Error with Product with Serializable

    other errors that occur during parsing

  85. case class Parsed(element: StructuralElement) extends MMTInterpretationProgress with Product with Serializable

    sent by structure parsers after parsing

  86. sealed abstract class Path extends BaseType

    A Path represents an MMT path.

    A Path represents an MMT path.

    An MMT path refers to a document (doc), a module (doc?mod), or a symbol (M % sym). Use the objects ?, %, /, \, and ! for pattern matching paths.

  87. case class PresentationError(s: String) extends Error with Product with Serializable

    errors that occur when presenting a knowledge item

  88. case class ProveMessage(context: Option[Context], inFormat: String, in: String, outFormat: String) extends ObjectMessage with Product with Serializable

    find a term of a given type postcondition: thy |- out : in

  89. trait QuestionMarkFunctions[A] extends AnyRef

    auxiliary trait to mixin convenience methods into Path classes

  90. case class RegistrationError(s: String) extends Error with Product with Serializable

    errors that occur when registering extensions

  91. class RepeatedAdd extends AnyRef

    helper class for creating a sequence of AddPosition's where each is right after the previous one

  92. sealed abstract class Response extends AnyRef

    type of responses for a Message

  93. trait Rule extends SemanticObject

    the type of all Rules

    the type of all Rules

    All Rules have an apply method that is passed a Solver for callbacks. The Solver does not implement any back-tracking. Therefore, rules may only use callbacks if their effects are required.

  94. abstract class RuleSet extends Rule

    A RuleSet groups some Rule's.

  95. trait SemanticObject extends AnyRef

    superclass for all semantic objects, i.e., objects that live in the semantic domain provided Scala

  96. case class SimpleStep(name: String) extends LNStep with Product with Serializable

    constant or structure declaration

  97. trait SlashFunctions[A] extends AnyRef

    auxiliary trait to mixin convenience methods into Path classes

  98. case class SourceError(origin: String, ref: SourceRef, mainMessage: String, extraMessages: List[String] = Nil, level: Level.Level = Level.Error) extends Error with ContentError with Product with Serializable

    errors that occur when parsing a knowledge item

  99. trait StructuralElement extends Content with NamedElement

    A StructuralElement is any knowledge item on the document, module, or symbol level.

    A StructuralElement is any knowledge item on the document, module, or symbol level.

    The structural elements are subdivided according to their dimension: content, presentation, or narration.

  100. sealed abstract class StructureMessage extends Message

    messages that result in structural changes to theories and are thus stateful

  101. case class StructureResponse(id: String) extends Response with Product with Serializable
  102. case class SubstitutionUndefined(name: LocalName, m: String) extends Error with Product with Serializable

    errors that occur during substitution with name of the variable for which the substitution is defined

  103. trait SyntaxDrivenRule extends Rule

    a rule for syntax-driven algorithms, applicable to expressions with a certain head

  104. abstract class TermComponentKey extends ObjComponentKey

    components that are MMT terms

  105. class TermProperty[A] extends ClientProperty[Obj, A]
  106. case class UpdateError(s: String) extends Error with Product with Serializable

    errors that occur when updating a knowledge item

  107. case class UpdateMessage(thy: Term, inFormat: String, decl: String) extends StructureMessage with Product with Serializable

    adding a declaration to a theory

    adding a declaration to a theory

    thy

    the theory to which the declaration is added

    inFormat

    the format in which the declaration is given

    decl

    the new declaration (replaces the declaration given by its URI)

Value Members

  1. object !

    This permits the syntax !(n) in patterns to match atomic local names.

  2. object /

    This permits the syntax head / tail in patterns.

  3. object ?

    This permits the syntax doc ? mod in patterns.

  4. object ??

    This permits the syntax mod ?? name in patterns.

  5. object AtBegin extends AddPosition with Product with Serializable
  6. object AtEnd extends AddPosition with Product with Serializable
  7. object CompilerError

    errors that occur during compiling

  8. object ComponentKey
  9. object DefComponent extends TermComponentKey with Product with Serializable

    definiens of symbols.Constant, DefinedTheory, DefinedView, DefinedStructure

  10. object DefaultAssignment extends Origin with Product with Serializable

    generated by lookup in partial links

  11. object ElaborationOfDefinition extends Origin with Product with Serializable

    obtained by elaborating the definition of a module

  12. object Error extends Serializable
  13. object ErrorThrower extends ErrorHandler

    throws errors

  14. object GeneratedMRef extends Origin with Product with Serializable

    MRef left when taking a theory out of a document

  15. object LNStep
  16. object Level

    error levels, see Error

    error levels, see Error

    even fatal errors can be ignored (by comparison)

  17. object LocalName extends Serializable
  18. object LocalRef extends Serializable
  19. object MMTTask
  20. object MetaDataComponent extends ComponentKey with Product with Serializable
  21. object NamespaceMap extends Serializable
  22. object NotationComponent
  23. object Original extends Origin with Product with Serializable

    an original declaration

  24. object ParsingNotationComponent extends NotationComponentKey with Product with Serializable

    (text-based) parsing notation of a symbol

  25. object Path

    helper object for paths

  26. object PatternBodyComponent extends ComponentKey with Product with Serializable
  27. object PresentationNotationComponent extends NotationComponentKey with Product with Serializable

    (two-dimensional, MathML-like) presentation notation of a symbol

  28. object Rule
  29. object RuleSet
  30. object SemanticObject
  31. object Stacktrace

    auxiliary functions for handling Java stack traces

  32. object TermComponent
  33. object TermProperty
  34. object TypeComponent extends TermComponentKey with Product with Serializable

    type of a symbols.Constant

  35. object VerbalizationNotationComponent extends NotationComponentKey with Product with Serializable

    (narrative) verbalization notation of a symbol

  36. object \

    This permits the syntax init \ last in patterns.

Deprecated Value Members

  1. object CodComponent extends TermComponentKey with Product with Serializable

    codomain of a modules.Link

    codomain of a modules.Link

    Annotations
    @MMT_TODO( message = "replace with TypeComponent" )
    Deprecated

    replace with TypeComponent

  2. object DomComponent extends TermComponentKey with Product with Serializable

    domain of a modules.Link, meta-theory of a theory

    domain of a modules.Link, meta-theory of a theory

    Annotations
    @MMT_TODO( message = "replace with TypeComponent" )
    Deprecated

    replace with TypeComponent

  3. object ParamsComponent extends ObjComponentKey with Product with Serializable

    parameters

    parameters

    Annotations
    @MMT_TODO( message = "replace with TypeComponent" )
    Deprecated

    replace with TypeComponent

Inherited from AnyRef

Inherited from Any

Ungrouped