case class UnknownOMLIT(valueString: String, synType: Term) extends Term with OMLITTrait with Product with Serializable
degenerate case of OMLIT when no RealizedType was known to parse a literal
This class is awkward but necessary to permit a lookup-free parser, which delays parsing of literals to a later phase. UnknownOMLITs are replaced with OMLITs in the libraries.StructureChecker.
- synType
the type of the this literal
- Source
- Obj.scala
- Alphabetic
- By Inheritance
- UnknownOMLIT
- Serializable
- Serializable
- Product
- Equals
- OMLITTrait
- Term
- ThisTypeTrait
- Obj
- HashEquality
- ShortURIPrinter
- BaseType
- Content
- ClientProperties
- HasMetaData
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
Type Members
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
^(sub: Substitution): ThisType
applies a substitution to an object (computed immediately) implemented in terms of ^^ and PlainSubstitutionApplier
applies a substitution to an object (computed immediately) implemented in terms of ^^ and PlainSubstitutionApplier
- Definition Classes
- Obj
-
def
^?(sub: Substitution): ThisType
optimized version of substitution defined in terms of SmartSubstitutionApplier
optimized version of substitution defined in terms of SmartSubstitutionApplier
- Definition Classes
- Obj
-
def
^^(sub: Substitution)(implicit sa: SubstitutionApplier): ThisType
convenience method that applies substitution by relegating to a SubstitutionApplier
convenience method that applies substitution by relegating to a SubstitutionApplier
This has the effect that o ^^ sub becomes an infix notation for substitution if an implicit SubstitutionApplier is available.
- Definition Classes
- Obj
-
def
apply(args: Term*): OMA
permits the intuitive f(t_1,...,t_n) syntax for term applications
permits the intuitive f(t_1,...,t_n) syntax for term applications
- Definition Classes
- Term
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
lazy val
clientProperty: ListMap[URI, Any]
- Definition Classes
- ClientProperties
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
def
copyFrom(o: Obj): Unit
replaces metadata of this with pointer to those of o
replaces metadata of this with pointer to those of o
- o
the original object call o2.copyFrom(o1) after transforming o1 into o2 in order to preserve metadata
- Definition Classes
- Obj
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(that: Any): Boolean
checks equality, including the case OMLIT =?= UnknownOMLIT
checks equality, including the case OMLIT =?= UnknownOMLIT
- Definition Classes
- OMLITTrait → AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
lazy val
freeVars: List[LocalName]
the free variables of this object in any order
the free variables of this object in any order
- Definition Classes
- Obj
-
def
from(o: Term): UnknownOMLIT.this.type
applies copyFrom and returns this
applies copyFrom and returns this
- returns
this object but with the metadata from o
- Definition Classes
- Term
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getMetaDataNode: NodeSeq
- Definition Classes
- HasMetaData
-
def
governingPath: Option[ContentPath]
the governing path required by Content is the head, if any
the governing path required by Content is the head, if any
- Definition Classes
- Obj
-
lazy val
hash: Int
the hash code
the hash code
- Definition Classes
- HashEquality
-
def
hashCode(): Int
hash code depends only on synType and valueString
hash code depends only on synType and valueString
- Definition Classes
- OMLITTrait → AnyRef → Any
-
def
hasheq(that: HashEquality[Obj]): Boolean
this hasheq that is the same as this == that, but fails immediately if false
this hasheq that is the same as this == that, but fails immediately if false
- Definition Classes
- HashEquality
-
def
hashneq(that: HashEquality[Obj]): Boolean
this hasheq that is the same as this == that, but fails immediately if false
this hasheq that is the same as this == that, but fails immediately if false
- Definition Classes
- HashEquality
-
def
head: None.type
- Definition Classes
- OMLITTrait → Obj
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
mdNode: Seq[Node] with AbstractSeq[Node] with Serializable
- Attributes
- protected
- Definition Classes
- Obj
-
val
metadata: MetaData
- Definition Classes
- HasMetaData
-
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
strip: Term
- Definition Classes
- Term
-
def
subobject(pos: Position): (Context, Obj)
returns the subobject at a given position and its context
returns the subobject at a given position and its context
- Definition Classes
- Obj
-
def
subobjects: Nil.type
all direct subobjects of this object with their context (excluding any outer context of this object)
all direct subobjects of this object with their context (excluding any outer context of this object)
- Definition Classes
- OMLITTrait → Obj
-
def
subobjectsNoContext(os: List[Obj]): List[(Context, Obj)]
auxiliary function for subobjects in the absence of binding
auxiliary function for subobjects in the absence of binding
- Attributes
- protected
- Definition Classes
- Obj
-
def
substitute(sub: Substitution)(implicit sa: SubstitutionApplier): OMLITTrait
generic version of substitution that does one step and recurses according to a SubstitutionApplier
generic version of substitution that does one step and recurses according to a SubstitutionApplier
capture is avoided by renaming bound variables that are free in sub
Individual SubstitutionAppliers can default to this method in order to recurse one level.
- Definition Classes
- OMLITTrait → Obj
-
val
synType: Term
- Definition Classes
- UnknownOMLIT → OMLITTrait
-
def
synTypeXML: Union[String, Node]
- Definition Classes
- OMLITTrait
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toCML: Node
- Definition Classes
- Obj
-
def
toCMLQVars(implicit qvars: Context): Elem
- Definition Classes
- OMLITTrait → Obj
-
def
toMPath: MPath
the syntactically computed MPath of the term.
the syntactically computed MPath of the term. If the term is module level, this is guaranteed to be correct.
- Definition Classes
- Term
-
def
toNode: Elem
prints to OpenMath
prints to OpenMath
- Definition Classes
- OMLITTrait → Obj → Content
-
def
toNode(rh: RenderingHandler): Unit
by default, this prints out toNode
by default, this prints out toNode
potentially large StructuralElements should override it with a memory-efficient implementation
- Definition Classes
- Content
-
def
toOBJNode: Elem
prints to OpenMath (with OMOBJ wrapper)
prints to OpenMath (with OMOBJ wrapper)
- Definition Classes
- Obj
-
def
toStr(implicit shortURIs: Boolean): String
configurable string representation
configurable string representation
- shortURIs
print OMS without namespace, theory
- Definition Classes
- UnknownOMLIT → ShortURIPrinter
-
def
toString(): String
defaults to toStr(false)
defaults to toStr(false)
- Definition Classes
- ShortURIPrinter → AnyRef → Any
-
val
valueString: String
canonical string representation of this literal
canonical string representation of this literal
- Definition Classes
- UnknownOMLIT → OMLITTrait
-
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()