public class KeYSelectionEvent
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private KeYSelectionModel |
source
the source of this event
|
Constructor and Description |
---|
KeYSelectionEvent(KeYSelectionModel source)
creates a new SelectedNodeEvent
|
Modifier and Type | Method and Description |
---|---|
KeYSelectionModel |
getSource()
returns the KeYSelectionModel that caused this event
|
private KeYSelectionModel source
public KeYSelectionEvent(KeYSelectionModel source)
source
- the SelectedNodeModel where the event had its
originpublic KeYSelectionModel getSource()