abstract class LookupWithNotFoundHandler extends Lookup
delegates all lookup methods to another Lookup and handles the NotFound exception
- Source
- Lookup.scala
- Alphabetic
- By Inheritance
- LookupWithNotFoundHandler
- Lookup
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Abstract Value Members
-
abstract
def
forDeclarationsInScope(mod: Term)(f: (MPath, Term, Declaration) ⇒ Unit): Unit
apply a function to all declarations that are visible (based on what is currently loaded) to a theory
apply a function to all declarations that are visible (based on what is currently loaded) to a theory
- mod
the theory
- f
applied to (theory t declaring d, morphism mod->t that makes d visible, d)
- Definition Classes
- Lookup
-
abstract
def
handler[A](code: ⇒ A): A
- Attributes
- protected
Concrete Value Members
-
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
-
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
apply(path: ContentPath): StructuralElement
- Definition Classes
- Lookup
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
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
get(home: Term, name: LocalName, error: (String) ⇒ Nothing): Declaration
lookup a declaration in a (possibly complex) module
lookup a declaration in a (possibly complex) module
- home
the module in which to look up
- name
the name look up; must start with ComplexStep unless it is local to home
- error
the continuation to call on the error message
- returns
the declaration
- Definition Classes
- LookupWithNotFoundHandler → Lookup
-
def
get(path: Path): StructuralElement
lookup a path
lookup a path
- Definition Classes
- LookupWithNotFoundHandler → Lookup
-
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]
- Definition Classes
- LookupWithNotFoundHandler → Lookup
-
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
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
-
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
preImage(p: GlobalName): Option[GlobalName]
if p is imported by a structure, returns the preimage of the symbol under the outermost structure
if p is imported by a structure, returns the preimage of the symbol under the outermost structure
- Definition Classes
- LookupWithNotFoundHandler → Lookup
-
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
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
- AnyRef → Any
-
def
visible(to: Term): Iterable[MPath]
- Definition Classes
- LookupWithNotFoundHandler → Lookup
-
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()