diff --git a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java index 4b88f1097806432678c5c33fe539f8b565e920dd..72d2fd01cb986078435a3feb56fc74fbc9a8ec25 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -1,5 +1,6 @@ package edu.kit.formal.gui.controller; +import com.google.common.eventbus.Subscribe; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; import de.uka.ilkd.key.proof.init.ProofInputException; @@ -18,6 +19,7 @@ import javafx.beans.property.*; import javafx.beans.value.ChangeListener; import javafx.beans.value.ObservableBooleanValue; import javafx.beans.value.ObservableValue; +import javafx.collections.FXCollections; import javafx.concurrent.Service; import javafx.concurrent.Task; import javafx.event.ActionEvent; @@ -51,12 +53,12 @@ import java.util.concurrent.Executors; * @author Alexander Weigl */ public class DebuggerMainWindowController implements Initializable { + public static final KeYProofFacade FACADE = new KeYProofFacade(); protected static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class); + public final ContractLoaderService contractLoaderService = new ContractLoaderService(); private final ProofTreeController proofTreeController = new ProofTreeController(); private final InspectionViewsController inspectionViewsController = new InspectionViewsController(); private final ExecutorService executorService = Executors.newFixedThreadPool(2); - public static final KeYProofFacade FACADE = new KeYProofFacade(); - public final ContractLoaderService contractLoaderService = new ContractLoaderService(); /** * Property: current loaded javaFile */ @@ -70,8 +72,10 @@ public class DebuggerMainWindowController implements Initializable { */ private final ObjectProperty chosenContract = new SimpleObjectProperty<>(this, "chosenContract"); private ScriptController scriptController; + @FXML private DebuggerStatusBar statusBar; + @FXML private DockPane dockStation; private JavaArea javaArea = new JavaArea(); @@ -107,6 +111,8 @@ public class DebuggerMainWindowController implements Initializable { @Override public void initialize(URL location, ResourceBundle resources) { + Events.register(this); + setDebugMode(false); scriptController = new ScriptController(dockStation); @@ -115,12 +121,14 @@ public class DebuggerMainWindowController implements Initializable { registerToolbarToStatusBar(); marriageProofTreeControllerWithActiveInspectionView(); //statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a")); - + marriageJavaCode(); //Debugging Utils.addDebugListener(javaCode); Utils.addDebugListener(executeNotPossible, "executeNotPossible"); + scriptController.mainScriptProperty().bindBidirectional(statusBar.mainScriptIdentifierProperty()); + } /** @@ -133,20 +141,29 @@ public class DebuggerMainWindowController implements Initializable { proofTreeController.currentGoalsProperty().addListener((o, old, fresh) -> { if (fresh != null) { imodel.setGoals(fresh); + } else { + // no goals, set an empty list + imodel.setGoals(FXCollections.observableArrayList()); } }); proofTreeController.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> { - if (newValue != null) { - imodel.setCurrentInterpreterGoal(newValue); - } + imodel.setCurrentInterpreterGoal(newValue); + //also update the selected to be shown + imodel.setSelectedGoalNodeToShow(newValue); }); proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> { scriptController.getDebugPositionHighlighter().highlight(newValue); }); - javaFileProperty().addListener((observable, oldValue, newValue) -> { + Utils.addDebugListener(proofTreeController.currentGoalsProperty(), Utils::reprKeyDataList); + Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty(), Utils::reprKeyData); + Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty()); + } + + public void marriageJavaCode() { + /*javaFileProperty().addListener((observable, oldValue, newValue) -> { showCodeDock(null); try { String code = FileUtils.readFileToString(newValue, Charset.defaultCharset()); @@ -154,8 +171,14 @@ public class DebuggerMainWindowController implements Initializable { } catch (IOException e) { e.printStackTrace(); } + });*/ + + chosenContract.addListener(o -> { + javaCode.set(Utils.getJavaCode(chosenContract.get())); + showCodeDock(null); }); + javaCode.addListener(new ChangeListener() { @Override public void changed(ObservableValue observable, String oldValue, String newValue) { @@ -166,11 +189,10 @@ public class DebuggerMainWindowController implements Initializable { } } }); - Utils.addDebugListener(proofTreeController.currentGoalsProperty()); - Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty()); - Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty()); + } + /** * If the mouse moves other toolbar button, the help text should display in the status bar */ diff --git a/src/main/java/edu/kit/formal/gui/controller/Events.java b/src/main/java/edu/kit/formal/gui/controller/Events.java index 1bf96c64b6ec784c7774e28d81e77dda1183d909..e7d302f26484c6cd32d8e57a5deeb78f39465df8 100644 --- a/src/main/java/edu/kit/formal/gui/controller/Events.java +++ b/src/main/java/edu/kit/formal/gui/controller/Events.java @@ -1,6 +1,8 @@ package edu.kit.formal.gui.controller; import com.google.common.eventbus.EventBus; +import edu.kit.formal.gui.controls.ScriptArea; +import lombok.Data; /** * See http://codingjunkie.net/guava-eventbus/ for an introduction. @@ -10,11 +12,24 @@ import com.google.common.eventbus.EventBus; public class Events { public static final EventBus GLOBAL_EVENT_BUS = new EventBus(); - public void register(Object object) { + public static void register(Object object) { GLOBAL_EVENT_BUS.register(object); } - public void unregister(Object object) { + public static void unregister(Object object) { GLOBAL_EVENT_BUS.unregister(object); } + + public static void fire(Object focusScriptArea) { + GLOBAL_EVENT_BUS.post(focusScriptArea); + } + + @Data + public static class FocusScriptArea { + private final ScriptArea scriptArea; + + public FocusScriptArea(ScriptArea area) { + this.scriptArea = area; + } + } } diff --git a/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java b/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java index 1893087c8dd8491935a9e2ddf3728f1577415039..400eb75ac252d006b8cf8d870f65b7672a80bb75 100644 --- a/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java +++ b/src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java @@ -89,7 +89,7 @@ public class PuppetMaster { * Publish state is called after the interpreter or debugger thread terminated. The resulting goals are set in the root model */ public void publishState() { - System.out.println("PuppetMaster.publishState"); + //("PuppetMaster.publishState"); //puppet is null if successful interpreter state and publish state if (puppet != null) { diff --git a/src/main/java/edu/kit/formal/gui/controls/DebuggerStatusBar.java b/src/main/java/edu/kit/formal/gui/controls/DebuggerStatusBar.java index d11cd1cd74d014b0d29a508f88f50d6394504718..de9319c5f57c6acc12163e9e8e50d34d4c5cf28d 100644 --- a/src/main/java/edu/kit/formal/gui/controls/DebuggerStatusBar.java +++ b/src/main/java/edu/kit/formal/gui/controls/DebuggerStatusBar.java @@ -2,10 +2,9 @@ package edu.kit.formal.gui.controls; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; -import javafx.beans.property.ListProperty; -import javafx.beans.property.SimpleListProperty; -import javafx.beans.property.SimpleObjectProperty; -import javafx.beans.property.SimpleStringProperty; +import edu.kit.formal.gui.controller.Events; +import edu.kit.formal.gui.model.MainScriptIdentifier; +import javafx.beans.property.*; import javafx.beans.value.ObservableStringValue; import javafx.collections.FXCollections; import javafx.collections.ObservableList; @@ -33,22 +32,23 @@ import java.util.LinkedList; */ public class DebuggerStatusBar extends StatusBar { private static final Logger LOGGER = LogManager.getLogger(DebuggerStatusBar.class); - + private final Appender loggerHandler = createAppender(); + private final ContextMenu contextMenu = createContextMenu(); + private ObjectProperty mainScriptIdentifier = new SimpleObjectProperty<>(); private Label lblCurrentNodes = new Label("#nodes: %s"); + private Label lblMainscript = new Label(); private ProgressIndicator progressIndicator = new ProgressIndicator(); private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX(); + private final Dialog loggerDialog = createDialog(); private EventHandler toolTipHandler = event -> { publishMessage(((Control) event.getTarget()).getTooltip().getText()); }; - - private final ContextMenu contextMenu = createContextMenu(); - private final Dialog loggerDialog = createDialog(); - public DebuggerStatusBar() { listenOnField("psdbg"); getRightItems().addAll( + lblMainscript, lblCurrentNodes, progressIndicator ); @@ -60,9 +60,32 @@ public class DebuggerStatusBar extends StatusBar { }); - } + mainScriptIdentifier.addListener((ov, o, n) -> { + if (n != null) { + lblMainscript.setText("Main Script: " + + n.getScriptArea().getFilePath().getName() + + (n.getScriptName() != null + ? '\\' + n.getScriptName() + : " @ " + n.getLineNumber())); + lblMainscript.setStyle("-fx-background-color: greenyellow;-fx-padding: 5pt;"); + } else { + lblMainscript.setStyle("-fx-background-color: orangered;-fx-padding: 5pt;"); + lblMainscript.setText("No main script selected"); + } + }); - private final Appender loggerHandler = createAppender(); + lblMainscript.setStyle("-fx-background-color: orangered;-fx-padding: 5pt;"); + lblMainscript.setText("No main script selected"); + + lblMainscript.setOnMouseClicked(event -> { + if (event.getClickCount() == 2) { + event.consume(); + ScriptArea area = mainScriptIdentifier.get().getScriptArea(); + Events.fire(new Events.FocusScriptArea(area)); + } + }); + + } private Appender createAppender() { PatternLayout layout = PatternLayout.createDefaultLayout(); @@ -117,6 +140,18 @@ public class DebuggerStatusBar extends StatusBar { return cm; } + public MainScriptIdentifier getMainScriptIdentifier() { + return mainScriptIdentifier.get(); + } + + public void setMainScriptIdentifier(MainScriptIdentifier mainScriptIdentifier) { + this.mainScriptIdentifier.set(mainScriptIdentifier); + } + + public ObjectProperty mainScriptIdentifierProperty() { + return mainScriptIdentifier; + } + private void showLog(ActionEvent actionEvent) { loggerDialog.show(); } @@ -192,14 +227,14 @@ public class DebuggerStatusBar extends StatusBar { return records.get(); } - public ListProperty recordsProperty() { - return records; - } - public void setRecords(ObservableList records) { this.records.set(records); } + public ListProperty recordsProperty() { + return records; + } + public int getMaxRecords() { return maxRecords; } diff --git a/src/main/java/edu/kit/formal/gui/controls/InspectionView.java b/src/main/java/edu/kit/formal/gui/controls/InspectionView.java index cd7a0d6d8154041e5bff5757eb8343c6a2a502bf..ef9eac30480c25edfc283854a0fdbdc38c3a38c8 100644 --- a/src/main/java/edu/kit/formal/gui/controls/InspectionView.java +++ b/src/main/java/edu/kit/formal/gui/controls/InspectionView.java @@ -35,15 +35,19 @@ public class InspectionView extends BorderPane { public InspectionView() { Utils.createWithFXML(this); - model.get().selectedGoalNodeToShowProperty().bind( - goalView.getSelectionModel().selectedItemProperty() - ); + model.get().selectedGoalNodeToShowProperty().addListener((o, a, b) -> { + goalView.getSelectionModel().select(b); + }); + goalView.getSelectionModel().selectedItemProperty().addListener((o, a, b) -> { + model.get().setSelectedGoalNodeToShow(b); + }); model.get().selectedGoalNodeToShowProperty().addListener( (observable, oldValue, newValue) -> { goalView.getSelectionModel().select(newValue); if (newValue != null && newValue.getData() != null) { - getSequentView().setNode(newValue.getData().getGoal()); + getSequentView().setNode(newValue.getData().getNode()); + getSequentView().setGoal(newValue.getData().getGoal()); // TODO weigl: get marked lines of the program, and set it model.get().highlightedJavaLinesProperty().get() .clear(); @@ -83,6 +87,14 @@ public class InspectionView extends BorderPane { goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY()); } + public InspectionModel getModel() { + return model.get(); + } + + public ReadOnlyObjectProperty modelProperty() { + return model; + } + /** * Cells for GoalView */ @@ -106,12 +118,4 @@ public class InspectionView extends BorderPane { setText(text); } } - - public InspectionModel getModel() { - return model.get(); - } - - public ReadOnlyObjectProperty modelProperty() { - return model; - } } diff --git a/src/main/java/edu/kit/formal/gui/controls/ScriptController.java b/src/main/java/edu/kit/formal/gui/controls/ScriptController.java index cf06c1fe6a4e14721cab2e6021e99ffc42c87399..48a441d91075b5b8020fc54575307084a1cc7ffa 100644 --- a/src/main/java/edu/kit/formal/gui/controls/ScriptController.java +++ b/src/main/java/edu/kit/formal/gui/controls/ScriptController.java @@ -1,7 +1,9 @@ package edu.kit.formal.gui.controls; +import com.google.common.eventbus.Subscribe; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; +import edu.kit.formal.gui.controller.Events; import edu.kit.formal.gui.model.Breakpoint; import edu.kit.formal.gui.model.MainScriptIdentifier; import edu.kit.formal.proofscriptparser.Facade; @@ -21,6 +23,7 @@ import org.apache.logging.log4j.Logger; import org.dockfx.DockNode; import org.dockfx.DockPane; import org.dockfx.DockPos; +import sun.reflect.generics.reflectiveObjects.NotImplementedException; import java.io.File; import java.io.IOException; @@ -44,6 +47,13 @@ public class ScriptController { public ScriptController(DockPane parent) { this.parent = parent; + Events.register(this); + } + + @Subscribe public void handle(Events.FocusScriptArea fsa) { + logger.debug("FocusScriptArea handled!"); + openScripts.get(fsa.getScriptArea()).focus(); + fsa.getScriptArea().requestFocus(); } public ObservableMap getOpenScripts() { @@ -111,7 +121,7 @@ public class ScriptController { this.lastScriptArea = area; area.focusedProperty().addListener((observable, oldValue, newValue) -> { - System.out.println("area = [" + area + "]"); + logger.debug("area = [" + area + "]"); if (newValue) lastScriptArea = area; }); @@ -168,7 +178,19 @@ public class ScriptController { } public void saveCurrentScript() { - //TODO + throw new NotImplementedException(); + } + + public MainScriptIdentifier getMainScript() { + return mainScript.get(); + } + + public ObjectProperty mainScriptProperty() { + return mainScript; + } + + public void setMainScript(MainScriptIdentifier mainScript) { + this.mainScript.set(mainScript); } private ScriptArea findEditor(ASTNode node) { @@ -186,13 +208,20 @@ public class ScriptController { } public void remove() { - if (lastScriptArea != null) + logger.debug("remove highlight"); + if (lastScriptArea != null) { + logger.debug("previous highlight on {} for {}", lastScriptArea, lastRegion); lastScriptArea.getMarkedRegions().remove(lastRegion); + } } public void highlight(ASTNode node) { + logger.debug("Highlight requested for {}", node); remove(); + ScriptArea.RegionStyle r = asRegion(node); + logger.debug("Region for highlighting: {}", r); + ScriptArea area = findEditor(node); area.getMarkedRegions().add(r); diff --git a/src/main/java/edu/kit/formal/gui/controls/SequentView.java b/src/main/java/edu/kit/formal/gui/controls/SequentView.java index 5313243e93b53347aca8710da63195fd64c8d5b4..0898e791fed4f412f142ad82bdf7aaa4035ff2d2 100644 --- a/src/main/java/edu/kit/formal/gui/controls/SequentView.java +++ b/src/main/java/edu/kit/formal/gui/controls/SequentView.java @@ -5,10 +5,12 @@ import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.pp.*; import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.settings.ProofIndependentSettings; import edu.kit.formal.interpreter.KeYProofFacade; import javafx.beans.Observable; import javafx.beans.property.SimpleObjectProperty; +import javafx.beans.value.ObservableBooleanValue; import javafx.scene.input.MouseButton; import javafx.scene.input.MouseEvent; import javafx.scene.layout.*; @@ -28,7 +30,9 @@ public class SequentView extends CodeArea { private LogicPrinter lp; private IdentitySequentPrintFilter filter; private LogicPrinter.PosTableStringBackend backend; - private SimpleObjectProperty node = new SimpleObjectProperty<>(); + private SimpleObjectProperty goal = new SimpleObjectProperty<>(); + private SimpleObjectProperty node = new SimpleObjectProperty<>(); + private ObservableBooleanValue rulesAvailable = goal.isNotNull(); private KeYProofFacade keYProofFacade; private TacletContextMenu menu; @@ -63,13 +67,13 @@ public class SequentView extends CodeArea { if (backend == null) { return; } - if (e.getButton() == MouseButton.SECONDARY) { + if (e.getButton() == MouseButton.SECONDARY && rulesAvailable.get()) { CharacterHit hit = hit(e.getX(), e.getY()); int insertionPoint = hit.getInsertionIndex(); PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter); if (pis == null) return; - menu = new TacletContextMenu(keYProofFacade, pis, node.get()); + menu = new TacletContextMenu(keYProofFacade, pis, goal.get()); menu.setAutoFix(true); menu.setAutoHide(true); menu.show(this, e.getScreenX(), e.getScreenY()); @@ -125,24 +129,36 @@ public class SequentView extends CodeArea { clear(); insertText(0, backend.getString()); - if (node.get().node().isClosed()) { + if (node.get().isClosed()) { this.setBorder(new Border(new BorderStroke(Color.RED, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT))); this.getStyleClass().add("closed-sequent-view"); } } - public Goal getNode() { - return node.get(); + public Goal getGoal() { + return goal.get(); } - public SimpleObjectProperty nodeProperty() { - return node; + public void setGoal(Goal goal) { + this.goal.set(goal); + } + + public SimpleObjectProperty goalProperty() { + return goal; + } + + public Node getNode() { + return node.get(); } - public void setNode(Goal node) { + public void setNode(Node node) { this.node.set(node); } + public SimpleObjectProperty nodeProperty() { + return node; + } + public KeYProofFacade getKeYProofFacade() { return keYProofFacade; } @@ -150,4 +166,6 @@ public class SequentView extends CodeArea { public void setKeYProofFacade(KeYProofFacade keYProofFacade) { this.keYProofFacade = keYProofFacade; } + + } diff --git a/src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java b/src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java index 523c6f385cf6540cdc7124228f30bf9806053d49..c513b2418732ad3721ec7690ceb9ec578afc7d09 100644 --- a/src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java +++ b/src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java @@ -14,6 +14,7 @@ import edu.kit.formal.gui.controller.DebuggerMainWindowController; import edu.kit.formal.interpreter.KeYProofFacade; import javafx.event.ActionEvent; import javafx.fxml.FXML; +import javafx.scene.Node; import javafx.scene.control.ContextMenu; import javafx.scene.control.Menu; import javafx.scene.control.MenuItem; diff --git a/src/main/java/edu/kit/formal/gui/controls/Utils.java b/src/main/java/edu/kit/formal/gui/controls/Utils.java index e3c127608cd1c2c3bd6626c00f01700e0a198548..6f724f5e7e9299a78478a5b3598ca00a9ab0fc21 100644 --- a/src/main/java/edu/kit/formal/gui/controls/Utils.java +++ b/src/main/java/edu/kit/formal/gui/controls/Utils.java @@ -3,10 +3,13 @@ package edu.kit.formal.gui.controls; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.pp.ProgramPrinter; import de.uka.ilkd.key.speclang.Contract; +import edu.kit.formal.interpreter.data.GoalNode; +import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.proofscriptparser.ScriptLanguageLexer; import javafx.beans.property.Property; import javafx.beans.value.ChangeListener; import javafx.beans.value.ObservableValue; +import javafx.collections.ObservableList; import javafx.fxml.FXMLLoader; import javafx.scene.control.Alert; import javafx.scene.control.Label; @@ -190,9 +193,13 @@ public class Utils { } public static void addDebugListener(Property property, java.util.function.Function conv) { - property.addListener((observable, oldValue, newValue) -> - logger.debug("Property '{}' of '%s' changed from {} to {}", property.getName(), - property.getBean().getClass().getSimpleName(), conv.apply(oldValue), conv.apply(newValue))); + property.addListener((observable, oldValue, newValue) -> { + String simpleName = property.getBean() != null ? property.getBean().getClass().getSimpleName() : ""; + logger.debug("Property '{}' of '{}' changed from {} to {}", property.getName(), + simpleName, + oldValue == null ? "" : conv.apply(oldValue), + newValue == null ? "" : conv.apply(newValue)); + }); } public static void addDebugListener(ObservableValue o, String id) { @@ -213,4 +220,15 @@ public class Utils { } return null; } + + public static String reprKeyDataList(ObservableList> kd) { + return kd.stream() + .map(Utils::reprKeyData) + .reduce((a, b) -> a + b) + .orElse(""); + } + + public static String reprKeyData(GoalNode t) { + return String.valueOf(t.getData().getNode().serialNr()); + } } diff --git a/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java b/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java index d03b75872462f362e2a6ffaaab9d3f159a9012ca..4f77570e8dd3967ac8bfd1c22ba9eab9d64ca3b1 100644 --- a/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java +++ b/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java @@ -21,7 +21,8 @@ public class WelcomePane extends AnchorPane { proofScriptDebugger.getWelcomePaneDock().close(); proofScriptDebugger.showActiveInspector(null); proofScriptDebugger.openScript( - new File("src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps") + // new File("src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps") + new File("src/test/resources/edu/kit/formal/interpreter/contraposition/wo_branching.kps") ); proofScriptDebugger.openKeyFile( diff --git a/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java b/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java index 54899b55c3b977dace15d0fcc46af106e97380aa..9836e2c5622627e305561bdeb3a97649cc530162 100644 --- a/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java +++ b/src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java @@ -161,7 +161,7 @@ public class InterpreterBuilder { @Override public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { - System.out.println("InterpreterBuilder.evaluate"); + //System.out.println("InterpreterBuilder.evaluate"); } }; lookup.getBuilders().add(0, ignoreHandler); diff --git a/src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java b/src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java index c41cccd7f9ddf5d4a324e652957853cf704c139b..4ef54ebeacb36262728fdb6b2971ee5322167260 100644 --- a/src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java +++ b/src/main/java/edu/kit/formal/interpreter/MatchEvaluator.java @@ -7,6 +7,7 @@ import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.ast.*; import lombok.Getter; +import org.apache.commons.lang.NotImplementedException; import java.util.ArrayList; import java.util.Collections; @@ -90,9 +91,8 @@ public class MatchEvaluator extends DefaultASTVisitor> case NEQ: return null; default: - System.out.println("Need to be implemented"); + throw new NotImplementedException("Need to be implemented"); } - return null; } /** diff --git a/src/main/java/edu/kit/formal/interpreter/data/KeyData.java b/src/main/java/edu/kit/formal/interpreter/data/KeyData.java index 9d44bd1e71ad8f1536c3985cb56f74bd9ccc4485..a411dc676abccc8c52b7a07276aa2986ce2b98f8 100644 --- a/src/main/java/edu/kit/formal/interpreter/data/KeyData.java +++ b/src/main/java/edu/kit/formal/interpreter/data/KeyData.java @@ -27,6 +27,8 @@ public class KeyData { programLinesLabel, programStatementsLabel, nameLabel; + + private Node node; private Goal goal; public KeyData(KeyData data, Goal node) { @@ -35,6 +37,7 @@ public class KeyData { //scriptApi = data.scriptApi; this.proof = data.proof; this.goal = node; + this.node = goal.node(); } public KeyData(Goal g, KeYEnvironment environment, Proof proof) { @@ -45,10 +48,11 @@ public class KeyData { public KeyData(Node root, KeYEnvironment environment, Proof proof) { this(proof.getGoal(root), environment, proof); + node = root; } public KeyData(KeyData kd, Node node) { - this(kd, kd.getProof().getGoal(node)); + this(node, kd.getEnv(), kd.getProof()); } public String getRuleLabel() { diff --git a/src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java b/src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java index f8bded41d4db122860ffd5489efc5196113078bc..bd0332cc69fca5f6c05913ddd22d416407f86385 100644 --- a/src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java +++ b/src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java @@ -48,7 +48,7 @@ public class ProofScriptCommandBuilder 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); + //System.out.println(map); try { EngineState estate = new EngineState(kd.getProof()); estate.setGoal(kd.getNode()); diff --git a/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java b/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java index 98821d724c66590204c7393749bfcbbd3fde3b30..15b7e43d30f1d0d6e981ad033b68e874c954e2f8 100644 --- a/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java @@ -243,10 +243,10 @@ public class ProofTreeController { * @param state */ private void setNewState(State state) { - setCurrentGoals(state.getGoals()); - setCurrentSelectedGoal(state.getSelectedGoalNode()); + setCurrentGoals(state==null? null : state.getGoals()); + setCurrentSelectedGoal(state==null?null:state.getSelectedGoalNode()); setCurrentHighlightNode(statePointer.getScriptstmt()); - LOGGER.debug("New State from this command: %s@%s", + LOGGER.debug("New State from this command: {}@{}", this.statePointer.getScriptstmt().getNodeName(), this.statePointer.getScriptstmt().getStartPosition()); }