package opaque
Informal or unknown content that MMT does not process. The main classes are - OpaqueElement: such content - OpaqueElementInterpreter the abstract interface for extensions that interpret it
- Source
- package.scala
- Alphabetic
- By Inheritance
- opaque
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
class
DefaultOpaqueElementInterpreter extends OpaqueElementInterpreter with OpaqueTextParser with OpaqueChecker with OpaqueHTMLPresenter with OpaqueTextPresenter
a fallback/default parser for completely unknown elements
-
class
HTMLInterpreter extends OpaqueElementInterpreter with OpaqueChecker with OpaqueHTMLPresenter
MMT objects are read from <script type="mmt">OBJ</script> tags in XHTML
MMT objects are read from <script type="mmt">OBJ</script> tags in XHTML
very rough proof of concept, should be refined a lot
-
class
ObjFragment extends TextFragment
a fragment containing a formal object
-
trait
OpaqueChecker extends OpaqueElementInterpreter
used to extend the StructureCheckers
-
case class
OpaqueContext(decls: List[ObjFragment]) extends ListWrapper[ObjFragment, OpaqueContext] with Product with Serializable
a list object fragments representing declarations, innermost first
-
abstract
class
OpaqueElement extends NarrativeElement
any element that MMT does not (fully) understand
any element that MMT does not (fully) understand
Extensions of MMT with Opaque knowledge consists of a pair of a subclass C of this class and an implementation of OpaqueElementInterpreter[C]
-
abstract
class
OpaqueElementInterpreter extends FormatBasedExtension
an extension that provides (parts of) the meaning of OpaqueElements
an extension that provides (parts of) the meaning of OpaqueElements
Instances of this class must be coupled with a subclass OE <: OpaqueElement. Methods of an OpaqueElementInterpreter will be passed to and must return only instances of OE, never of other OpaqueElements.
OE is not a type parameter of OpaqueElementInterpreter because that is less helpful than one may think. Interpreters are anyway chosen at run time based on the format so that the type information can rarely be exploited and often requires casting anyway.
Therefore, all methods work simply with OpaqueElement. But MMT and all oi:OpaqueElementInterpreter must respect the following invariant: If oe:OpaqueElement and oi.isApplicable(oe.format), then oe.isInstanceOf[oi.OE]. In particular, the 'downcast' method can be used to refine the type of inputs passed to this class.
-
trait
OpaqueHTMLPresenter extends OpaqueElementInterpreter
used to extend HTMLPresenters
-
class
OpaqueText extends OpaqueElement
opaque contents using flat text structure intermixed with Objects
opaque contents using flat text structure intermixed with Objects
string representation: {...} for variable scopes, $...$ for MMT objects XML representation: <scope> for variable scopes, <OMOBJ> or <unparsed> for MMT objects
-
trait
OpaqueTextParser extends OpaqueElementInterpreter
used to extend StructureParsers
-
trait
OpaqueTextPresenter extends OpaqueElementInterpreter
used to extend MMTStructurePresenters
-
class
OpaqueXML extends OpaqueElement
Opaque content stored in an XML-tree structure with intermixed with Objects
Opaque content stored in an XML-tree structure with intermixed with Objects
MMT objects O are stored in 'node' using pointer <mmt index="i"/> where i is the index of O in 'terms'.
-
case class
ScopeFragment(body: List[TextFragment]) extends TextFragment with Product with Serializable
introduces a variable scope
introduces a variable scope
Scoping rules: An ObjFragment f has access to all declaring ObjFragment's in - proper ancestor scopes - the current scope if they precede f in the following order: declaring left-to-right, then non-declaring left-to-right
-
case class
StringFragment(value: String) extends TextFragment with Product with Serializable
a fragment holding any string
- case class TermFragmentInXML(index: Int, format: String, tc: TermContainer) extends Product with Serializable
-
abstract
class
TextFragment extends AnyRef
see OpaqueText
- class TextInterpreter extends OpaqueElementInterpreter with OpaqueTextParser with OpaqueChecker with OpaqueTextPresenter with OpaqueHTMLPresenter
-
class
UnknownOpaqueElement extends OpaqueElement
completely unknown elements
Value Members
- object OpaqueContext extends ListWrapperCompanion[ObjFragment, OpaqueContext] with Serializable
- object OpaqueText
-
object
OpaqueXML
helper functions