public class GeneralInformationEvent extends NotificationEvent
GeneralFailureEvent
instead.Constructor and Description |
---|
GeneralInformationEvent(java.lang.String informationMessage)
Creates an event informing the user about the fact given as string
|
GeneralInformationEvent(java.lang.String context,
java.lang.String informationMessage)
Creates an event informing the user about the fact given as string
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getContext()
returns the context as string
|
java.lang.String |
getMessage()
returns the information as string
|
getEventID
public GeneralInformationEvent(java.lang.String context, java.lang.String informationMessage)
context
- the String describing the context/category of the
information (e.g. used as window title, head line etc.)informationMessage
- the String containing the informationpublic GeneralInformationEvent(java.lang.String informationMessage)
informationMessage
- the String containing the informationCopyright © 2003-2019 The KeY-Project.