From a7bc41b8a730068694b7bfddca8d658c0afcb264 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 1 Nov 2017 05:05:15 +0100 Subject: [PATCH] Diffing and UI improvements --- .../kit/iti/formal/psdbg/parser/ASTDiff.java | 155 ++++++++++++++++++ .../iti/formal/psdbg/parser/ast/ASTNode.java | 4 + .../psdbg/parser/ast/AssignmentStatement.java | 13 ++ .../psdbg/parser/ast/CallStatement.java | 13 +- .../psdbg/parser/ast/CaseStatement.java | 11 ++ .../psdbg/parser/ast/CasesStatement.java | 17 ++ .../formal/psdbg/parser/ast/ClosesCase.java | 11 ++ .../parser/ast/DefaultCaseStatement.java | 18 ++ .../formal/psdbg/parser/ast/GoalSelector.java | 12 ++ .../parser/ast/GuardedCaseStatement.java | 10 ++ .../formal/psdbg/parser/ast/Parameters.java | 33 +++- .../formal/psdbg/parser/ast/ProofScript.java | 14 ++ .../psdbg/parser/ast/RepeatStatement.java | 2 + .../formal/psdbg/parser/ast/Signature.java | 15 +- .../formal/psdbg/parser/ast/Statements.java | 22 ++- .../iti/formal/psdbg/parser/ast/TryCase.java | 2 + .../iti/formal/psdbg/parser/ASTDiffTest.java | 29 ++++ .../iti/formal/psdbg/parser/test_diff_1.kps | 18 ++ .../iti/formal/psdbg/parser/test_diff_2.kps | 21 +++ .../psdbg/interpreter/KeYProofFacade.java | 4 +- .../funchdl/RuleCommandHandler.java | 6 +- .../psdbg/gui/controller/DebuggerMain.java | 95 ++++++++++- .../psdbg/gui/controls/SequentView.java | 2 + .../formal/psdbg/examples/agatha/script.kps | 2 - .../psdbg/gui/controller/DebuggerMain.fxml | 30 ++-- 25 files changed, 519 insertions(+), 40 deletions(-) create mode 100644 lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java create mode 100644 lang/src/test/java/edu/kit/iti/formal/psdbg/parser/ASTDiffTest.java create mode 100644 lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/test_diff_1.kps create mode 100644 lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/test_diff_2.kps diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java new file mode 100644 index 00000000..a7785e4f --- /dev/null +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java @@ -0,0 +1,155 @@ +package edu.kit.iti.formal.psdbg.parser; + +import edu.kit.iti.formal.psdbg.parser.ast.*; + +public class ASTDiff implements Visitor { + private ASTNode other; + + private ProofScript newScript; + + @Override + public ProofScript visit(ProofScript proofScript) { + newScript = new ProofScript(); + newScript.setName(proofScript.getName()); + newScript.setSignature(proofScript.getSignature()); + + other = ((ProofScript) other).getBody(); + newScript.setBody(visit(newScript.getBody())); + return newScript; + } + + @Override + public ASTNode visit(AssignmentStatement assign) { + return null; + } + + @Override + public ASTNode visit(BinaryExpression e) { + return null; + } + + @Override + public ASTNode visit(MatchExpression match) { + return null; + } + + @Override + public ASTNode visit(TermLiteral term) { + return null; + } + + @Override + public ASTNode visit(StringLiteral string) { + return null; + } + + @Override + public ASTNode visit(Variable variable) { + return null; + } + + @Override + public ASTNode visit(BooleanLiteral bool) { + return null; + } + + @Override + public Statements visit(Statements statements) { + Statements s = new Statements(); + Statements other = (Statements) this.other; + assert statements.size() <= other.size(); + + int i = 0; + for (; i < statements.size(); i++) { + if (statements.get(i).eq(other.get(i))) { + break; + } + } + + for (int j = i; j < other.size(); j++) { + s.add(other.get(i)); + } + + return s; + } + + @Override + public ASTNode visit(IntegerLiteral integer) { + return null; + } + + @Override + public ASTNode visit(CasesStatement cases) { + return null; + } + + @Override + public ASTNode visit(DefaultCaseStatement defCase) { + return null; + } + + @Override + public ASTNode visit(CallStatement call) { + return null; + } + + @Override + public ASTNode visit(TheOnlyStatement theOnly) { + return null; + } + + @Override + public ASTNode visit(ForeachStatement foreach) { + return null; + } + + @Override + public ASTNode visit(RepeatStatement repeat) { + return null; + } + + @Override + public ASTNode visit(Signature signature) { + return null; + } + + @Override + public ASTNode visit(Parameters parameters) { + return null; + } + + @Override + public ASTNode visit(UnaryExpression e) { + return null; + } + + @Override + public ASTNode visit(TryCase TryCase) { + return null; + } + + @Override + public ASTNode visit(GuardedCaseStatement guardedCaseStatement) { + return null; + } + + @Override + public ASTNode visit(CaseStatement caseStatement) { + return null; + } + + @Override + public ASTNode visit(SubstituteExpression subst) { + return null; + } + + @Override + public ASTNode visit(ClosesCase closesCase) { + return null; + } + + public ProofScript diff(ProofScript old, ProofScript rev) { + other = rev; + return (ProofScript) visit(old); + } +} diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java index 82fa18e9..0b769605 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java @@ -125,4 +125,8 @@ public abstract class ASTNode } while (n != null); return true; } + + public boolean eq(ASTNode other) { + return equals(other); + } } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/AssignmentStatement.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/AssignmentStatement.java index ea589e2a..d45c7f35 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/AssignmentStatement.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/AssignmentStatement.java @@ -74,4 +74,17 @@ public class AssignmentStatement return type != null; } + + @Override + public boolean eq(ASTNode o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + + AssignmentStatement that = (AssignmentStatement) o; + + if (!getLhs().eq(that.getLhs())) return false; + if (!getRhs().eq(that.getRhs())) return false; + return getType() != null ? getType().equals(that.getType()) : that.getType() == null; + } } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/CallStatement.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/CallStatement.java index 2822388e..54640e09 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/CallStatement.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/CallStatement.java @@ -64,9 +64,20 @@ public class CallStatement extends Statement @Getter @Setter @NonNull private Statements body = new Statements(); + + @Override + public boolean eq(ASTNode o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + + GoalSelector that = (GoalSelector) o; + + return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null; + } + } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/GuardedCaseStatement.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/GuardedCaseStatement.java index 6491cb47..4d6e6adb 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/GuardedCaseStatement.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/GuardedCaseStatement.java @@ -37,5 +37,15 @@ public class GuardedCaseStatement extends CaseStatement { return scs; } + @Override + public boolean eq(ASTNode o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + + GuardedCaseStatement that = (GuardedCaseStatement) o; + + return getGuard().eq(that.getGuard()); + } } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Parameters.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Parameters.java index 1fc44f11..236a4430 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Parameters.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Parameters.java @@ -23,7 +23,6 @@ package edu.kit.iti.formal.psdbg.parser.ast; */ - import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser; import edu.kit.iti.formal.psdbg.parser.Visitor; import lombok.EqualsAndHashCode; @@ -46,11 +45,13 @@ import java.util.function.Function; public class Parameters extends ASTNode { private final Map parameters = new LinkedHashMap<>(); - @Override public T accept(Visitor visitor) { + @Override + public T accept(Visitor visitor) { return visitor.visit(this); } - @Override public Parameters copy() { + @Override + public Parameters copy() { Parameters p = new Parameters(); forEach((k, v) -> p.put(k.copy(), v.copy())); p.setRuleContext(this.getRuleContext()); @@ -138,18 +139,38 @@ public class Parameters extends ASTNode } public Expression computeIfPresent(Variable key, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return parameters.computeIfPresent(key, remappingFunction); } public Expression compute(Variable key, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return parameters.compute(key, remappingFunction); } public Expression merge(Variable key, Expression value, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return parameters.merge(key, value, remappingFunction); } + @Override + public boolean eq(ASTNode o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + + Parameters that = (Parameters) o; + for (Map.Entry e : that.parameters.entrySet()) { + if (!e.getValue().eq(get(e.getKey()))) + return false; + } + + for (Map.Entry e : parameters.entrySet()) { + if (!e.getValue().eq(that.get(e.getKey()))) + return false; + } + + return true; + } + } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ProofScript.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ProofScript.java index 6526c539..b747ec94 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ProofScript.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ProofScript.java @@ -59,4 +59,18 @@ public class ProofScript extends ASTNode { } + @Override + public boolean eq(ASTNode o) { + if (this == o) return true; + if (!(o instanceof ProofScript)) return false; + if (!super.equals(o)) return false; + + ProofScript that = (ProofScript) o; + + if (getName() != null ? !getName().equals(that.getName()) : that.getName() != null) return false; + if (getSignature() != null ? !getSignature().eq(that.getSignature()) : that.getSignature() != null) + return false; + return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null; + } + } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/RepeatStatement.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/RepeatStatement.java index a2418324..68d1f22f 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/RepeatStatement.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/RepeatStatement.java @@ -59,4 +59,6 @@ public class RepeatStatement extends GoalSelector implements Map { private final Map sig = new LinkedHashMap<>(); - @Override public T accept(Visitor visitor) { + @Override + public T accept(Visitor visitor) { return visitor.visit(this); } - @Override public Signature copy() { + @Override + public Signature copy() { Signature signature = new Signature(); forEach((k, v) -> signature.put(k.copy(), v)); signature.setRuleContext(this.ruleContext); @@ -144,17 +145,17 @@ public class Signature extends ASTNode impl } public Type computeIfPresent(Variable key, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return sig.computeIfPresent(key, remappingFunction); } public Type compute(Variable key, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return sig.compute(key, remappingFunction); } public Type merge(Variable key, Type value, - BiFunction remappingFunction) { + BiFunction remappingFunction) { return sig.merge(key, value, remappingFunction); } } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java index 1425e31c..5b61d691 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java @@ -161,15 +161,18 @@ public class Statements extends ASTNode statements.forEach(action); } - @Override public String toString() { + @Override + public String toString() { return "Statements{" + "statements=" + statements + '}'; } - @Override public T accept(Visitor visitor) { + @Override + public T accept(Visitor visitor) { return visitor.visit(this); } - @Override public Statements copy() { + @Override + public Statements copy() { Statements s = new Statements(); forEach(e -> { Statement ecopy = e.copy(); @@ -180,4 +183,17 @@ public class Statements extends ASTNode return s; } + @Override + public boolean eq(ASTNode o) { + if (this == o) return true; + if (!(o instanceof Statements)) return false; + if (!super.equals(o)) return false; + Statements that = (Statements) o; + for (int i = 0; i < statements.size(); i++) { + if (!statements.get(i).eq(that.statements.get(i))) { + return false; + } + } + return true; + } } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TryCase.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TryCase.java index 00d2663c..73dbd469 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TryCase.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TryCase.java @@ -31,4 +31,6 @@ public class TryCase extends CaseStatement { tc.setRuleContext(this.getRuleContext()); return tc; } + + } diff --git a/lang/src/test/java/edu/kit/iti/formal/psdbg/parser/ASTDiffTest.java b/lang/src/test/java/edu/kit/iti/formal/psdbg/parser/ASTDiffTest.java new file mode 100644 index 00000000..13a7afe4 --- /dev/null +++ b/lang/src/test/java/edu/kit/iti/formal/psdbg/parser/ASTDiffTest.java @@ -0,0 +1,29 @@ +package edu.kit.iti.formal.psdbg.parser; + +import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; +import org.junit.Test; + +import java.io.File; +import java.io.IOException; +import java.util.List; + +import static org.junit.Assert.assertEquals; + +public class ASTDiffTest { + + private static final String PREFIX = "src/test/resources/edu/kit/iti/formal/psdbg/parser"; + + @Test + public void testDiff1() throws IOException { + List o = Facade.getAST(new File(PREFIX, "test_diff_1.kps")); + ASTDiff astDiff = new ASTDiff(); + ProofScript res = astDiff.diff(o.get(0), o.get(1)); + + assertEquals( + o.get(2).accept(new PrettyPrinter()), + res.accept(new PrettyPrinter()) + ); + } + + +} \ No newline at end of file diff --git a/lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/test_diff_1.kps b/lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/test_diff_1.kps new file mode 100644 index 00000000..c1a6b6cd --- /dev/null +++ b/lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/test_diff_1.kps @@ -0,0 +1,18 @@ +script A() { + A; + B; + C; + D; +} + +script A() { + A; + B; + C; + D; + E;F; +} + +script A() { + E;F; +} diff --git a/lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/test_diff_2.kps b/lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/test_diff_2.kps new file mode 100644 index 00000000..a89d4c94 --- /dev/null +++ b/lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/test_diff_2.kps @@ -0,0 +1,21 @@ +script A() { + A; + B; + C; + cases { + case x=2: + a; + + } +} + +script A() { + A; + B; + C; + F; +} + +script A() { + E;F; +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java index 796e598f..52fbb7e4 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java @@ -71,12 +71,12 @@ public class KeYProofFacade { /** * reload the current proof. synchronously because only the first load is slow. */ - public void reload() throws ProofInputException, ProblemLoaderException { + public void reload(File problemFile) throws ProofInputException, ProblemLoaderException { if (contract.get() != null) {// reinstante the contract setProof(getEnvironment().createProof( contract.get().getProofObl(getEnvironment().getServices()))); } else { - setProof(KeYApi.loadFromKeyFile(proof.get().getProofFile()).getLoadedProof().getProof()); + setProof(KeYApi.loadFromKeyFile(problemFile).getLoadedProof().getProof()); } } diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java index f744af53..fd59d84b 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java @@ -16,6 +16,8 @@ import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicabl import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import lombok.Getter; import lombok.RequiredArgsConstructor; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; import org.key_project.util.collection.ImmutableList; import java.util.HashMap; @@ -27,6 +29,8 @@ import java.util.Map; */ @RequiredArgsConstructor public class RuleCommandHandler implements CommandHandler { + private static final Logger LOGGER = LogManager.getLogger(RuleCommandHandler.class); + @Getter private final Map rules; @@ -53,7 +57,7 @@ public class RuleCommandHandler implements CommandHandler { KeyData kd = expandedNode.getData(); Map map = new HashMap<>(); params.asMap().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString())); - System.out.println(map); + LOGGER.info("Execute {} with {}", call, map); try { map.put("#2", call.getCommand()); EngineState estate = new EngineState(kd.getProof()); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index dabc798d..ca974570 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -19,10 +19,12 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.dbg.*; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; import javafx.application.Platform; +import javafx.beans.binding.BooleanBinding; import javafx.collections.FXCollections; import javafx.concurrent.Service; import javafx.concurrent.Task; import javafx.event.ActionEvent; +import javafx.event.EventHandler; import javafx.fxml.FXML; import javafx.fxml.Initializable; import javafx.scene.control.*; @@ -76,6 +78,36 @@ public class DebuggerMain implements Initializable { @FXML private DockPane dockStation; + @FXML + private ToggleButton togBtnCommandHelp; + + @FXML + private ToggleButton togBtnProofTree; + + @FXML + private ToggleButton togBtnActiveInspector; + + @FXML + private ToggleButton togBtnWelcome; + + @FXML + private ToggleButton togBtnCodeDock; + + @FXML + private CheckMenuItem miCommandHelp; + + @FXML + private CheckMenuItem miCodeDock; + + @FXML + private CheckMenuItem miWelcomeDock; + + @FXML + private CheckMenuItem miActiveInspector; + + @FXML + private CheckMenuItem miProofTree; + private JavaArea javaArea = new JavaArea(); private DockNode javaAreaDock = new DockNode(javaArea, "Java Source", @@ -135,6 +167,33 @@ public class DebuggerMain implements Initializable { Utils.addDebugListener(model.executeNotPossibleProperty(), "executeNotPossible"); scriptController.mainScriptProperty().bindBidirectional(statusBar.mainScriptIdentifierProperty()); initializeExamples(); + + + dockingNodeHandling(togBtnActiveInspector, + miActiveInspector, + activeInspectorDock, + DockPos.CENTER); + + dockingNodeHandling(togBtnCodeDock, + miCodeDock, + javaAreaDock, + DockPos.RIGHT); + + dockingNodeHandling(togBtnCommandHelp, + miCommandHelp, + commandHelpDock, + DockPos.RIGHT); + + dockingNodeHandling(togBtnWelcome, + miWelcomeDock, + welcomePaneDock, + DockPos.CENTER); + + dockingNodeHandling(togBtnProofTree, + miProofTree, + proofTreeDock, + DockPos.LEFT); + } @@ -254,6 +313,27 @@ public class DebuggerMain implements Initializable { } } + public void dockingNodeHandling(ToggleButton btn, CheckMenuItem cmi, DockNode dn, DockPos defaultPosition) { + BooleanBinding prop = dn.dockedProperty().or(dn.floatingProperty()); + prop.addListener((p, o, n) -> { + btn.setSelected(n); + cmi.setSelected(n); + }); + + EventHandler handler = event -> { + if (!prop.get()) { + if (dn.getLastDockPos() != null) + dn.dock(dockStation, dn.getLastDockPos()); + else + dn.dock(dockStation, defaultPosition); + } else { + dn.undock(); + } + }; + btn.setOnAction(handler); + cmi.setOnAction(handler); + } + @FXML public void executeScript() { executeScript(false); @@ -304,9 +384,9 @@ public class DebuggerMain implements Initializable { if (FACADE.getProofState() == KeYProofFacade.ProofState.DIRTY) { try { - FACADE.reload(); + FACADE.reload(model.getKeyFile()); } catch (ProofInputException | ProblemLoaderException e) { - //TODO + LOGGER.error(e); Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment", e ); @@ -356,6 +436,7 @@ public class DebuggerMain implements Initializable { model.setDebuggerFramework(df); } catch (RecognitionException e) { + LOGGER.error(e); Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); } } @@ -389,6 +470,7 @@ public class DebuggerMain implements Initializable { task.setOnFailed(event -> { statusBar.stopProgress(); event.getSource().exceptionProperty().get(); + Utils.showExceptionDialog("Could not load sourceName", "Key sourceName loading error", "", (Throwable) event.getSource().exceptionProperty().get() ); @@ -490,6 +572,7 @@ public class DebuggerMain implements Initializable { String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset()); ScriptArea area = scriptController.createNewTab(scriptFile); } catch (IOException e) { + LOGGER.error(e); Utils.showExceptionDialog("Exception occured", "", "Could not load sourceName " + scriptFile, e); } @@ -500,6 +583,7 @@ public class DebuggerMain implements Initializable { try { scriptController.saveCurrentScript(); } catch (IOException e) { + LOGGER.error(e); Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save current script", e); } @@ -537,6 +621,7 @@ public class DebuggerMain implements Initializable { try { scriptController.saveCurrentScriptAs(scriptFile); } catch (IOException e) { + LOGGER.error(e); Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save to file " + scriptFile.getName(), e); } } @@ -561,6 +646,7 @@ public class DebuggerMain implements Initializable { public void stepOver(ActionEvent actionEvent) { LOGGER.debug("DebuggerMain.stepOver"); try { + assert model.getDebuggerFramework() != null : "You should have started the prove"; model.getDebuggerFramework().execute(new StepOverCommand<>()); } catch (DebuggerException e) { Utils.showExceptionDialog("", "", "", e); @@ -571,6 +657,7 @@ public class DebuggerMain implements Initializable { /** * Perform a step into + * * @param actionEvent */ public void stepInto(ActionEvent actionEvent) { @@ -610,7 +697,7 @@ public class DebuggerMain implements Initializable { @FXML public void showWelcomeDock(ActionEvent actionEvent) { - if (!welcomePaneDock.isDocked()) { + if (!welcomePaneDock.isDocked() && !welcomePaneDock.isFloating()) { welcomePaneDock.dock(dockStation, DockPos.CENTER); } } @@ -690,6 +777,7 @@ public class DebuggerMain implements Initializable { FACADE.activateContract(result); getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals()); } catch (ProofInputException e) { + LOGGER.error(e); Utils.showExceptionDialog("", "", "", e); } }); @@ -697,6 +785,7 @@ public class DebuggerMain implements Initializable { @Override protected void failed() { + LOGGER.error(exceptionProperty().get()); Utils.showExceptionDialog("", "", "", exceptionProperty().get()); } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java index b863e29f..06f71447 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java @@ -73,6 +73,7 @@ public class SequentView extends CodeArea { hightlightRange(0, 0); } } catch (NullPointerException npe) { + npe.printStackTrace(); } mouseEvent.consume(); } @@ -130,6 +131,7 @@ public class SequentView extends CodeArea { Sequent sequent = node.get().sequent(); filter = new IdentitySequentPrintFilter(); + filter.setSequent(sequent); ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter()); this.backend = new LogicPrinter.PosTableStringBackend(80); diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps index b5fc44ae..b2bb9f36 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/agatha/script.kps @@ -3,8 +3,6 @@ script agascript() { andLeft; notLeft; - repeat { andLeft; } - andLeft; andLeft; andLeft; diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml index 2d7319d2..d658e322 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml @@ -65,31 +65,31 @@ - + - - + + - - + + - - + + - - + + - + @@ -194,7 +194,7 @@