public class ProofScriptWorker extends javax.swing.SwingWorker<java.lang.Object,java.lang.Object> implements InterruptListener
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 and Description |
---|
ProofScriptWorker(KeYMediator mediator,
java.io.File file) |
ProofScriptWorker(KeYMediator mediator,
java.lang.String script,
Location location) |
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) |
private final KeYMediator mediator
private final java.lang.String script
private final Location initialLocation
private javax.swing.JDialog monitor
private javax.swing.JTextArea logArea
private final java.util.Observer observer
public ProofScriptWorker(KeYMediator mediator, java.io.File file) throws java.io.IOException
java.io.IOException
public ProofScriptWorker(KeYMediator mediator, java.lang.String script, Location location)
protected java.lang.Object doInBackground() throws java.lang.Exception
doInBackground
in class javax.swing.SwingWorker<java.lang.Object,java.lang.Object>
java.lang.Exception
private void makeDialog()
protected void process(java.util.List<java.lang.Object> chunks)
process
in class javax.swing.SwingWorker<java.lang.Object,java.lang.Object>
public void init()
public void done()
done
in class javax.swing.SwingWorker<java.lang.Object,java.lang.Object>
private static void runWithDeadline(java.lang.Runnable runnable, int milliseconds)
public void interruptionPerformed()
interruptionPerformed
in interface InterruptListener