public abstract class TacletMatcherKit
extends java.lang.Object
getKit()
to get the concrete factory and call createTacletMatcher(Taclet)
to create a matcher for a Taclet
The active factory is chosen at runtime by passing a value for the system property taclet.match
Currently supported values are: legacy
and vm
. The legacy matching algorithm is
the one used since the beginning of KeY. It will soon become deprecated and replaced y vm
as default.Modifier and Type | Class and Description |
---|---|
private static class |
TacletMatcherKit.LegacyTacletMatcherKit
The concrete factory for the legacy taclet matcher.
|
private static class |
TacletMatcherKit.VMTacletMatcherKit
The concrete factory for the vm based taclet matcher.
|
Modifier and Type | Field and Description |
---|---|
private static TacletMatcherKit |
ACTIVE_TACLET_MATCHER_KIT |
private static java.lang.String |
TACLET_MATCHER_SELECTION_VALUE
sets up the concrete factory to use depending on the provided system property or the given default if no
property is set
|
Constructor and Description |
---|
TacletMatcherKit() |
Modifier and Type | Method and Description |
---|---|
abstract TacletMatcher |
createTacletMatcher(Taclet taclet)
the creator method returning the matcher for the specified taclet
|
static TacletMatcherKit |
getKit()
returns the currently enabled factory
|
private static final java.lang.String TACLET_MATCHER_SELECTION_VALUE
private static final TacletMatcherKit ACTIVE_TACLET_MATCHER_KIT
public static TacletMatcherKit getKit()
public abstract TacletMatcher createTacletMatcher(Taclet taclet)
taclet
- the Taclet
for which to create a matcher