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