public class KeYRecoderExcHandler extends Object implements ErrorHandler
Modifier and Type | Field and Description |
---|---|
private int |
errorThreshold |
private List<Throwable> |
exceptions |
Constructor and Description |
---|
KeYRecoderExcHandler() |
KeYRecoderExcHandler(int errorThreshold) |
Modifier and Type | Method and Description |
---|---|
void |
clear() |
protected int |
getErrorCount() |
int |
getErrorThreshold() |
List<Throwable> |
getExceptions() |
void |
modelUpdated(EventObject event) |
void |
modelUpdating(EventObject event) |
protected void |
recoderExitAction() |
void |
reportError(Exception e) |
void |
reportException(Throwable e) |
void |
setErrorThreshold(int maxCount) |
public KeYRecoderExcHandler()
public KeYRecoderExcHandler(int errorThreshold)
public void reportException(Throwable e)
public void clear()
protected int getErrorCount()
public int getErrorThreshold()
getErrorThreshold
in interface ErrorHandler
public final void setErrorThreshold(int maxCount)
setErrorThreshold
in interface ErrorHandler
protected void recoderExitAction()
public void reportError(Exception e)
reportError
in interface ErrorHandler
public void modelUpdating(EventObject event)
modelUpdating
in interface ModelUpdateListener
public void modelUpdated(EventObject event)
modelUpdated
in interface ModelUpdateListener