public class NotificationManager
extends java.lang.Object
Constructor and Description |
---|
NotificationManager(KeYMediator mediator,
javax.swing.JFrame comp)
creates an instance of the notification manager
|
Modifier and Type | Method and Description |
---|---|
void |
addNotificationTask(NotificationTask task)
adds a notification task to this manager
|
void |
handleNotificationEvent(NotificationEvent event)
dispatches the received notification event and triggers the corresponding
task
|
boolean |
inAutoMode() |
NotificationTask |
removeNotificationTask(NotificationEventID eventID)
Removes the
NotificationTask with the given NotificationEventID . |
void |
removeNotificationTask(NotificationTask task)
removes the given notification task from the list of active tasks
|
void |
setDefaultNotification(javax.swing.JFrame comp) |
public NotificationManager(KeYMediator mediator, javax.swing.JFrame comp)
public void setDefaultNotification(javax.swing.JFrame comp)
public void addNotificationTask(NotificationTask task)
task
- the NotificationTask to be addedpublic void removeNotificationTask(NotificationTask task)
task
- the task to be removedpublic NotificationTask removeNotificationTask(NotificationEventID eventID)
NotificationTask
with the given NotificationEventID
.
This functionality is used by the Eclipse integration.
eventID
- The NotificationEventID
to remove its NotificationTask
.NotificationTask
or null
if none was available.public boolean inAutoMode()
public void handleNotificationEvent(NotificationEvent event)
event
- Copyright © 2003-2019 The KeY-Project.