001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof.init;
012:
013: import java.io.File;
014:
015: import javax.swing.JOptionPane;
016:
017: import de.uka.ilkd.key.gui.ExceptionDialog;
018: import de.uka.ilkd.key.gui.KeYMediator;
019: import de.uka.ilkd.key.gui.Main;
020: import de.uka.ilkd.key.gui.SwingWorker;
021: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
022:
023: /**
024: * Loader for the generation of taclet proof obligations, mostly copied from
025: * <code>ProblemLoader</code>
026: */
027: public class TacletSoundnessPOLoader implements Runnable {
028: final File file;
029: final Main main;
030: final KeYMediator mediator;
031:
032: private SwingWorker worker;
033:
034: ProblemInitializer init;
035:
036: public TacletSoundnessPOLoader(File file, Main main) {
037: this .main = main;
038: mediator = main.mediator();
039: this .file = file;
040: }
041:
042: public void run() {
043: /*
044: * Invoking start() on the SwingWorker causes a new Thread to be created
045: * that will call construct(), and then finished(). Note that finished()
046: * is called even if the worker is interrupted because we catch the
047: * InterruptedException in doWork().
048: */
049: worker = new SwingWorker() {
050:
051: public Object construct() {
052: Object res = doWork();
053: return res;
054: }
055:
056: public void finished() {
057: mediator.startInterface(true);
058: Main main = Main.getInstance();
059: String msg = (String) get();
060: if (!"".equals(msg)) {
061: JOptionPane
062: .showMessageDialog(
063: main,
064: msg,
065: "Error occurred while creating proof obligation",
066: JOptionPane.ERROR_MESSAGE);
067: }
068: }
069: };
070:
071: mediator.stopInterface(true);
072: worker.start();
073: }
074:
075: protected Object doWork() {
076: final TacletSoundnessPO prob = new TacletSoundnessPO(file
077: .getName(), file, main.getProgressMonitor());
078:
079: String status = "";
080: try {
081: ProofEnvironment env = mediator.getSelectedProof().env();
082: ProblemInitializer pi = new ProblemInitializer(Main
083: .getInstance());
084: pi.startProver(env, prob);
085: } catch (Throwable e) {
086: mediator.getExceptionHandler().reportException(e);
087: new ExceptionDialog(mediator.mainFrame(), mediator
088: .getExceptionHandler().getExceptions());
089: mediator.getExceptionHandler().clear();
090: main
091: .setStatusLine("Exception occurred while creating proof obligation");
092: status = e.toString();
093: e.printStackTrace();
094: } finally {
095: prob.close();
096: }
097:
098: return status;
099: }
100:
101: }
|