Commit 89d49cfb authored by Sarah Grebing's avatar Sarah Grebing

coping with closed nodes visaully

parent 72cc4c20
Pipeline #11192 failed with stage
in 3 minutes and 17 seconds
......@@ -7,12 +7,10 @@ import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.InterpreterBuilder;
import edu.kit.formal.interpreter.KeYProofFacade;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.ast.ProofScript;
import javafx.beans.Observable;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.beans.value.ObservableBooleanValue;
......@@ -22,9 +20,7 @@ import javafx.concurrent.Task;
import javafx.event.ActionEvent;
import javafx.fxml.FXML;
import javafx.fxml.Initializable;
import javafx.scene.Node;
import javafx.scene.control.*;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.GridPane;
import javafx.scene.layout.Pane;
import javafx.scene.layout.Priority;
......@@ -93,8 +89,7 @@ public class DebuggerMainWindowController implements Initializable {
/***********************************************************************************************************
* GoalView
* **********************************************************************************************************/
//@FXML
//private ListView<GoalNode<KeyData>> goalView;
@FXML
private InspectionViewTabPane inspectionViewTabPane;
private ExecutorService executorService = Executors.newFixedThreadPool(2);
......@@ -112,11 +107,6 @@ public class DebuggerMainWindowController implements Initializable {
private File initialDirectory;
// @FXML
// private JavaArea javaSourceCode;
//@FXML
//private SequentView sequentView;
private InterpretingService interpreterService = new InterpretingService();
......@@ -169,6 +159,10 @@ public class DebuggerMainWindowController implements Initializable {
model.scriptFileProperty().addListener((observable, oldValue, newValue) -> {
statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
});
/**
* create a new insepctionviewtab that is the main tab and not closable
*/
inspectionViewTabPane.createNewInspectionViewTab(model, true);
......@@ -217,6 +211,12 @@ public class DebuggerMainWindowController implements Initializable {
}
//endregion
/**
* Execute the script that with using the interpreter that is build using teh interpreterbuilder
*
* @param ib
* @param debugMode
*/
private void executeScript(InterpreterBuilder ib, boolean debugMode) {
this.debugMode.set(debugMode);
blocker.deinstall();
......@@ -388,10 +388,7 @@ public class DebuggerMainWindowController implements Initializable {
blocker.unlock();
}
public void showGoalOptions(MouseEvent actionEvent) {
Node n = (Node) actionEvent.getTarget();
goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
}
public KeYProofFacade getFacade() {
return facade;
......@@ -449,26 +446,7 @@ public class DebuggerMainWindowController implements Initializable {
}
}
private class GoalNodeListCell extends ListCell<GoalNode<KeyData>> {
public GoalNodeListCell(ListView<GoalNode<KeyData>> goalNodeListView) {
itemProperty().addListener(this::update);
goalOptionsMenu.selectedViewOptionProperty().addListener(this::update);
}
private void update(Observable observable) {
if (getItem() == null) {
setText("");
return;
}
KeyData item = getItem().getData();
String text = "n/a";
if (goalOptionsMenu.getSelectedViewOption() != null) {
text = goalOptionsMenu.getSelectedViewOption().getText(item);
}
setText(text);
}
}
private class InterpretingService extends Service<State<KeyData>> {
private final SimpleObjectProperty<Interpreter<KeyData>> interpreter = new SimpleObjectProperty<>();
......
......@@ -73,16 +73,21 @@ public class PuppetMaster {
return null;
}
/**
* Publish state is called after the interpreter or debugger thread terminated. The resulting goals are set in teh root model
*/
public void publishState() {
System.out.println("PuppetMaster.publishState");
//puppet is null if sucessful interprter state and publish state
//puppet is null if sucessful interpreter state and publish state
if (puppet != null) {
final State<KeyData> state = puppet.getCurrentState().copy();
System.out.println(state);
Platform.runLater(() -> {
currentGoals.set(state.getGoals());
currentSelectedGoal.set(state.getSelectedGoalNode());
});
} else {
//if puppet is null an empty state may be reached therefore state get goals etc returns null
......
......@@ -23,6 +23,7 @@ import java.util.ResourceBundle;
/**
* Right part of the splitpane that displays the different parts of a state
* @author S. Grebing
*/
public class InspectionViewTab extends Tab implements Initializable {
......@@ -34,6 +35,7 @@ public class InspectionViewTab extends Tab implements Initializable {
@FXML
private ListView goalView;
public InspectionViewTab() {
super();
FXMLLoader loader = new FXMLLoader(getClass().getResource("InspectionView.fxml"));
......@@ -100,6 +102,7 @@ public class InspectionViewTab extends Tab implements Initializable {
getGoalView().getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> {
getSequentView().setNode(newValue.getData().getNode());
});
getGoalView().setCellFactory(GoalNodeListCell::new);
......
......@@ -9,6 +9,8 @@ import de.uka.ilkd.key.settings.ProofIndependentSettings;
import javafx.beans.Observable;
import javafx.beans.property.SimpleObjectProperty;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.*;
import javafx.scene.paint.Color;
import org.fxmisc.richtext.CharacterHit;
import org.fxmisc.richtext.CodeArea;
......@@ -107,17 +109,21 @@ public class SequentView extends CodeArea {
clear();
insertText(0, backend.getString());
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 Node getNode() {
return node.get();
}
public SimpleObjectProperty<Node> nodeProperty() {
return node;
}
public void setNode(Node node) {
this.node.set(node);
}
public SimpleObjectProperty<Node> nodeProperty() {
return node;
}
}
......@@ -2,9 +2,11 @@ package edu.kit.formal.gui.model;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.proofscriptparser.ast.ASTNode;
import javafx.beans.property.SimpleListProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.collections.ObservableList;
import javafx.scene.paint.Color;
import java.util.List;
import java.util.Map;
import java.util.Set;
......@@ -17,9 +19,9 @@ public class InspectionModel {
private ASTNode node;
private List<GoalNode> currentGoals;
private SimpleListProperty<GoalNode> currentGoals;
private GoalNode selectedGoalNodeToShow;
private SimpleObjectProperty<GoalNode> selectedGoalNodeToShow;
private Map<GoalNode, Color> colorofEachGoalNodeinListView;
......@@ -33,14 +35,90 @@ public class InspectionModel {
private boolean isInterpreterTab;
public InspectionModel(ASTNode node) {
this.node = node;
public InspectionModel() {
}
/***************************************************************************************************************
* Getter and Setter
*
*/
***************************************************************************************************************/
public ASTNode getNode() {
return node;
}
public void setNode(ASTNode node) {
this.node = node;
}
public ObservableList<GoalNode> getCurrentGoals() {
return currentGoals.get();
}
public void setCurrentGoals(ObservableList<GoalNode> currentGoals) {
this.currentGoals.set(currentGoals);
}
public SimpleListProperty<GoalNode> currentGoalsProperty() {
return currentGoals;
}
public GoalNode getSelectedGoalNodeToShow() {
return selectedGoalNodeToShow.get();
}
public void setSelectedGoalNodeToShow(GoalNode selectedGoalNodeToShow) {
this.selectedGoalNodeToShow.set(selectedGoalNodeToShow);
}
public SimpleObjectProperty<GoalNode> selectedGoalNodeToShowProperty() {
return selectedGoalNodeToShow;
}
public Map<GoalNode, Color> getColorofEachGoalNodeinListView() {
return colorofEachGoalNodeinListView;
}
public void setColorofEachGoalNodeinListView(Map<GoalNode, Color> colorofEachGoalNodeinListView) {
this.colorofEachGoalNodeinListView = colorofEachGoalNodeinListView;
}
public boolean isShowJavaView() {
return showJavaView;
}
public void setShowJavaView(boolean showJavaView) {
this.showJavaView = showJavaView;
}
public String getJavaString() {
return javaString;
}
public void setJavaString(String javaString) {
this.javaString = javaString;
}
public Set<Integer> getHighlightedJavaLines() {
return highlightedJavaLines;
}
public void setHighlightedJavaLines(Set<Integer> highlightedJavaLines) {
this.highlightedJavaLines = highlightedJavaLines;
}
public boolean isClosable() {
return closable;
}
public void setClosable(boolean closable) {
this.closable = closable;
}
public boolean isInterpreterTab() {
return isInterpreterTab;
}
public void setInterpreterTab(boolean interpreterTab) {
isInterpreterTab = interpreterTab;
}
}
package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.api.ProjectedNode;
import de.uka.ilkd.key.api.ProofApi;
import de.uka.ilkd.key.api.ProofManagementApi;
import de.uka.ilkd.key.control.KeYEnvironment;
......@@ -22,7 +21,9 @@ import java.util.Collections;
import java.util.List;
/**
* Created by sarah on 5/29/17.
* Facade to KeY. Build part of the interpreter
* @author S. Grebing
* @author A. Weigl
*/
public class KeYProofFacade {
private SimpleObjectProperty<Proof> proof = new SimpleObjectProperty<>();
......@@ -31,6 +32,8 @@ public class KeYProofFacade {
private SimpleObjectProperty<Contract> contract = new SimpleObjectProperty<>();
private BooleanBinding readyToExecute = proof.isNotNull();
//Workaround until api is relaxed
private ProofManagementApi pma;
//region loading
public Task<Void> loadKeyFileTask(File keYFile) {
......@@ -61,9 +64,6 @@ public class KeYProofFacade {
};
}
//Workaround until api is relaxed
private ProofManagementApi pma;
public List<Contract> getContractsForJavaFile(File javaFile)
throws ProblemLoaderException {
pma = KeYApi.loadFromKeyFile(javaFile);
......@@ -111,38 +111,38 @@ public class KeYProofFacade {
return proof.get();
}
public SimpleObjectProperty<Proof> proofProperty() {
return proof;
}
public void setProof(Proof proof) {
this.proof.set(proof);
}
public KeYEnvironment getEnvironment() {
return environment.get();
public SimpleObjectProperty<Proof> proofProperty() {
return proof;
}
public SimpleObjectProperty<KeYEnvironment> environmentProperty() {
return environment;
public KeYEnvironment getEnvironment() {
return environment.get();
}
public void setEnvironment(KeYEnvironment environment) {
this.environment.set(environment);
}
public Contract getContract() {
return contract.get();
public SimpleObjectProperty<KeYEnvironment> environmentProperty() {
return environment;
}
public SimpleObjectProperty<Contract> contractProperty() {
return contract;
public Contract getContract() {
return contract.get();
}
public void setContract(Contract contract) {
this.contract.set(contract);
}
public SimpleObjectProperty<Contract> contractProperty() {
return contract;
}
public Boolean getReadyToExecute() {
return readyToExecute.getValue();
}
......
......@@ -180,6 +180,16 @@
}
}
.closed-sequent-view {
-fx-font-size: 14pt;
-fx-background-color: @red;
.sequent-highlight {
-rtfx-background-color: @base01;
-fx-fill: @base1
}
}
.section-pane {
.title {
-fx-font-weight: bold;
......
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