Commit 179c80b3 authored by Sarah Grebing's avatar Sarah Grebing

First part of splitting mainwindowcontroller inspection model is missing atm

parent a2e1278a
...@@ -6,10 +6,12 @@ import edu.kit.formal.gui.model.InspectionModel; ...@@ -6,10 +6,12 @@ import edu.kit.formal.gui.model.InspectionModel;
import edu.kit.formal.gui.model.RootModel; import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.data.GoalNode; import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import javafx.beans.Observable;
import javafx.fxml.FXML; import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader; import javafx.fxml.FXMLLoader;
import javafx.fxml.Initializable; import javafx.fxml.Initializable;
import javafx.scene.Node; import javafx.scene.Node;
import javafx.scene.control.ListCell;
import javafx.scene.control.ListView; import javafx.scene.control.ListView;
import javafx.scene.control.Tab; import javafx.scene.control.Tab;
import javafx.scene.input.MouseEvent; import javafx.scene.input.MouseEvent;
...@@ -24,13 +26,13 @@ import java.util.ResourceBundle; ...@@ -24,13 +26,13 @@ import java.util.ResourceBundle;
*/ */
public class InspectionViewTab extends Tab implements Initializable { public class InspectionViewTab extends Tab implements Initializable {
public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
@FXML @FXML
private SequentView sequentView; private SequentView sequentView;
@FXML @FXML
private JavaArea javaSourceCode; private JavaArea javaSourceCode;
@FXML @FXML
private ListView goalView; private ListView goalView;
private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
public InspectionViewTab() { public InspectionViewTab() {
super(); super();
...@@ -43,7 +45,7 @@ public class InspectionViewTab extends Tab implements Initializable { ...@@ -43,7 +45,7 @@ public class InspectionViewTab extends Tab implements Initializable {
e.printStackTrace(); e.printStackTrace();
} }
goalView.setVisible(true);
} }
public SequentView getSequentView() { public SequentView getSequentView() {
...@@ -98,5 +100,33 @@ public class InspectionViewTab extends Tab implements Initializable { ...@@ -98,5 +100,33 @@ public class InspectionViewTab extends Tab implements Initializable {
getGoalView().getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> { getGoalView().getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> {
getSequentView().setNode(newValue.getData().getNode()); getSequentView().setNode(newValue.getData().getNode());
}); });
getGoalView().setCellFactory(GoalNodeListCell::new);
}
/**
* Cells for GoalView
*/
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);
}
}
} }
package edu.kit.formal.gui.controls; package edu.kit.formal.gui.controls;
import edu.kit.formal.gui.model.RootModel; import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import javafx.beans.Observable;
import javafx.fxml.FXML; import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader; import javafx.fxml.FXMLLoader;
import javafx.scene.control.ListCell;
import javafx.scene.control.ListView;
import javafx.scene.control.TabPane; import javafx.scene.control.TabPane;
import java.io.IOException; import java.io.IOException;
...@@ -17,7 +12,14 @@ import java.io.IOException; ...@@ -17,7 +12,14 @@ import java.io.IOException;
*/ */
public class InspectionViewTabPane extends TabPane { public class InspectionViewTabPane extends TabPane {
/**
* active tab in which the interpreter resp. Debugger state is shown.
* This tab can be changed and later on in this tab it should be possible to select proof commands
* All other tabs are only post morten tabs which cannot be shown
*/
private InspectionViewTab activeInterpreterTab; private InspectionViewTab activeInterpreterTab;
@FXML @FXML
private InspectionViewTab inspectionViewTab; private InspectionViewTab inspectionViewTab;
...@@ -32,17 +34,9 @@ public class InspectionViewTabPane extends TabPane { ...@@ -32,17 +34,9 @@ public class InspectionViewTabPane extends TabPane {
e.printStackTrace(); e.printStackTrace();
} }
// this.setActiveInterpreterTab(inspectionViewTab);
// getActiveInspectionViewTab().getGoalView().setCellFactory(GoalNodeListCell::new);
} }
public InspectionViewTab getInspectionViewTab() {
return inspectionViewTab;
}
public void setActiveInterpreterTab(InspectionViewTab activeInterpreterTab) { public void setActiveInterpreterTab(InspectionViewTab activeInterpreterTab) {
this.activeInterpreterTab = activeInterpreterTab; this.activeInterpreterTab = activeInterpreterTab;
...@@ -55,27 +49,22 @@ public class InspectionViewTabPane extends TabPane { ...@@ -55,27 +49,22 @@ public class InspectionViewTabPane extends TabPane {
public void createNewInspectionViewTab(RootModel model, boolean activeTab) { public void createNewInspectionViewTab(RootModel model, boolean activeTab) {
InspectionViewTab tab = new InspectionViewTab(); InspectionViewTab tab = new InspectionViewTab();
if (activeTab) { if (activeTab) {
System.out.println(this.getActiveInspectionViewTab() == null);
this.setActiveInterpreterTab(tab);
tab.setText("Active Tab");
tab.setClosable(false);
this.setActiveInterpreterTab(tab); this.setActiveInterpreterTab(tab);
} }
tab.getGoalView().setCellFactory(GoalNodeListCell::new);
model.chosenContractProperty().addListener(o -> { model.chosenContractProperty().addListener(o -> {
tab.refresh(model); tab.refresh(model);
}); });
bindGoalNodesWithCurrentTab(model); bindGoalNodesWithCurrentTab(model);
tab.getGoalView().setCellFactory(GoalNodeListCell::new);
tab.setText("New Tab");
if (activeTab) {
this.setActiveInterpreterTab(tab);
}
this.getTabs().add(tab);
this.getTabs().add(tab);
// inspectionViewTabPane.getInspectionViewTab().getGoalView().setCellFactory(GoalNodeListCell::new);
}
public void refresh(RootModel model) {
getActiveInspectionViewTab().refresh(model);
} }
public void bindGoalNodesWithCurrentTab(RootModel model) { public void bindGoalNodesWithCurrentTab(RootModel model) {
...@@ -90,30 +79,6 @@ public class InspectionViewTabPane extends TabPane { ...@@ -90,30 +79,6 @@ public class InspectionViewTabPane extends TabPane {
} }
/**
* Cells for GoalView
*/
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);
}
}
} }
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