public class EditorPanelProperties
extends java.lang.Object
Constructor and Description |
---|
EditorPanelProperties(org.processmining.framework.plugin.PluginContext context,
ProcessTree tree,
int maxWidth,
int maxHeight,
GraphMouseListener graphMouseListener,
GraphPanel graphPanel,
java.util.Collection<javax.swing.JComponent> components) |
Modifier and Type | Method and Description |
---|---|
javax.swing.JComponent |
createProperties() |
int |
getHeight() |
void |
update() |
public EditorPanelProperties(org.processmining.framework.plugin.PluginContext context, ProcessTree tree, int maxWidth, int maxHeight, GraphMouseListener graphMouseListener, GraphPanel graphPanel, java.util.Collection<javax.swing.JComponent> components)