package frontend
This package defines several central classes: - Controller is the main MMT class. - Shell is the main executable (which will create one controller). - MMTConfig is the MMT configuration data structure. A controller maintains one configuration. - Extension is the addon/plugin interface of MMT. Every extension has access to one controller instance. - Report handles logging, and every instance of Logger has access to a report instance.
- Source
- package.scala
- Alphabetic
- By Inheritance
- frontend
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
case class
ArchiveConf(id: String, formats: List[String], readonly: Boolean) extends BackendConf with Product with Serializable
registers an archive with its formats and a flag of whether it is readonly (pregenerated) or should be built
- abstract class BackendConf extends ConfEntry
-
trait
ChangeListener extends Extension
A ChangeListener is an Extension that is called on every Constant
-
case class
Closure(p: Path) extends MakeAbstract with Product with Serializable
retrieves the closure of a knowledge item
-
case class
Component(p: Path, comp: ComponentKey) extends MakeAbstract with Product with Serializable
retrieves a component of a knowledge item
-
abstract
class
ConfEntry extends AnyRef
an entry in an MMT configuration file (see MMTConfig)
-
class
Controller extends ROController with ActionHandling with Logger
A Controller is the central class maintaining all MMT content and extensions.
A Controller is the central class maintaining all MMT content and extensions.
Every application (e.g., Shell) typically creates one controller. The controller creates and owns one instance of many MMT clasess (see the documentation of the respective fields below).
It also maintains the MMTConfig and exectures Actions.
-
class
ControllerState extends AnyRef
minor variables kept by the controller, usually modifiable via actions
-
case class
DatabaseConf(url: URI, uri: URI) extends BackendConf with Product with Serializable
registers a remote database
-
case class
Deps(path: Path) extends MakeConcrete with Product with Serializable
retrieves all relational elements about a certain path and renders them as XML
-
case class
Elaboration(p: Path) extends MakeAbstract with Product with Serializable
retrieves the elaboration of an instance
-
case class
EnvVarConf(id: String, value: String) extends ConfEntry with Product with Serializable
sets an MMT-specific environment variable
- trait Extension extends Logger
-
case class
ExtensionConf(key: String, cls: String, args: List[String]) extends ConfEntry with Product with Serializable
registers BuildTargets with their arguments
registers BuildTargets with their arguments
- key
the key of the target
- cls
the qualified Java class name of this target's implementation (must only be on the class path if this target is actually used)
- args
the arguments to be used if this target is instantiated
-
class
ExtensionManager extends Logger
An ExtensionManager maintains all language-specific extensions of MMT.
An ExtensionManager maintains all language-specific extensions of MMT. This includes Compilers, QueryTransformers, and Foundations. They are provided as plugins and registered via their qualified class name, which is instantiated by reflection.
-
abstract
class
FileHandler extends ReportHandler
common methods for logging to a file
-
class
FileServerHere extends ShellExtension
example shell extension that starts a static HTTP server serving the current directory
-
case class
ForeignConf(section: String, key: String, values: List[String]) extends ConfEntry with Product with Serializable
ignored by MMT but available to plugins
-
trait
FormatBasedExtension extends Extension
extensions classes that can be tested for applicability based on a format string
-
case class
FormatConf(id: String, importers: List[String], exporters: List[String]) extends ConfEntry with Product with Serializable
defines an archive format
defines an archive format
- id
the format name
- importers
the importers to be used for archives of this format
- exporters
the exporters to be used for archives of this format
-
case class
Get(p: Path) extends MakeAbstract with Product with Serializable
retrieves a knowledge item
-
class
HtmlFileHandler extends FileHandler
outputs to a file in html syntax
- class InteractiveSimplifier extends AnyRef
-
case class
LMHConf(local: File, https: Boolean, remote: Option[URI]) extends BackendConf with Product with Serializable
registers a set of LMH working copies
-
trait
LeveledExtension extends Extension
Common super class of all extensions, whose functionality is systematically split between structure and object level
Common super class of all extensions, whose functionality is systematically split between structure and object level
Implementing classes should have a constructor that takes an Extension providing the object level functionality and add the structure level functionality.
-
trait
Logger extends AnyRef
extended by all classes that use the logging aspect
-
class
MMTConfig extends AnyRef
an MMT configuration stores catalogs for finding extensions, archives, etc.
an MMT configuration stores catalogs for finding extensions, archives, etc. It is a list of ConfEntry that can be read from a .cfg file
-
class
MMTILoop extends ILoop
a wrapper around the interactive Scala interpreter
-
class
MMTInterpolator extends AnyRef
provides convenience methods to be used in an interactive Scala interpreter session
provides convenience methods to be used in an interactive Scala interpreter session
usage: val ip = new MMTInterpolator(controller); import i.MMTContext
-
abstract
class
MMTScript extends Extension
parent class for classes generated from .mbt
parent class for classes generated from .mbt
all methods defined in this class can be used inside .mbt scripts
-
class
MMTScriptEngine extends AnyRef
executes a file as an MMTScript by calling Scala reflection
-
class
Make extends ShellExtension
a make-like shell extension that calls a build target on a file/folder in an archive
-
abstract
class
MakeAbstract extends AnyRef
represent retrieval operations that return content elements
represent retrieval operations that return content elements
These objects become Action commands by wrapping them in post-processing steps. see the children of MakePresentation
-
abstract
class
MakeConcrete extends AnyRef
represents the first post-processing phase
represents the first post-processing phase
These produce concrete syntax from the abstract syntax.
-
case class
MathPathConf(local: File) extends BackendConf with Product with Serializable
registers a folder on which to find archives
-
class
Memory extends ROMemory
Groups all stateful objects of the controller that store MMT data
-
case class
NamespaceConf(id: String, uri: URI) extends ConfEntry with Product with Serializable
declares an abbreviation (CURIE-style namespace prefix) for a URI
-
case class
NotFound(path: Path, found: Option[Path] = None) extends Throwable with Product with Serializable
An exception that is thrown when a needed knowledge item is not available
An exception that is thrown when a needed knowledge item is not available
A Controller catches it and retrieves the item dynamically.
- path
the URI of the not-found element
- found
a parent URI that has been loaded
-
class
Notify extends AnyRef
Convenience class to notify a set of ChangeListeners
-
abstract
class
Output extends AnyRef
represents the final post-processing phase, which outputs concrete syntax
-
case class
Present(c: MakeAbstract, param: String) extends MakeConcrete with Product with Serializable
takes a content element and renders it using notations
-
case class
Print(pres: MakeConcrete) extends Output with Product with Serializable
prints to STDOUT
-
case class
ProfileConf(id: String, archives: List[String]) extends BackendConf with Product with Serializable
Registers a profile as a subset of active archives
-
trait
REPLExtension extends Extension
An extension that provides REPL functionality to MMT.
-
abstract
class
ROController extends AnyRef
An interface to a controller containing read-only methods.
-
abstract
class
ROMemory extends AnyRef
A read-only abstraction of memory
-
class
RecordingHandler extends ReportHandler
remembers logged lines
-
class
Report extends Logger
Instances of Report handle all output to the user
-
abstract
class
ReportHandler extends AnyRef
takes a log message from Report and displays/stores etc.
takes a log message from Report and displays/stores etc. it
-
case class
Respond(pres: MakeConcrete) extends Output with Product with Serializable
produces the result and throws it away
produces the result and throws it away
call get to keep it in memory and retrieve it
-
case class
SemanticsConf(theory: MPath, cls: String, args: List[String]) extends ConfEntry with Product with Serializable
registers an extension providing opaque semantics for a theory
registers an extension providing opaque semantics for a theory
- theory
the theory
- cls
the implementing extension
-
class
Shell extends StandardIOHelper
Creates a Controller and provides a shell interface to it.
Creates a Controller and provides a shell interface to it.
The command syntax is given by the Action class and the parser in its companion object.
-
case class
ShellArguments(help: Boolean, about: Boolean, mmtFiles: List[String], scalaFiles: List[String], cfgFiles: List[String], commands: List[String], shell: Boolean, noshell: Boolean, keepalive: Boolean, useQueue: Boolean, verbosity: Int) extends Product with Serializable
Represents arguments passed to MMT on the command line.
Represents arguments passed to MMT on the command line.
- help
Should we print a help text
- about
Should we print an about text
- mmtFiles
List of MMT files to load
- scalaFiles
List of Scala files to load
- cfgFiles
List of config files to load
- commands
List of commands to run
- shell
interactive mode requested (show shell, terminate manually)
- noshell
batch mode unrequested (no shell, terminate immediately)
- keepalive
server mode requested (after shell (if at all) terminate only when processes finished)
- verbosity
<0: no output, >=0: console output, >10: console output including debug
-
class
ShellSendCommand extends ShellExtension
pass on arguments to an MMT server instance and terminate
-
trait
StandardIOHelper extends AnyRef
mixes in helper functions for interactive shells
-
class
StandardREPL extends REPLExtension
The standard, bare-bones implementation of the REPL
-
class
StructureTrffaverser extends AnyRef
This class can be used to conveniently apply the same operation to all terms in a structural element
-
class
TextFileHandler extends FileHandler
outputs to a file
-
case class
ToFile(pres: MakeConcrete, file: File) extends Output with Product with Serializable
writes to a file
-
case class
ToWindow(pres: MakeConcrete, window: String) extends Output with Product with Serializable
displays content in a window
-
abstract
class
Plugin extends Extension
extensions that provide semantics for MMT theories
extensions that provide semantics for MMT theories
- Annotations
- @MMT_TODO( message = ... )
- Deprecated
contents of plugins should become rules, registered build targets (which are loaded on demand) or content-generating operators that are declared in theories
-
abstract
class
ShellExtension extends FormatBasedExtension
used to add a new command line application to MMT
used to add a new command line application to MMT
ShellExtensions are looked for after all configurations are loaded. These must contain the corresponding ExtensionConf entry so that MMT can find a ShellExtension.
- Annotations
- @MMT_TODO( message = "use ActionCompanion instead" )
- Deprecated
use ActionCompanion instead
Value Members
-
object
ConsoleHandler extends ReportHandler
outputs to standard output
- object Controller
-
object
MMTConfig
helper functions for configurations
- object Report
-
object
Run extends Shell
A shell, the default way to run MMT as an application
- object Shell
- object ShellArguments extends Serializable