de.uka.ilkd.key.gui.configuration

Class ConfigChangeEvent

java.lang.Object

de.uka.ilkd.key.gui.configuration.ConfigChangeEvent

public class ConfigChangeEvent
extends java.lang.Object

An event that indicates that the users focused node or proof has changed

Field Summary

Fields

Modifier and Type	Field and Description
private Config	source the source of this event

Constructor Summary

Constructors

Constructor and Description
ConfigChangeEvent(Config source) creates a new ConfigChangeEvent

Method Summary

Modifier and Type	Method and Description
Config	getSource() returns the Config that caused this event

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

source

private Config source

the source of this event

Constructor Detail

ConfigChangeEvent

public ConfigChangeEvent(Config source)

creates a new ConfigChangeEvent

Parameters:

source - the Config where the event had its origin

Method Detail

getSource

public Config getSource()

returns the Config that caused this event

Returns:

the Config that caused this event