Commit 24e7bad0 authored by Lulu Luong's avatar Lulu Luong

updated ScriptTreeContextMenu

parent 6621e07a
Pipeline #33747 passed with stages
in 2 minutes and 28 seconds
...@@ -1337,32 +1337,15 @@ public class DebuggerMain implements Initializable { ...@@ -1337,32 +1337,15 @@ public class DebuggerMain implements Initializable {
/** /**
* refreshes the view on the scripttree * refreshes the view on the scripttree
*/ */
public void refreshScriptTreeView() { private void refreshScriptTreeView() {
scriptTreeGraph = new ScriptTreeGraph(); scriptTreeGraph = new ScriptTreeGraph();
PTreeNode startnode = null; PTreeNode startnode = null;
try { if (model.getDebuggerFramework() != null && model.getDebuggerFramework().getPtreeManager() != null) {
startnode = model.getDebuggerFramework().getPtreeManager().getStartNode(); startnode = model.getDebuggerFramework().getPtreeManager().getStartNode();
} finally {
scriptTreeGraph.createGraph(startnode, FACADE.getProof().root());
scriptTreeView.setStg(scriptTreeGraph);
scriptTreeView.toView();
}
/*
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();
} }
scriptTreeGraph.createGraph(startnode, FACADE.getProof().root());
scriptTreeView.setStg(scriptTreeGraph); scriptTreeView.setStg(scriptTreeGraph);
scriptTreeView.toView(); scriptTreeView.toView();
*/
} }
@FXML @FXML
......
...@@ -3,26 +3,29 @@ package edu.kit.iti.formal.psdbg.gui.controls; ...@@ -3,26 +3,29 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.LabelFactory; import edu.kit.iti.formal.psdbg.LabelFactory;
import edu.kit.iti.formal.psdbg.gui.controller.Events; import edu.kit.iti.formal.psdbg.gui.controller.Events;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
import javafx.collections.ObservableList; import javafx.collections.ObservableList;
import javafx.scene.control.Menu; import javafx.scene.control.Menu;
import javafx.scene.control.MenuItem; import javafx.scene.control.MenuItem;
import javafx.scene.control.SeparatorMenuItem; import javafx.scene.control.SeparatorMenuItem;
import javafx.scene.control.TreeItem; import javafx.scene.control.TreeItem;
import lombok.Setter;
import java.util.function.Consumer;
public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu { 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");
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 from here");
MenuItem collapseAllNodes = new MenuItem("Collapse Tree"); MenuItem collapseAllNodes = new MenuItem("Collapse Tree from here");
MenuItem expandFromNode = new MenuItem("Expand Tree from here");
private ScriptTreeView scriptTreeView; private ScriptTreeView scriptTreeView;
...@@ -31,98 +34,51 @@ public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu { ...@@ -31,98 +34,51 @@ public class ScriptTreeContextMenu extends javafx.scene.control.ContextMenu {
this.scriptTreeView = scriptTreeView; this.scriptTreeView = scriptTreeView;
expandAllNodes.setOnAction((event) -> { expandAllNodes.setOnAction((event) -> {
expandRootToLeaves(scriptTreeView.treeView.getRoot()); scriptTreeView.consumeNode(n ->
}); expandNodeToLeaves(n), "");
collapseAllNodes.setOnAction((event -> {
collapseRootToLeaves(scriptTreeView.treeView.getRoot());
}));
/*
expandFromNode.setOnAction((event -> {
expandTreeFromNode(event.getSource()
}));
*/
getItems().setAll(expandAllNodes, collapseAllNodes); //, new SeparatorMenuItem(), createCases, showSequent, showGoal);
setAutoFix(true);
setAutoHide(true);
/*
copyBranchLabel.setOnAction(evt -> proofTree.consumeNode(n -> Utils.intoClipboard(
LabelFactory.getBranchingLabel(n)), "Copied!"));
copyProgramLines.setOnAction(evt -> {
proofTree.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getProgramLines(n));
}, "Copied!");
}); });
MenuItem copySequent = new MenuItem("Sequent"); collapseAllNodes.setOnAction((event) -> {
copySequent.setOnAction(evt -> { scriptTreeView.consumeNode(n ->
proofTree.consumeNode(n -> { collapseNodeToLeaves(n), "");
assert proofTree.getServices() != null : "set KeY services!";
String s = LogicPrinter.quickPrintSequent(n.sequent(), proofTree.getServices());
Utils.intoClipboard(s);
}, "Copied!");
}); });
MenuItem copyRulesLabel = new MenuItem("Rule labels"); showSequent.setOnAction((event -> {
copyRulesLabel.setOnAction(evt -> { scriptTreeView.consumeNode(n ->
proofTree.consumeNode(n -> { Events.fire(new Events.ShowSequent(((AbstractTreeNode) n.getValue()).getNode())), "");
Utils.intoClipboard( }));
LabelFactory.getRuleLabel(n));
}, "Copied!");
});
MenuItem copyProgramStatements = new MenuItem("Statements");
copyProgramStatements.setOnAction(event -> {
proofTree.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getProgramStatmentLabel(n));
}, "Copied!");
});
Menu copy = new Menu("Copy", new MaterialDesignIconView(MaterialDesignIcon.CONTENT_COPY),
copyBranchLabel, copyProgramLines,
copyProgramStatements, copyRulesLabel,
copySequent);
createCases.setOnAction(this::onCreateCases);
showSequent.setOnAction((evt) ->
proofTree.consumeNode(n -> Events.fire(new Events.ShowSequent(n)), ""));
showGoal.setOnAction((evt) -> proofTree.consumeNode(n -> Events.fire(new Events.SelectNodeInGoalList(n)), "Found!"));
copyBranchLabel.setOnAction(evt -> scriptTreeView.consumeNode(n -> {
Utils.intoClipboard(
LabelFactory.getBranchingLabel(((AbstractTreeNode) n.getValue()).getNode()));
}, "Copied!"));
//TODO SCRIPTTREE ACTION getItems().setAll(expandAllNodes, collapseAllNodes, new SeparatorMenuItem(), showSequent, createCases); //, new SeparatorMenuItem(), createCases, showSequent, showGoal);
getItems().setAll(refresh, expandAllNodes, new SeparatorMenuItem(), copy, createCases, showSequent, showGoal);
setAutoFix(true); setAutoFix(true);
setAutoHide(true); setAutoHide(true);
*/
} }
static void expandRootToLeaves(TreeItem candidate) {
static void expandNodeToLeaves(TreeItem candidate) {
if (candidate != null) { if (candidate != null) {
if (!candidate.isLeaf()) { if (!candidate.isLeaf()) {
candidate.setExpanded(true); candidate.setExpanded(true);
ObservableList<TreeItem> children = candidate.getChildren(); ObservableList<TreeItem> children = candidate.getChildren();
children.forEach(treeItem -> expandRootToLeaves(treeItem)); children.forEach(treeItem -> expandNodeToLeaves(treeItem));
} }
} }
} }
static void collapseRootToLeaves(TreeItem candidate) { static void collapseNodeToLeaves(TreeItem candidate) {
if (candidate != null) { if (candidate != null) {
if (!candidate.isLeaf()) { if (!candidate.isLeaf()) {
candidate.setExpanded(false); candidate.setExpanded(false);
ObservableList<TreeItem> children = candidate.getChildren(); ObservableList<TreeItem> children = candidate.getChildren();
children.forEach(treeItem -> expandRootToLeaves(treeItem)); children.forEach(treeItem -> expandNodeToLeaves(treeItem));
} }
} }
} }
} }
...@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.gui.controls; ...@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import com.sun.javafx.css.Style; import com.sun.javafx.css.Style;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain; import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
import edu.kit.iti.formal.psdbg.gui.controller.Events;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*; import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.*;
import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel; import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
...@@ -26,6 +27,7 @@ import java.util.ArrayList; ...@@ -26,6 +27,7 @@ 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;
import java.util.function.Consumer;
/** /**
* Displays a Treeview of the ScriptTree, which represents state of proof using only * Displays a Treeview of the ScriptTree, which represents state of proof using only
...@@ -40,7 +42,7 @@ public class ScriptTreeView extends BorderPane { ...@@ -40,7 +42,7 @@ public class ScriptTreeView extends BorderPane {
@Setter @Setter
private ScriptTreeGraph stg; private ScriptTreeGraph stg;
private ContextMenu contextMenu; private ScriptTreeContextMenu contextMenu;
private AbstractTreeNode rootNode; private AbstractTreeNode rootNode;
private Map<Node, AbstractTreeNode> mapping; private Map<Node, AbstractTreeNode> mapping;
...@@ -194,4 +196,13 @@ public class ScriptTreeView extends BorderPane { ...@@ -194,4 +196,13 @@ public class ScriptTreeView extends BorderPane {
} }
return contextMenu; return contextMenu;
} }
public void consumeNode(Consumer<TreeItem> consumer, String success) {
TreeItem<AbstractTreeNode> item = treeView.getSelectionModel().getSelectedItem();
if (item != null) {
consumer.accept(item);
} else {
Events.fire(new Events.PublishMessage("Current item does not have a node.", 2));
}
}
} }
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