de.uka.ilkd.key.prover.impl

Class DefaultTaskStartedInfo

java.lang.Object

de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo

All Implemented Interfaces:

TaskStartedInfo

public class DefaultTaskStartedInfo
extends java.lang.Object
implements TaskStartedInfo

Default implementation of a TaskStartedInfo.

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.prover.TaskStartedInfo

TaskStartedInfo.TaskKind

Field Summary

Fields

Modifier and Type	Field and Description
private TaskStartedInfo.TaskKind	kind
private java.lang.String	message
private int	size

Constructor Summary

Constructors

Constructor and Description
DefaultTaskStartedInfo(TaskStartedInfo.TaskKind kind, java.lang.String message, int size)

Method Summary

Modifier and Type	Method and Description
TaskStartedInfo.TaskKind	getKind() allows to query about the nature of task
java.lang.String	getMessage() returns a message with a description of the task, example: "Processing Strategy"
int	getSize() returns measure for the total size of the task.
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

kind

private final TaskStartedInfo.TaskKind kind

message

private final java.lang.String message

size

private final int size

Constructor Detail

DefaultTaskStartedInfo

public DefaultTaskStartedInfo(TaskStartedInfo.TaskKind kind,
                              java.lang.String message,
                              int size)

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getKind

public TaskStartedInfo.TaskKind getKind()

allows to query about the nature of task

Specified by:

getKind in interface TaskStartedInfo

Returns:

the kind of the task

getMessage

public java.lang.String getMessage()

returns a message with a description of the task, example: "Processing Strategy"

Specified by:

getMessage in interface TaskStartedInfo

getSize

public int getSize()

returns measure for the total size of the task. The number indicates the amount of work needed to complete the task, mostly used by the GUI to display a progress bar. A returned value of 0 means unknown size.

Specified by:

getSize in interface TaskStartedInfo