Commit 6621e07a authored by Lulu Luong's avatar Lulu Luong

added collapse in ScriptTreeContextMenu

parent 4fbb71f4
Pipeline #33610 passed with stages
in 2 minutes and 26 seconds
...@@ -165,7 +165,6 @@ public class DebuggerMain implements Initializable { ...@@ -165,7 +165,6 @@ public class DebuggerMain implements Initializable {
private ProofTree proofTree = new ProofTree(this); private ProofTree proofTree = new ProofTree(this);
private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree"); private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree");
//TODO: anpassen
private ScriptTreeGraph scriptTreeGraph = new ScriptTreeGraph(); private ScriptTreeGraph scriptTreeGraph = new ScriptTreeGraph();
private ScriptTreeView scriptTreeView = new ScriptTreeView(this); private ScriptTreeView scriptTreeView = new ScriptTreeView(this);
private DockNode scriptTreeDock = new DockNode(scriptTreeView,"Script Tree"); private DockNode scriptTreeDock = new DockNode(scriptTreeView,"Script Tree");
...@@ -299,8 +298,6 @@ public class DebuggerMain implements Initializable { ...@@ -299,8 +298,6 @@ public class DebuggerMain implements Initializable {
//marriage key proof facade to proof tree //marriage key proof facade to proof tree
//TODO: refresh script tree
getFacade().proofProperty().addListener( getFacade().proofProperty().addListener(
(prop, o, n) -> { (prop, o, n) -> {
if (n == null) { if (n == null) {
...@@ -401,6 +398,7 @@ public class DebuggerMain implements Initializable { ...@@ -401,6 +398,7 @@ public class DebuggerMain implements Initializable {
renewThreadStateTimer(); renewThreadStateTimer();
savePointController = new SavePointController(this); savePointController = new SavePointController(this);
} }
/** /**
...@@ -534,7 +532,7 @@ public class DebuggerMain implements Initializable { ...@@ -534,7 +532,7 @@ public class DebuggerMain implements Initializable {
public void executeScript() { public void executeScript() {
//execute script without stepwise //execute script without stepwise
scriptExecutionController.executeScript(false); scriptExecutionController.executeScript(false);
//executeScript(false);
} }
...@@ -617,6 +615,9 @@ public class DebuggerMain implements Initializable { ...@@ -617,6 +615,9 @@ public class DebuggerMain implements Initializable {
assert statePointer != null; assert statePointer != null;
State<KeyData> lastState = statePointer.getStateAfterStmt(); State<KeyData> lastState = statePointer.getStateAfterStmt();
getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState); getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState);
refreshScriptTreeView();
if (lastState.getGoals().isEmpty()) { if (lastState.getGoals().isEmpty()) {
statusBar.setNumberOfGoals(0); statusBar.setNumberOfGoals(0);
Utils.showClosedProofDialog("the script " + scriptController.getMainScript().getScriptName()); Utils.showClosedProofDialog("the script " + scriptController.getMainScript().getScriptName());
...@@ -742,6 +743,7 @@ public class DebuggerMain implements Initializable { ...@@ -742,6 +743,7 @@ public class DebuggerMain implements Initializable {
//execute stepwise from start //execute stepwise from start
scriptExecutionController.executeScript(true); scriptExecutionController.executeScript(true);
//executeScript(true); //executeScript(true);
} }
...@@ -751,6 +753,7 @@ public class DebuggerMain implements Initializable { ...@@ -751,6 +753,7 @@ public class DebuggerMain implements Initializable {
df.setErrorListener(this::onInterpreterError); df.setErrorListener(this::onInterpreterError);
if (addInitBreakpoint) { if (addInitBreakpoint) {
df.releaseUntil(new Blocker.CounterBlocker(1)); // just execute df.releaseUntil(new Blocker.CounterBlocker(1)); // just execute
} }
df.getBreakpoints().addAll(breakpoints); df.getBreakpoints().addAll(breakpoints);
df.getStatePointerListener().add(this::handleStatePointer); df.getStatePointerListener().add(this::handleStatePointer);
...@@ -1197,7 +1200,6 @@ public class DebuggerMain implements Initializable { ...@@ -1197,7 +1200,6 @@ public class DebuggerMain implements Initializable {
@FXML @FXML
public void selectSavepoint(ActionEvent actionEvent) { public void selectSavepoint(ActionEvent actionEvent) {
//TODO remove highlight of SPs
SavePoint selected = cboSavePoints.getValue(); SavePoint selected = cboSavePoints.getValue();
...@@ -1283,7 +1285,6 @@ public class DebuggerMain implements Initializable { ...@@ -1283,7 +1285,6 @@ public class DebuggerMain implements Initializable {
scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected); scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
} }
...@@ -1319,29 +1320,48 @@ public class DebuggerMain implements Initializable { ...@@ -1319,29 +1320,48 @@ public class DebuggerMain implements Initializable {
@FXML @FXML
public void showScriptTree(ActionEvent actionEvent) { public void showScriptTree(ActionEvent actionEvent) {
//TODO: anpassen if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof loaded is loaded yet. If proof loading was invoked, please wait. Loading may take a while.", ButtonType.OK);
alert.showAndWait();
return;
}
if (!scriptTreeDock.isDocked() && !scriptTreeDock.isFloating()) { if (!scriptTreeDock.isDocked() && !scriptTreeDock.isFloating()) {
scriptTreeDock.dock(dockStation, DockPos.LEFT); scriptTreeDock.dock(dockStation, DockPos.LEFT);
} }
// old version of scripttree refreshScriptTreeView();
ScriptTreeGraph stg = new ScriptTreeGraph();
PTreeNode startnode = (model.getDebuggerFramework() != null)?model.getDebuggerFramework().getPtreeManager().getStartNode():null;
if(startnode == null) return;
stg.createGraph(startnode, FACADE.getProof().root());
scriptTreeView.setModel(model);
scriptTreeView.setFACADE(FACADE);
scriptTreeView.setStg(stg); }
scriptTreeView.toView();
/*TreeItem<AbstractTreeNode> item = (stg.toView()); /**
* refreshes the view on the scripttree
*/
public void refreshScriptTreeView() {
scriptTreeGraph = new ScriptTreeGraph();
PTreeNode startnode = null;
try {
startnode = model.getDebuggerFramework().getPtreeManager().getStartNode();
} finally {
scriptTreeGraph.createGraph(startnode, FACADE.getProof().root());
scriptTreeView.setStg(scriptTreeGraph);
scriptTreeView.toView();
}
scriptTreeView.setTree(item);
*/
/*
if (model.getDebuggerFramework() != null) {
PTreeNode startnode = model.getDebuggerFramework().getPtreeManager().getStartNode();
if (startnode != null) {
scriptTreeGraph.createGraph(startnode, FACADE.getProof().root());
}
} else {
//No script executed yet
scriptTreeGraph = new ScriptTreeGraph();
}
scriptTreeView.setStg(scriptTreeGraph);
scriptTreeView.toView();
*/
} }
...@@ -1515,7 +1535,6 @@ public class DebuggerMain implements Initializable { ...@@ -1515,7 +1535,6 @@ public class DebuggerMain implements Initializable {
//traverseProofTreeAndAddSentinelsToLeaves(); //traverseProofTreeAndAddSentinelsToLeaves();
} }
ptree.expandRootToSentinels(); ptree.expandRootToSentinels();
DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " + DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " +
original.getStatement().accept(new ShortCommandPrinter()) original.getStatement().accept(new ShortCommandPrinter())
...@@ -1523,6 +1542,7 @@ public class DebuggerMain implements Initializable { ...@@ -1523,6 +1542,7 @@ public class DebuggerMain implements Initializable {
node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea())); node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea()));
node.requestFocus(); node.requestFocus();
} }
} }
......
...@@ -85,7 +85,6 @@ public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu { ...@@ -85,7 +85,6 @@ public class ProofTreeContextMenu extends javafx.scene.control.ContextMenu {
expandAllNodes.setOnAction((event) -> { expandAllNodes.setOnAction((event) -> {
proofTree.expandRootToLeaves(proofTree.getTreeProof().getRoot()); proofTree.expandRootToLeaves(proofTree.getTreeProof().getRoot());
}); });
//TODO SCRIPTTREE ACTION
getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal); getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal);
setAutoFix(true); setAutoFix(true);
setAutoHide(true); setAutoHide(true);
......
...@@ -15,24 +15,36 @@ public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu { ...@@ -15,24 +15,36 @@ public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu {
MenuItem copyBranchLabel = new MenuItem("Branch Label"); MenuItem copyBranchLabel = new MenuItem("Branch Label");
MenuItem copyProgramLines = new MenuItem("Program Lines"); MenuItem copyProgramLines = new MenuItem("Program Lines");
MenuItem createCases = new MenuItem("Created Case for Open Goals"); MenuItem createCases = new MenuItem("Created Case for Open Goals");
MenuItem refresh = new MenuItem("Refresh (TOFIX)"); MenuItem refresh = new MenuItem("Refresh");
MenuItem showSequent = new MenuItem("Show Sequent"); MenuItem showSequent = new MenuItem("Show Sequent");
MenuItem showGoal = new MenuItem("Show in Goal List"); MenuItem showGoal = new MenuItem("Show in Goal List");
MenuItem expandAllNodes = new MenuItem("Expand Tree"); MenuItem expandAllNodes = new MenuItem("Expand Tree");
MenuItem collapseAllNodes = new MenuItem("Collapse Tree");
MenuItem expandFromNode = new MenuItem("Expand Tree from here");
private ScriptTreeView scriptTreeView; private ScriptTreeView scriptTreeView;
public ScriptTreeContextMenu(ScriptTreeView scriptTreeView) { public ScriptTreeContextMenu(ScriptTreeView scriptTreeView) {
this.scriptTreeView = scriptTreeView; this.scriptTreeView = scriptTreeView;
refresh.setOnAction(event -> scriptTreeView.setTree(scriptTreeView.toView()));
refresh.setGraphic(new MaterialDesignIconView(MaterialDesignIcon.REFRESH));
expandAllNodes.setOnAction((event) -> { expandAllNodes.setOnAction((event) -> {
expandRootToLeaves(scriptTreeView.treeView.getRoot()); expandRootToLeaves(scriptTreeView.treeView.getRoot());
}); });
getItems().setAll(refresh, expandAllNodes); //, new SeparatorMenuItem(), createCases, showSequent, showGoal); collapseAllNodes.setOnAction((event -> {
collapseRootToLeaves(scriptTreeView.treeView.getRoot());
}));
/*
expandFromNode.setOnAction((event -> {
expandTreeFromNode(event.getSource()
}));
*/
getItems().setAll(expandAllNodes, collapseAllNodes); //, new SeparatorMenuItem(), createCases, showSequent, showGoal);
setAutoFix(true); setAutoFix(true);
setAutoHide(true); setAutoHide(true);
/* /*
...@@ -102,4 +114,15 @@ public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu { ...@@ -102,4 +114,15 @@ public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu {
} }
} }
} }
static void collapseRootToLeaves(TreeItem candidate) {
if (candidate != null) {
if (!candidate.isLeaf()) {
candidate.setExpanded(false);
ObservableList<TreeItem> children = candidate.getChildren();
children.forEach(treeItem -> expandRootToLeaves(treeItem));
}
}
}
} }
...@@ -20,14 +20,17 @@ import javafx.scene.control.TreeView; ...@@ -20,14 +20,17 @@ import javafx.scene.control.TreeView;
import javafx.scene.control.cell.TextFieldTreeCell; import javafx.scene.control.cell.TextFieldTreeCell;
import javafx.util.StringConverter; import javafx.util.StringConverter;
import lombok.Getter; import lombok.Getter;
import lombok.Setter;
import javax.annotation.Nullable;
import java.util.*; import java.util.*;
public class ScriptTreeGraph { public class ScriptTreeGraph {
@Getter @Getter
private ScriptTreeNode rootNode; @Setter
private AbstractTreeNode rootNode;
@Getter @Getter
private Map<Node, AbstractTreeNode> mapping; private Map<Node, AbstractTreeNode> mapping;
...@@ -56,24 +59,28 @@ public class ScriptTreeGraph { ...@@ -56,24 +59,28 @@ public class ScriptTreeGraph {
public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) { public void createGraph(PTreeNode<KeyData> rootPTreeNode, Node root) {
this.currentNode = rootPTreeNode; AbstractTreeNode rootNode;
if(currentNode == null) return; if (rootPTreeNode != null) {
ScriptTreeNode rootNode = new ScriptTreeNode(root, rootPTreeNode, rootPTreeNode.getStatement().getStartPosition().getLineNumber()); this.currentNode = rootPTreeNode;
mapping = new HashMap<>(); if (currentNode == null) return;
foreachNodes = new HashMap<>(); rootNode = new ScriptTreeNode(root, rootPTreeNode, rootPTreeNode.getStatement().getStartPosition().getLineNumber());
repeatNodes = new HashMap<>(); mapping = new HashMap<>();
placeholderNodes = new ArrayList<>(); foreachNodes = new HashMap<>();
front = new ArrayList<>(); repeatNodes = new HashMap<>();
sortedList = new ArrayList<>(); placeholderNodes = new ArrayList<>();
State<KeyData> stateAfterStmt = rootPTreeNode.getStateAfterStmt(); front = new ArrayList<>();
if (stateAfterStmt != null) { sortedList = new ArrayList<>();
for (GoalNode<KeyData> g : stateAfterStmt.getGoals()) { State<KeyData> stateAfterStmt = rootPTreeNode.getStateAfterStmt();
putIntoMapping(g.getData().getNode(), null); if (stateAfterStmt != null) {
putIntoFront(g.getData().getNode()); for (GoalNode<KeyData> g : stateAfterStmt.getGoals()) {
putIntoMapping(g.getData().getNode(), null);
putIntoFront(g.getData().getNode());
}
} }
} else { } else {
rootNode = new DummyGoalNode(root, root.isClosed());
} }
this.rootNode = rootNode; this.rootNode = rootNode;
computeList(); computeList();
compute(); compute();
...@@ -167,6 +174,9 @@ public class ScriptTreeGraph { ...@@ -167,6 +174,9 @@ public class ScriptTreeGraph {
* Fills mapping/Creates model for graph * Fills mapping/Creates model for graph
*/ */
public void compute () { public void compute () {
if (sortedList == null) {
return;
}
Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0); Iterator<PTreeNode<KeyData>> iter = sortedList.listIterator(0);
ScriptVisitor visitor = new ScriptVisitor(); ScriptVisitor visitor = new ScriptVisitor();
...@@ -619,6 +629,9 @@ public class ScriptTreeGraph { ...@@ -619,6 +629,9 @@ public class ScriptTreeGraph {
} }
private void addGoals() { private void addGoals() {
if (front == null) {
return;
}
front.forEach(k -> { front.forEach(k -> {
replacePlaceholder(k, new DummyGoalNode(k, k.isClosed())); replacePlaceholder(k, new DummyGoalNode(k, k.isClosed()));
......
...@@ -22,10 +22,19 @@ import javafx.util.StringConverter; ...@@ -22,10 +22,19 @@ import javafx.util.StringConverter;
import lombok.Setter; import lombok.Setter;
import java.awt.*; import java.awt.*;
import java.util.ArrayList;
import java.util.HashMap; import java.util.HashMap;
import java.util.List; import java.util.List;
import java.util.Map; import java.util.Map;
/**
* Displays a Treeview of the ScriptTree, which represents state of proof using only
* statements in the script
* Branching Labels
* DummyGoalNodes
*
* @author luong
*/
public class ScriptTreeView extends BorderPane { public class ScriptTreeView extends BorderPane {
@Setter @Setter
...@@ -33,19 +42,9 @@ public class ScriptTreeView extends BorderPane { ...@@ -33,19 +42,9 @@ public class ScriptTreeView extends BorderPane {
private ContextMenu contextMenu; private ContextMenu contextMenu;
private ScriptTreeNode rootNode; private AbstractTreeNode rootNode;
private Map<Node, AbstractTreeNode> mapping; private Map<Node, AbstractTreeNode> mapping;
@Setter
private DebuggerMainModel model;
@Setter
private KeYProofFacade FACADE;
/**
* Contains color of nodes
*/
private MapProperty<Node, String> colorOfNodes = new SimpleMapProperty<Node, String>(FXCollections.observableHashMap());
@FXML @FXML
TreeView<AbstractTreeNode> treeView; TreeView<AbstractTreeNode> treeView;
...@@ -62,6 +61,7 @@ public class ScriptTreeView extends BorderPane { ...@@ -62,6 +61,7 @@ public class ScriptTreeView extends BorderPane {
public void setTree(TreeItem<AbstractTreeNode> tree) { public void setTree(TreeItem<AbstractTreeNode> tree) {
treeView.setRoot(tree); treeView.setRoot(tree);
treeView.refresh();
} }
private TreeCell<AbstractTreeNode> cellFactory(TreeView<AbstractTreeNode> nodeTreeView) { private TreeCell<AbstractTreeNode> cellFactory(TreeView<AbstractTreeNode> nodeTreeView) {
...@@ -82,70 +82,58 @@ public class ScriptTreeView extends BorderPane { ...@@ -82,70 +82,58 @@ public class ScriptTreeView extends BorderPane {
tftc.setConverter(stringConverter); tftc.setConverter(stringConverter);
tftc.itemProperty().addListener((p, o, n) -> { tftc.itemProperty().addListener((p, o, n) -> {
if (n != null) if (n != null) {
repaint(tftc); repaint(tftc);
} else {
tftc.setStyle("");
}
}); });
//colorOfNodes.addListener((InvalidationListener) o -> repaint(tftc));
return tftc; return tftc;
} }
/** /**
* returns treeItem that represents current Script tree * Build ScriptTreeView with ScriptTreeGraph and displays it in the view
* @return
*/ */
public TreeItem<AbstractTreeNode> toView() { public void toView() {
TreeItem<AbstractTreeNode> treeItem;
PTreeNode startnode;
try {
startnode = (model.getDebuggerFramework() != null) ?
model.getDebuggerFramework().getPtreeManager().getStartNode() :
null;
} catch (NullPointerException e) {
treeItem = new TreeItem<>(new AbstractTreeNode(null));
DummyGoalNode dummy = new DummyGoalNode(null, false);
treeItem.getChildren().add(new TreeItem<>(dummy));
this.setTree(treeItem); TreeItem<AbstractTreeNode> treeItem = new TreeItem<>(new AbstractTreeNode(null));
return treeItem; rootNode = stg.getRootNode();
}
//No script executed
if (startnode == null) {
System.out.println("Entered maybe redundaant toview(inside) method"); //TODO
treeItem = new TreeItem<>(new AbstractTreeNode(null));
DummyGoalNode dummy = new DummyGoalNode(null, false);
treeItem.getChildren().add(new TreeItem<>(dummy));
if (rootNode instanceof DummyGoalNode) {
treeItem.getChildren().add(new TreeItem<>(rootNode));
this.setTree(treeItem); this.setTree(treeItem);
return treeItem; return;
} }
stg.createGraph(startnode, FACADE.getProof().root());
rootNode = stg.getRootNode();
mapping = stg.getMapping(); mapping = stg.getMapping();
treeItem = new TreeItem<>(new AbstractTreeNode(null));
List<AbstractTreeNode> children = mapping.get(rootNode.getNode()).getChildren(); List<AbstractTreeNode> children = mapping.get(rootNode.getNode()).getChildren();
if (children == null) return treeItem; if (children == null) {
this.setTree(treeItem);
return;
}
treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode()))); treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode())));
while (children.size() == 1) { while (children.size() == 1) {
treeItem.getChildren().add(new TreeItem<>(children.get(0))); treeItem.getChildren().add(new TreeItem<>(children.get(0)));
children = children.get(0).getChildren(); children = children.get(0).getChildren();
if(children == null) return treeItem; if (children == null) {
this.setTree(treeItem);
return;
}
} }
if (children.size() != 0) { if (children.size() != 0) {
children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k))); List<TreeItem> subTreeItems = new ArrayList<>();
children.forEach(k -> subTreeItems.add(rekursiveToView(k)));
for (TreeItem item : subTreeItems) {
treeItem.getChildren().add(item);
}
} }
this.setTree(treeItem); this.setTree(treeItem);
return treeItem;
} }
private TreeItem<AbstractTreeNode> rekursiveToView(AbstractTreeNode current) { private TreeItem<AbstractTreeNode> rekursiveToView(AbstractTreeNode current) {
...@@ -192,12 +180,12 @@ public class ScriptTreeView extends BorderPane { ...@@ -192,12 +180,12 @@ public class ScriptTreeView extends BorderPane {
} else { } else {
tftc.styleProperty().setValue("-fx-background-color: indianred"); tftc.styleProperty().setValue("-fx-background-color: indianred");
//styleProperty().bind(tftc.styleProperty()); //styleProperty().bind(tftc.styleProperty());
// tftc.setStyle("-fx-background-color: indianred"); // tftc.setStyle("-fx-background-color: indianred");
//colorOfNodes.putIfAbsent(n, "indianred"); //colorOfNodes.putIfAbsent(n, "indianred");
} }
} }
} }
} }
public ContextMenu getContextMenu() { public ContextMenu getContextMenu() {
......
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