@Retention(value=RUNTIME)
public static @interface KeYGuiExtension.Info
Modifier and Type | Optional Element and Description |
---|---|
java.lang.String |
description
Long description of this extension.
|
boolean |
disabled
Disabled extension are not instantiated
|
boolean |
experimental
Marks an extensions as experimental.
|
java.lang.String |
name
Simple name of this extension, else the fqdn of the class is used
|
boolean |
optional
Optional extension can be disabled by the user.
|
int |
priority
Loading priority of this extension.
|
public abstract java.lang.String name
public abstract boolean optional
public abstract boolean disabled
public abstract java.lang.String description
what does it? who develops it?
Copyright © 2003-2019 The KeY-Project.