de.uka.ilkd.key.gui.ext

Interface KeYExtConst

public interface KeYExtConst

Constants used in the KeY GUI Extensions.

Author:

Alexander Weigl

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	PATH Additional key for Actions.
static java.lang.String	PRIORITY Additional key for Actions.

Field Detail

PRIORITY

static final java.lang.String PRIORITY

Additional key for Actions. Describes the priority, and therefor an order to arrange these actions.

See Also:

Constant Field Values

PATH

static final java.lang.String PATH

Additional key for Actions. Describes a path in a menu where an action should be injected in.

The path should be a dot-separated string, i.e. "Heatmap.Options" would inject an action into a sub-sub Menu Options below Heatmap.

See Also:

KeYGuiExtensionFacade.findMenu(JMenu, Iterator), Constant Field Values