public class KeYSelectionEvent
extends java.lang.Object
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
|
public KeYSelectionEvent(KeYSelectionModel source)
source
- the SelectedNodeModel where the event had its
originpublic KeYSelectionModel getSource()
Copyright © 2003-2019 The KeY-Project.