diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java index df59e0c1ae7..222925c67ca 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java @@ -3,6 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.control; +import java.util.concurrent.locks.Condition; +import java.util.concurrent.locks.ReentrantLock; +import javax.swing.*; + import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; @@ -19,12 +23,20 @@ import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * The default implementation of {@link ProofControl}. * * @author Martin Hentschel */ +@NullMarked public class DefaultProofControl extends AbstractProofControl { + private static final Logger LOGGER = LoggerFactory.getLogger(DefaultProofControl.class); + /** * The {@link UserInterfaceControl} in which this {@link ProofControl} is used. */ @@ -33,8 +45,15 @@ public class DefaultProofControl extends AbstractProofControl { /** * The currently running {@link Thread}. */ + @Nullable private Thread autoModeThread; + /** + * A condition for waiting during active auto-mode. + */ + @Nullable + private Condition notInAutoMode; + /** * Constructor. * @@ -81,10 +100,16 @@ public synchronized void stopAutoMode() { @Override public void waitWhileAutoMode() { - while (isInAutoMode()) { // Wait until auto mode has stopped. + if (SwingUtilities.isEventDispatchThread()) { + LOGGER.error("", new IllegalStateException( + "tried to block the UI thread whilst waiting for auto mode to finish")); + return; // do not block the UI thread + } + if (notInAutoMode != null) { try { - Thread.sleep(100); - } catch (InterruptedException e) { + notInAutoMode.await(); + } catch (InterruptedException ignore) { + } } } @@ -101,10 +126,13 @@ private class AutoModeThread extends Thread { private final ProverTaskListener ptl; + private final ReentrantLock lock = new ReentrantLock(); + public AutoModeThread(Proof proof, ImmutableList goals, ProverTaskListener ptl) { this.proof = proof; this.goals = goals; this.ptl = ptl; + notInAutoMode = lock.newCondition(); } @Override @@ -122,6 +150,10 @@ public void run() { starter.start(); } } finally { + lock.lock(); + notInAutoMode.signalAll(); + lock.unlock(); + autoModeThread = null; fireAutoModeStopped(new ProofEvent(proof)); } @@ -146,10 +178,13 @@ private class MacroThread extends Thread { private final PosInOccurrence posInOcc; + private final ReentrantLock lock = new ReentrantLock(); + public MacroThread(Node node, ProofMacro macro, PosInOccurrence posInOcc) { this.node = node; this.macro = macro; this.posInOcc = posInOcc; + notInAutoMode = lock.newCondition(); } @Override @@ -172,6 +207,11 @@ public void run() { if (ptl != null) { ptl.taskFinished(info); } + + lock.lock(); + notInAutoMode.signalAll(); + lock.unlock(); + autoModeThread = null; fireAutoModeStopped(new ProofEvent(proof)); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java index 6453f422730..49bc7dd169e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java @@ -6,7 +6,6 @@ import java.util.ArrayList; import java.util.Collection; import java.util.EventObject; -import java.util.concurrent.locks.Condition; import java.util.List; import java.util.concurrent.CopyOnWriteArrayList; import java.util.function.Consumer; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java index eb7625c1142..65be1558450 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java @@ -28,9 +28,9 @@ import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.strategy.StrategyProperties; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -49,7 +49,8 @@ public class MediatorProofControl extends AbstractProofControl { private AutoModeWorker worker; /** - * This is condition is non-null during auto-mode execution. You can wait on it to block until auto-mode has finished. + * This is condition is non-null during auto-mode execution. You can wait on it to block until + * auto-mode has finished. */ @Nullable private Condition notInAutoMode; @@ -118,7 +119,7 @@ public void waitWhileAutoMode() { "tried to block the UI thread whilst waiting for auto mode to finish")); return; // do not block the UI thread } - if(notInAutoMode != null) { + if (notInAutoMode != null) { try { notInAutoMode.await(); } catch (InterruptedException ignore) {