class Library extends Lookup with Logger
A Library is the in-memory representation of an MMT diagram, including the implicit-diagram, and all root documents.
It implements the lookup and change of MMT URIs via get/add/update/delete/reorder methods.
Invariant: This class guarantees structural well-formedness in the sense that libraries conform to the MMT grammar and all declarations have canonical URIs. The well-formedness of the objects in the declarations is not guaranteed.
The Controller own a library and uses it to load elements into memory dynamically. Therefore, access should always be through the corresponding methods of the controller. Elements are unloaded dynamically if MMT runs out of memory.
- Self Type
- Library
- Source
- Library.scala
- Alphabetic
- By Inheritance
- Library
- Logger
- Lookup
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
-
new
Library(extman: ExtensionManager, report: Report, previous: Option[Library])
- extman
the controller's extension manager
- report
parameter for logging.
- previous
a second library that stores the previous version whenever an element is changed
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
add(e: StructuralElement, at: AddPosition = AtEnd): Unit
adds a declaration
adds a declaration
- e
the added declaration
-
def
apply(path: ContentPath): StructuralElement
- Definition Classes
- Lookup
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
val
asLocalLookup: LookupWithNotFoundHandler with FailingNotFoundHandler
same as this but GetError instead of NotFound
-
def
clear: Unit
forgets everything
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
- def deactivate(se: StructuralElement): Unit
-
def
delete(path: Path): Unit
deletes the element with the given URI
deletes the element with the given URI
- path
the path to the element to be deleted
-
def
endAdd(c: ContainerElement[_]): Unit
add-related work that has to be done at the end of an element in particular: implicit morphisms are registered only when the inducing element has been checked
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
def
forDeclarationsInScope(mod: Term)(f: (MPath, Term, Declaration) ⇒ Unit): Unit
all declarations that are visible (based on what is currently loaded) to a theory replaced with forDeclarationsInScope
-
def
get(home: Term, name: LocalName, error: (String) ⇒ Nothing): Declaration
retrieval in a module expression
-
def
get(p: Path): StructuralElement
top level retrieval method
-
def
getAllPaths: Iterable[MPath]
returns all module paths indexed by this library
-
def
getAs[E <: ContentElement](cls: Class[E], home: Term, name: LocalName, error: (String) ⇒ Nothing): E
like get but with restricted return type
like get but with restricted return type
- Definition Classes
- Lookup
-
def
getAs[E <: StructuralElement](cls: Class[E], path: Path): E
like get but with restricted return type example: getAs(classOf[Constant], path): Constant
like get but with restricted return type example: getAs(classOf[Constant], path): Constant
- Definition Classes
- Lookup
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getComponent(path: CPath): ComponentContainer
- Definition Classes
- Lookup
-
def
getConstant(path: GlobalName, msg: (Path) ⇒ String = defmsg): Constant
- Definition Classes
- Lookup
-
def
getDomain(a: Declaration): (AbstractTheory, Option[Link])
gets the domain in which a Declaration was declared
gets the domain in which a Declaration was declared
This can be used to retrieve the source of an assignment declared in a DeclaredLink. It is also the official way to test whether a Constant is an assignment.
- a
the Constant declaration/assignment
- returns
if assignment: the source theory and the containing link; if declaration: the containing theory
- Definition Classes
- Lookup
-
def
getImplicit(from: Term, to: Term): Option[Term]
retrieve the implicit morphism "from --implicit--> to"
-
def
getImplicit(from: MPath, to: MPath): Option[Term]
- Definition Classes
- Lookup
-
def
getLink(path: ContentPath, msg: (Path) ⇒ String = defmsg): Link
- Definition Classes
- Lookup
-
def
getModule(path: MPath): Module
important special case
important special case
- Definition Classes
- Lookup
-
def
getModules: Iterable[Module]
retrieves all modules in any order
-
def
getO(home: Term, name: LocalName): Option[Declaration]
like get but returns optional
like get but returns optional
- Definition Classes
- Lookup
-
def
getO(path: Path): Option[StructuralElement]
like get, but returns option
like get, but returns option
- Definition Classes
- Lookup
-
def
getParent(d: Declaration): ModuleOrLink
returns the container element that contains a declarations
returns the container element that contains a declarations
- Definition Classes
- Lookup
-
def
getStructure(path: GlobalName, msg: (Path) ⇒ String = defmsg): Structure
- Definition Classes
- Lookup
-
def
getSymbol(path: GlobalName, msg: (Path) ⇒ String = defmsg): Declaration
- Definition Classes
- Lookup
-
def
getTheory(path: MPath, msg: (Path) ⇒ String = defmsg): Theory
- Definition Classes
- Lookup
-
def
getView(path: MPath, msg: (Path) ⇒ String = defmsg): View
- Definition Classes
- Lookup
-
def
hasImplicit(from: Term, to: Term): Boolean
- Definition Classes
- Lookup
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
log(e: Error): Unit
logs an error - always logged
logs an error - always logged
- Attributes
- protected
- Definition Classes
- Logger
-
def
log(s: ⇒ String, subgroup: Option[String] = None): Unit
logs a message with this logger's logprefix
logs a message with this logger's logprefix
- Attributes
- protected
- Definition Classes
- Logger
-
def
logError(s: ⇒ String): Unit
log as an error message
log as an error message
- Attributes
- protected
- Definition Classes
- Logger
-
def
logGroup[A](a: ⇒ A): A
wraps around a group to create nested logging
wraps around a group to create nested logging
- Attributes
- protected
- Definition Classes
- Logger
- val logPrefix: String
-
def
logTemp(s: ⇒ String): Unit
temporary logging - always logged
temporary logging - always logged
- Attributes
- protected
- Definition Classes
- Logger
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
notifyUpdated(p: CPath): Unit
marks all known dependent components as dirty
marks all known dependent components as dirty
This method is public because components may be changed from the outside. In that case, this method may be called additionally to maintain invariants.
When deleting a Symbol or Component, this is called automatically.
- p
path to the component that was changed/deleted
-
def
preImage(p: GlobalName): Option[GlobalName]
returns the symbol from which the argument symbol arose by a structure declaration
-
def
quasiAliasFor(c: GlobalName): List[GlobalName]
all constants for which c is a quasi-alias (recursively) a quasi-alias is defined by a definition c = OMS(d)
all constants for which c is a quasi-alias (recursively) a quasi-alias is defined by a definition c = OMS(d)
- Definition Classes
- Lookup
- def reactivate(se: StructuralElement): Unit
-
def
reorder(p: Path): Unit
moves an element with a given path to the end of its parent document
- val report: Report
-
def
resolveName(parents: List[MPath], name: LocalName): List[GlobalName]
resolves a name in a list of theories using any included theory, possibly inserting include steps
resolves a name in a list of theories using any included theory, possibly inserting include steps
- Definition Classes
- Lookup
-
def
resolveRealizedName(parent: ModuleOrLink, name: LocalName): List[GlobalName]
resolves a name in a module using any included or realized theories
resolves a name in a module using any included or realized theories
- Definition Classes
- Lookup
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- Library → AnyRef → Any
-
def
update(e: StructuralElement): Unit
updates a StructuralElement
-
def
visible(to: Term): Iterable[MPath]
as visibleVia but dropping the implicit morphisms
-
def
visibleDirect(to: Term): List[MPath]
as visible but only those where the morphism is trivial (i.e., all includes)
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
object
ApplyMorphs extends Traverser[Term]
A Traverser that recursively eliminates all explicit morphism applications.
A Traverser that recursively eliminates all explicit morphism applications. apply(t,m) can be used to apply a morphism to a term.
- Definition Classes
- Lookup
-
object
ExpandDefinitions extends Traverser[(ContentPath) ⇒ Boolean]
A Traverser that recursively expands definitions of Constants.
A Traverser that recursively expands definitions of Constants. It carries along a test function that is used to determine when a constant should be expanded.
- Definition Classes
- Lookup