public class ProofSaverEvent
extends java.util.EventObject
ProofSaver
.Constructor and Description |
---|
ProofSaverEvent(ProofSaver source,
java.lang.String filename,
java.lang.String errorMsg)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getErrorMsg()
Returns the error message.
|
java.lang.String |
getFilename()
Returns the file name.
|
ProofSaver |
getSource() |
public ProofSaverEvent(ProofSaver source, java.lang.String filename, java.lang.String errorMsg)
source
- The ProofSaver
which throws this event.filename
- The file name.errorMsg
- The error message.public java.lang.String getFilename()
public java.lang.String getErrorMsg()
public ProofSaver getSource()
getSource
in class java.util.EventObject
Copyright © 2003-2019 The KeY-Project.