Commit 83df2985 authored by Sarah Grebing's avatar Sarah Grebing

bugfix filter inapplicable rules

parent f80ca40f
Pipeline #22326 passed with stages
in 3 minutes and 29 seconds
...@@ -112,6 +112,8 @@ public class KeYProofFacade { ...@@ -112,6 +112,8 @@ public class KeYProofFacade {
protected void succeeded() { protected void succeeded() {
System.out.println("KeYProofFacade.succeeded"); System.out.println("KeYProofFacade.succeeded");
environment.set(getValue().getEnv()); environment.set(getValue().getEnv());
//SaG: this needs to be set to filter inapplicable rules
getEnvironment().getProofControl().setMinimizeInteraction(true);
proof.set(getValue().getProof()); proof.set(getValue().getProof());
contract.set(null); contract.set(null);
setLoading(false); setLoading(false);
......
...@@ -15,8 +15,10 @@ import org.apache.logging.log4j.LogManager; ...@@ -15,8 +15,10 @@ import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
import javax.annotation.Nullable; import javax.annotation.Nullable;
import javax.xml.bind.JAXBException;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.io.StringWriter;
import java.util.Optional; import java.util.Optional;
import java.util.concurrent.CyclicBarrier; import java.util.concurrent.CyclicBarrier;
import java.util.concurrent.Semaphore; import java.util.concurrent.Semaphore;
...@@ -73,12 +75,13 @@ public class SaveCommand implements CommandHandler<KeyData> { ...@@ -73,12 +75,13 @@ public class SaveCommand implements CommandHandler<KeyData> {
if(execute.get()) if(execute.get())
interpreter.getSelectedNode().getData().getProof().saveToFile(newFile); interpreter.getSelectedNode().getData().getProof().saveToFile(newFile);
//KeyPersistentFacade.write(); KeyPersistentFacade.write(interpreter.getCurrentState(), new StringWriter());
//TODO Call to key persistend facade
} catch (IOException e) { } catch (IOException e) {
e.printStackTrace(); e.printStackTrace();
} catch (InterruptedException e) { } catch (InterruptedException e) {
e.printStackTrace(); e.printStackTrace();
} catch (JAXBException e) {
e.printStackTrace();
} }
} }
......
...@@ -1137,8 +1137,7 @@ public class DebuggerMain implements Initializable { ...@@ -1137,8 +1137,7 @@ public class DebuggerMain implements Initializable {
interactiveModeController.setDebuggerFramework(model.getDebuggerFramework()); interactiveModeController.setDebuggerFramework(model.getDebuggerFramework());
interactiveModeController.setKeYServices(this.getFacade().getService()); interactiveModeController.setKeYServices(this.getFacade().getService());
interactiveModeController.setActivated(true); interactiveModeController.setActivated(true);
//SaG: this needs to be set to filter inapplicable rules
this.getFacade().getEnvironment().getProofControl().setMinimizeInteraction(true);
interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel()); interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
interactive_undo.setDisable(false); interactive_undo.setDisable(false);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment