package notations
This package maintains the common data structures for parsing and presentation.
TextNotation is the main notation class. It is similar to MMT objects, in particular it is stateless.
NotationContainer statefully maintains the notations assigned to a declaration. These are owned by StructuralElements to carry notations, akin to how they carry type/definition.
- Source
- package.scala
- Alphabetic
- By Inheritance
- notations
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
sealed abstract
class
Arg extends ArgumentMarker
an argument
- sealed trait ArgumentComponent extends ArityComponent
- sealed abstract class ArgumentMarker extends Marker with ArgumentComponent
-
case class
Arity(subargs: List[ArgumentComponent], variables: List[VariableComponent], arguments: List[ArgumentComponent], attribution: Boolean) extends Product with Serializable
the arity of a symbol describes what kind of objects can be formed from it
the arity of a symbol describes what kind of objects can be formed from it
- subargs
arguments before the context
- variables
the variable positions in order
- arguments
arguments after the context
- attribution
true if it can attribute an object special cases and analogs in the OpenMath role system for a symbol s: no arguments, variables: constant, s some arguments, no variables: application OMA(s, args) some arguments, some variables: binder, OMBINDC(s, vars, args) as above but exactly 1 argument: usual binders, generalized binders as suggested by Davenport, Kohlhase, MKM 2010
-
sealed
trait
ArityComponent extends AnyRef
see Arity
see Arity
Almost all ArityComponents arise as the non-Delimiter NotationMarkers
- sealed abstract class AtomicPresentationMarker extends PresentationMarker
-
case class
Bindfix(delim: Delimiter, impl: Int, expl: Int, assoc: Boolean) extends SimpleFixity with Product with Serializable
delimiter followed by first and second (explicit) argument with .
delimiter followed by first and second (explicit) argument with . in between
- assoc
merge with nested bindings using the same binder; currently ignored assumes arguments are one variable and one scope; expl must be 1
-
case class
CommonMarkerProperties(precedence: Option[Precedence], localNotations: Option[LocalNotationInfo]) extends Product with Serializable
bundles minor properties of markers to make the interfaces more robust
-
case class
Delim(s: String, associatesToLeft: Boolean = true) extends Delimiter with Product with Serializable
a delimiter
a delimiter
- s
the delimiting String, %w for whitespace
-
sealed abstract
class
Delimiter extends Marker
Markers that are delimiters
-
case class
ErrorMarker(content: List[Marker]) extends PresentationMarker with Product with Serializable
Marker for error elements in MathML
-
case class
Finite(ones: Int) extends InfInt with Product with Serializable
integer
-
abstract
class
Fixity extends AnyRef
a Fixity is used by a TextNotation to arrange arguments and delimiters
a Fixity is used by a TextNotation to arrange arguments and delimiters
A Fixity is a high-level construct that elaborates into a list of Markers. Parser and present only use the latter.
-
case class
FractionMarker(above: List[Marker], below: List[Marker], line: Boolean) extends PresentationMarker with Product with Serializable
a marker for fractions
-
case class
GlyphMarker(src: Delim, alt: String = "Failed Loading") extends AtomicPresentationMarker with Product with Serializable
a marker for mglyph, to load non-standard symbols
a marker for mglyph, to load non-standard symbols
- src
the source (link) of the symbol
- alt
the text to show in case of failure
-
case class
GroupMarker(content: List[Marker]) extends PresentationMarker with Product with Serializable
groups a list of markers into a single marker
-
case class
HOAS(apply: GlobalName, bind: GlobalName, typeAtt: GlobalName) extends Product with Serializable
tuple of HOAS symbol names
-
class
HOASApplySpine extends AnyRef
convenience apply/unapply for a HOAS application operator unapply recurses to uncurry
-
class
HOASNotation extends NotationExtension
OMA(apply, op, args)) <--> OMA(op, args)
OMA(apply, op, args)) <--> OMA(op, args)
OMA(apply, op, OMBIND(bind, context, args)) <--> OMBIND(op, context, args)
x: OMA(typeAtt, tp) <--> x: tp
assumption: HOAS notations do not have arguments before context
-
case class
IdenMarker(value: Delim) extends AtomicPresentationMarker with Product with Serializable
Marker for Identifier in MathML -
-
case class
ImplicitArg(number: Int, properties: CommonMarkerProperties = noProps) extends ArgumentMarker with Product with Serializable
an implicit argument
an implicit argument
usually these are not mentioned in the notation, but occasionally they have to be, e.g., when an implicit argument is the last argument
-
sealed abstract
class
InfInt extends Ordered[InfInt]
InfInt: integers with positive and negative infinity
-
case class
Infix(delim: Delimiter, impl: Int, expl: Int, assoc: Option[Boolean]) extends SimpleFixity with Product with Serializable
delimiter after the first (explicit) argument
delimiter after the first (explicit) argument
- assoc
None/Some(true)/Some(false) for none, left, right; currently ignored
-
case class
InstanceName(base: Delim) extends PlaceholderDelimiter with Product with Serializable
expands by prepending the instance name to a delimiter
expands by prepending the instance name to a delimiter
- base
delimiter independent of instance name
- case class InvalidNotation(msg: String) extends Throwable with Product with Serializable
-
case class
LabelArg(number: Int, info: LabelInfo, properties: CommonMarkerProperties = noProps) extends Arg with Product with Serializable
OML arguments, possibly with required type/definiens
-
case class
LabelInfo(typed: Boolean, defined: Boolean, dependent: Boolean) extends Product with Serializable
bundles flags for properties of LabelArg and LabelSeqArg
bundles flags for properties of LabelArg and LabelSeqArg
- typed
types are required
- defined
definitions are required
- dependent
definitions are required
-
case class
LabelMarker(content: List[Marker], label: String) extends PresentationMarker with Product with Serializable
a maker based on mathml label
-
case class
LabelSeqArg(number: Int, sep: Delim, info: LabelInfo, properties: CommonMarkerProperties) extends SeqArg with Product with Serializable
sequence of LabelArg
sequence of LabelArg
- sep
the separator
-
case class
LocalNotationInfo(argument: Int, role: Role, replace: Boolean) extends Product with Serializable
determines how different notations are to be used for parsing a particular argument
determines how different notations are to be used for parsing a particular argument
- argument
the argument that determines what notations to use
- role
how does that argument determine a set of notations
- replace
determines if new notations replace or extend existing ones
-
sealed abstract
class
Marker extends AnyRef
Objects of type Marker make up the pattern of a Notation
-
case class
Mixfix(markers: List[Marker]) extends Fixity with Product with Serializable
the default Fixity, which is directly a list of markers
-
class
NestedHOASNotation extends NotationExtension
Church-style higher-order abstract (obj) syntax within LF-style higher-order abstract syntax (meta),
Church-style higher-order abstract (obj) syntax within LF-style higher-order abstract syntax (meta),
e.g., apply: tm A=>B -> tm B -> tm B lam : (tm A -> tm B) -> tm A=>B
assumption: notations give meta-arguments as arguments before context
-
class
NotationCache extends ArchiveChangeListener
caches notations for objects that are not in memory by reading them when an archive is opened
caches notations for objects that are not in memory by reading them when an archive is opened
When loading an object into in Controller.add, cache entries are deleted so that future lookup are made via the libary
-
class
NotationContainer extends ComponentContainer
A NotationContainer wraps around various notations that can be associated with a Declaration
- class NotationDimension extends AnyRef
-
abstract
class
NotationExtension extends Rule
A Fixity is a high-level description of a list of markers that can be used for parsing or presentation
A Fixity is a high-level description of a list of markers that can be used for parsing or presentation
It is returned by a FixityParser and used in a TextNotation
-
case class
NotationScope(variant: Option[String], languages: List[String], priority: Int) extends Product with Serializable
scope where a notation is applicable variant : optionally the name of this notation variant languages : the languages where this notation is applicable (e.g.
scope where a notation is applicable variant : optionally the name of this notation variant languages : the languages where this notation is applicable (e.g. tex, mmt, lf, mathml) priority : the priority of this notation when looking for a default notation
-
case class
NumberMarker(value: Delim) extends AtomicPresentationMarker with Product with Serializable
a marker for a fixed numeric value
-
class
OMAUnder extends AnyRef
apply/unapply for a pragmatic OMA under a given list of HOAS apply operators
-
case class
PhantomMarker(content: List[Marker]) extends PresentationMarker with Product with Serializable
Marker for phantom elements in MathML
-
abstract
class
PlaceholderDelimiter extends Delimiter
special delimiters that use non-trivial implementations of expand
special delimiters that use non-trivial implementations of expand
These are only useful for presentation, not for parsing.
-
case class
Postfix(delim: Delimiter, impl: Int, expl: Int) extends SimpleFixity with Product with Serializable
delimiter after the (explicit) arguments
- case class PragmaticTerm(op: GlobalName, subs: Substitution, con: Context, args: List[Term], attribution: Boolean, notation: TextNotation, pos: List[Position]) extends Product with Serializable
- class Pragmatics extends ChangeListener
-
sealed
case class
Precedence(prec: InfInt, loseTie: Boolean) extends Ordered[Precedence] with Product with Serializable
binding precedences of operators are represented
binding precedences of operators are represented
- loseTie
tie-breaking flag for comparisons
-
case class
Prefix(delim: Delimiter, impl: Int, expl: Int) extends SimpleFixity with Product with Serializable
delimiter followed by the (explicit) arguments
-
sealed abstract
class
PresentationMarker extends Marker
PresentationMarker's occur in two-dimensional notations
PresentationMarker's occur in two-dimensional notations
They typically take other lists of markers as arguments, thus building a tree of markers.
- trait PresentationMarkerWrappingMarkerList extends AnyRef
-
case class
RootMarker(argument: List[Marker], index: List[Marker] = Nil) extends PresentationMarker with Product with Serializable
a marker representing the nth(index) root in mathml
-
case class
ScriptMarker(main: Marker, sup: Option[Marker], sub: Option[Marker], over: Option[Marker], under: Option[Marker]) extends PresentationMarker with Product with Serializable
decorates a marker with various scripts
-
sealed abstract
class
SeqArg extends ArgumentMarker
a sequence argument
-
case class
SimpArg(number: Int, properties: CommonMarkerProperties = noProps) extends Arg with Product with Serializable
normal arguments
-
case class
SimpSeqArg(number: Int, sep: Delim, properties: CommonMarkerProperties) extends SeqArg with Product with Serializable
sequence of SimpArg
sequence of SimpArg
- sep
the separator
-
abstract
class
SimpleFixity extends Fixity
A SimpleFixity is one out of multiple typical fixities (infix, postfix, etc) characterized by using only a single delimiter.
A SimpleFixity is one out of multiple typical fixities (infix, postfix, etc) characterized by using only a single delimiter.
impl and expl do not have to agree with the number of arguments demanded by the type system. * Notation has more arguments than function type: Notation extensions may handle the extra arguments. Example: equal : {a:tp} tm (a => a => bool), impl = 1, expl = 2 * Notation has less arguments than function type: Operator return a function. Example: union : {a:tp} tm (a set => a set => a set) where a set = a => bool, impl = 1, expl = 2
-
case class
SymbolName() extends PlaceholderDelimiter with Product with Serializable
expands to the name of the symbol or an alias (whichever is the shortest)
expands to the name of the symbol or an alias (whichever is the shortest)
useful for repetitive notations that differ only in the name
-
case class
TableMarker(content: List[Marker]) extends PresentationMarker with Product with Serializable
a marker based on mathml mtd elements, representing tables
-
case class
TdMarker(content: List[Marker]) extends PresentationMarker with Product with Serializable
a marker based on mathml mtd elements, representing table cells
- case class TextMarker(text: Delim) extends AtomicPresentationMarker with Product with Serializable
-
case class
TextNotation(fixity: Fixity, precedence: Precedence, meta: Option[MPath], scope: NotationScope = NotationScope.default) extends HasMetaData with Product with Serializable
A TextNotation is a Notation that can be used for parsing objects in text syntax
A TextNotation is a Notation that can be used for parsing objects in text syntax
- fixity
the mixfix notation
- precedence
the precedence, notations with lower precedence are tried first, thus grab larger subterms
- meta
the meta-theory of this notation if different from the current meta-theory
- scope
a typed Var must be preceded by a Delim because Var.key does not trigger the notation not all markers may be Arg because such notations cannot be parsed if the only marker is SeqArg, it must hold that OMA(name, List(x)) = x because sequences of length 1 are parsed as themselves
-
case class
TrMarker(content: List[Marker]) extends PresentationMarker with Product with Serializable
a marker based on mathml mtd elements, representing table rows
-
case class
Var(number: Int, typed: Boolean, sep: Option[Delim], properties: CommonMarkerProperties = noProps) extends Marker with VariableComponent with Product with Serializable
a variable binding
a variable binding
- number
the number of the variable
- typed
true if the variable carries a type (to be inferred if omitted)
- sep
if given, this is a variable sequence with this separator; for typed variables with the same type, only the last one needs a type
- sealed trait VariableComponent extends ArityComponent
-
sealed abstract
class
VerbalizationMarker extends Marker
Verbalization markers occur in verbalization notations
- case class WordMarker(word: String) extends VerbalizationMarker with Product with Serializable
Value Members
- object Arity extends Serializable
- object AttributedObject extends Marker with Product with Serializable
- object CommonMarkerProperties extends Serializable
-
object
Delim extends Serializable
replace the default unapply method to ignore the argument with default value when pattern-matching
-
object
Delimiter
helper object
-
object
FixityParser
parses MixFix and SimpleFixity
-
object
InfInt
helper object for InfInts
-
object
InferenceMarker extends AtomicPresentationMarker with Product with Serializable
a marker for type of the presented object
-
object
Infinite extends InfInt with Product with Serializable
positively infinite InfInt
- object LabelInfo extends Serializable
- object LocalNotationInfo extends Serializable
- object Marker
-
object
MixfixNotation extends NotationExtension
the standard mixfix notation for a list of Markers
-
object
NegInfinite extends InfInt with Product with Serializable
positively infinite InfInt
- object NotationContainer
-
object
NotationConversions
defines some implicit conversions to produce Markers
- object NotationDimension
- object NotationLexFunction extends AsymmetricEscapeLexer
- object NotationRealizedType extends RepresentedRealizedType[TextNotation]
- object NotationScope extends Serializable
- object NotationSemanticType extends Atomic[TextNotation]
- object NotationType
-
object
Precedence extends Serializable
helper object for precedences
- object PresentationMarker
- object TextNotation extends Serializable