public class NotificationManager
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private class |
NotificationManager.NotificationListener |
Modifier and Type | Field and Description |
---|---|
private boolean |
autoMode
true if we are currently in automode
|
private NotificationManager.NotificationListener |
notificationListener |
private java.util.Map<NotificationEventID,NotificationTask> |
notificationTasks
list of notification tasks
|
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) |
private java.util.Map<NotificationEventID,NotificationTask> notificationTasks
private boolean autoMode
private NotificationManager.NotificationListener notificationListener
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
-