final
object
Filter
Constructors
Members
val
empty
: Filter
def
apply
(
id:
String
)
(
f:
PartialFunction
[
TermInfo, TermAction
]
)
: Filter
def
merge
(
pfs:
[
Filter
]
)
: Filter
Merges multiple [[Filter]]s into one.
Merges multiple [[Filter]]s into one.
def
wrap
(
id:
String
)
(
f:
TermInfo => Option
[
TermAction
]
)
: Filter