de.uka.ilkd.key.gui

Class ProofScriptWorker

java.lang.Object

javax.swing.SwingWorker<java.lang.Object,java.lang.Object>

de.uka.ilkd.key.gui.ProofScriptWorker

All Implemented Interfaces:

InterruptListener, java.lang.Runnable, java.util.concurrent.Future<java.lang.Object>, java.util.concurrent.RunnableFuture<java.lang.Object>, java.util.EventListener

public class ProofScriptWorker
extends javax.swing.SwingWorker<java.lang.Object,java.lang.Object>
implements InterruptListener

Nested Class Summary

Nested classes/interfaces inherited from class javax.swing.SwingWorker

javax.swing.SwingWorker.StateValue

Field Summary

Fields

Modifier and Type	Field and Description
private Location	initialLocation
private javax.swing.JTextArea	logArea
private KeYMediator	mediator
private javax.swing.JDialog	monitor
private java.util.Observer	observer
private java.lang.String	script

Constructor Summary

Constructors

Constructor and Description
ProofScriptWorker(KeYMediator mediator, java.io.File file)
ProofScriptWorker(KeYMediator mediator, java.lang.String script, Location location)

Method Summary

Modifier and Type	Method and Description
protected java.lang.Object	doInBackground()
void	done()
void	init()
void	interruptionPerformed()
private void	makeDialog()
protected void	process(java.util.List<java.lang.Object> chunks)
private static void	runWithDeadline(java.lang.Runnable runnable, int milliseconds)

Methods inherited from class javax.swing.SwingWorker

addPropertyChangeListener, cancel, execute, firePropertyChange, get, get, getProgress, getPropertyChangeSupport, getState, isCancelled, isDone, publish, removePropertyChangeListener, run, setProgress

Methods inherited from class java.lang.Object

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

Field Detail

mediator

private final KeYMediator mediator

script

private final java.lang.String script

initialLocation

private final Location initialLocation

monitor

private javax.swing.JDialog monitor

logArea

private javax.swing.JTextArea logArea

observer

private final java.util.Observer observer

Constructor Detail

ProofScriptWorker

public ProofScriptWorker(KeYMediator mediator,
                         java.io.File file)
                  throws java.io.IOException

Throws:

java.io.IOException

ProofScriptWorker

public ProofScriptWorker(KeYMediator mediator,
                         java.lang.String script,
                         Location location)

Method Detail

doInBackground

protected java.lang.Object doInBackground()
                                   throws java.lang.Exception

Specified by:

doInBackground in class javax.swing.SwingWorker<java.lang.Object,java.lang.Object>

Throws:

java.lang.Exception

makeDialog

private void makeDialog()

process

protected void process(java.util.List<java.lang.Object> chunks)

Overrides:

process in class javax.swing.SwingWorker<java.lang.Object,java.lang.Object>

init

public void init()

done

public void done()

Overrides:

done in class javax.swing.SwingWorker<java.lang.Object,java.lang.Object>

runWithDeadline

private static void runWithDeadline(java.lang.Runnable runnable,
                                    int milliseconds)

interruptionPerformed

public void interruptionPerformed()

Specified by:

interruptionPerformed in interface InterruptListener