Commit 68480d15 authored by Alexander Weigl's avatar Alexander Weigl

not going well

parent 1e66aa27
Pipeline #39595 failed with stages
in 32 seconds
......@@ -52,7 +52,7 @@ public abstract class Example {
String content = IOUtils.toString(helpText, Charset.defaultCharset());
debuggerMain.openNewHelpDock(getName() + " Example", content);
}
debuggerMain.getWelcomePaneDock().close();
//TODO debuggerMain.getWelcomePaneDock().close();
} catch (IOException e) {
e.printStackTrace();
}
......
......@@ -2,31 +2,30 @@ package edu.kit.iti.formal.psdbg.examples;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import org.apache.commons.io.IOUtils;
import java.beans.PropertyChangeEvent;
import java.beans.PropertyChangeListener;
import java.io.*;
import java.net.URL;
import java.nio.charset.Charset;
/**
* Under construction!!!!!!
*
* @author Alexander Weigl
*/
public class JavaExample extends Example {
protected URL javaFile;
protected URL settingsFile;
//public void setProjectFile(URL projectFile){this.projectFile = projectFile;}
private URL projectFile;
public void setJavaFile(URL javaFile) {
this.javaFile = javaFile;
}
//public void setProjectFile(URL projectFile){this.projectFile = projectFile;}
protected URL javaFile;
protected URL settingsFile;
public void setSettingsFile(URL settingsFile) {
this.settingsFile = settingsFile;
......@@ -41,7 +40,7 @@ public class JavaExample extends Example {
File script = newTempFile(scriptFile, getName() + ".kps");
debuggerMain.openScript(script);
debuggerMain.getWelcomePaneDock().close();
//TODO debuggerMain.getWelcomePaneDock().close();
//File key = newTempFile(keyFile, "project.key");
File java = newTempFile(javaFile, getName() + ".java");
//System.out.println(java.getAbsolutePath());
......@@ -50,7 +49,7 @@ public class JavaExample extends Example {
if (settingsFile != null) {
File settings = newTempFile(settingsFile, getName() + ".props");
ProofListener pl = new ProofListener(debuggerMain, settings);
debuggerMain.getFacade().proofProperty().addListener(pl);
//TODO debuggerMain.getFacade().proofProperty().addListener(pl);
}
debuggerMain.showActiveInspector(null);
if (helpText != null) {
......@@ -62,7 +61,7 @@ public class JavaExample extends Example {
}
}
public class ProofListener implements ChangeListener<Proof> {
public class ProofListener implements PropertyChangeListener {
File settingsFile;
DebuggerMain debuggerMain;
......@@ -73,7 +72,8 @@ public class JavaExample extends Example {
}
@Override
public void changed(ObservableValue<? extends Proof> observable, Proof oldValue, Proof newValue) {
public void propertyChange(PropertyChangeEvent evt) {
Proof newValue = (Proof) evt.getNewValue();
if (newValue != null) {
try {
BufferedReader reader = new BufferedReader(new FileReader(settingsFile));
......@@ -81,9 +81,7 @@ public class JavaExample extends Example {
} catch (FileNotFoundException e) {
e.printStackTrace();
}
debuggerMain.getFacade().proofProperty().removeListener(this);
//TODO debuggerMain.getFacade().proofProperty().removeListener(this);
}
}
}
......
......@@ -63,9 +63,8 @@ import java.util.stream.Collectors;
* @author Alexander Weigl
*/
public class DebuggerMain extends JFrame {
public static final KeYProofFacade FACADE = new KeYProofFacade();
protected static final Logger LOGGER = LogManager.getLogger(DebuggerMain.class);
private static final KeYProofFacade FACADE = new KeYProofFacade();
private static final Logger LOGGER = LogManager.getLogger(DebuggerMain.class);
public final ContractLoaderService contractLoaderService = new ContractLoaderService();
......@@ -73,39 +72,54 @@ public class DebuggerMain extends JFrame {
@Getter
private final DebuggerMainModel model = new DebuggerMainModel();
/*TODO LATER:
private final GraphView graphView = new GraphView();
private final Graph.PTreeGraph graph = graphView.getGraph();
private final Dockable graphViewNode = new DockNode(graphView, "Debug graph");
*/
private JMenuItem menuExecuteFromSavepoint;
private JMenuItem menuRestartFromSavepoint;
private JButton buttonStartInterpreter;
//TODO private ScriptController scriptController;
private JComboBox<SavePoint> cboSavePoints;
private JButton btnSavePointRollback;
@Getter
private Action actStepOut = new DummyAction("Step Out"),
actShowProofTree = new DummyAction("Show Proof Tree"),
actShowCommandHelp = new DummyAction("Show command help"),
actShowWelcomeDock = new DummyAction("Show Welcome Dock"),
actShowActiveInspector = new DummyAction("AI"),
actShowCodeDock = new DummyAction("Show code dock"),
actStopDebugMode = new DummyAction("Stop debug mode"),
actExecuteStepwise = new DummyAction("execute stepwise"),
actStepInto = new DummyAction("Step into"),
actStepOver = new DummyAction(""),
actStepOverReverse = new DummyAction(""),
actStepIntoReverse = new DummyAction(""),
actNewScript = new DummyAction(""),
actExecuteScript = new DummyAction(""),
actOpenScript = new DummyAction(""),
actSaveProof = new DummyAction(""),
actClose = new DummyAction(""),
actLoadKeYFile = new DummyAction(""),
actLoadJavaFile = new DummyAction(""),
actSaveScript = new DummyAction(""),
actSaveAsScript = new DummyAction(""),
actOpenInKey = new DummyAction(""),
actReformat = new DummyAction(""),
actDebugPrintDot = new DummyAction(""),
actExecuteFromSavepoint = new DummyAction(""),
actRestartFromSavepoint = new DummyAction(""),
actSavePointRollback = new DummyAction(""),
actStartInterpreter = new DummyAction("");
//TODO private ScriptController scriptController;
private JComboBox<SavePoint> cboSavePoints = new JComboBox<>();
//TODO private InspectionViewsController inspectionViewsController;
private SavePointController savePointController;
private InterpreterBuilder interpreterBuilder;
//private DebuggerStatusBar statusBar;
private JPanel statusBar;
private JToggleButton togBtnCommandHelp;
private JToggleButton togBtnProofTree;
private JToggleButton togBtnActiveInspector;
private JToggleButton togBtnWelcome;
private JToggleButton togBtnCodeDock;
private JCheckBoxMenuItem miCommandHelp;
private JCheckBoxMenuItem miCodeDock;
private JCheckBoxMenuItem miWelcomeDock;
private JCheckBoxMenuItem miActiveInspector;
private JCheckBoxMenuItem miProofTree;
private JToggleButton btnInteractiveMode;
private JButton interactive_undo;
private ToggleViewAction actToggleCommandHelp, actToggleProofTree, actToggleActiveInspector,
actToggleWelcome, actToggleCode;
private Action actInteractiveMode = new DummyAction("Interactive Mode");
private Action actInteractiveUndo = new DummyAction("Interactive Undo");
private JTextArea javaArea = new JTextArea();
//private JavaArea javaArea = new JavaArea();
private Dockable javaAreaDock;
......@@ -125,6 +139,11 @@ public class DebuggerMain extends JFrame {
private Timer interpreterThreadTimer;
private CControl dockControl;
private CContentArea dockContent;
private Action actShowAbout;
public DebuggerMain() {
setupUI();
}
public static DefaultSingleCDockable create(JPanel content, String title) {
return new DefaultSingleCDockable(title, content);
......@@ -218,10 +237,12 @@ public class DebuggerMain extends JFrame {
}
private void setupUI() {
setupMenu();
setupToolbar();
setupDocking();
//TODO scriptController = new ScriptController(dockControl);
//TODO interactiveModeController = new InteractiveModeController(scriptController);
btnInteractiveMode.setSelected(false);
//TODO btnInteractiveMode.setSelected(false);
//TODO inspectionViewsController = new InspectionViewsController(dockControl);
//TODO activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock();
//register the welcome dock in the center
......@@ -305,6 +326,65 @@ public class DebuggerMain extends JFrame {
Events.register(this);
}
private void setupMenu() {
JMenuBar menubar = new JMenuBar();
JMenu fileMenu = new JMenu("File");
fileMenu.add(actNewScript);
fileMenu.add(actOpenScript);
fileMenu.add(actLoadKeYFile);
fileMenu.add(actLoadJavaFile);
fileMenu.add(actSaveScript);
fileMenu.add(actSaveAsScript);
fileMenu.add(actSaveProof);
fileMenu.add(actClose);
var fileEdit = new JMenu("Edit");
fileEdit.add(actOpenInKey);
fileEdit.add(actReformat);
fileEdit.add(actDebugPrintDot);
var runMenu = new JMenu("Debug");
runMenu.add(actExecuteScript);
runMenu.add(actExecuteFromSavepoint);
runMenu.add(actRestartFromSavepoint);
runMenu.add(actExecuteStepwise);
runMenu.add(actStepInto);
runMenu.add(actStepOver);
runMenu.add(actStepOverReverse);
runMenu.add(actStepIntoReverse);
runMenu.add(actStepOut);
runMenu.add(actStopDebugMode);
JMenu viewMenu = new JMenu("View");
viewMenu.add(actShowCodeDock);
viewMenu.add(actShowWelcomeDock);
viewMenu.add(actShowActiveInspector);
viewMenu.add(actShowProofTree);
viewMenu.add(actShowCommandHelp);
JMenu examplesMenu = new JMenu();
JMenu helpMenu = new JMenu("Help");
helpMenu.add(actShowAbout);
menubar.add(fileMenu);
menubar.add(fileEdit);
menubar.add(runMenu);
menubar.add(examplesMenu);
menubar.add(viewMenu);
setJMenuBar(menubar);
}
private void setupToolbar() {
JToolBar toolBar = new JToolBar();
toolBar.add(actStartInterpreter);
toolBar.add(actExecuteStepwise);
toolBar.addSeparator();
toolBar.add(cboSavePoints);
toolBar.add(actExecuteFromSavepoint);
toolBar.addSeparator();
add(toolBar, BorderLayout.NORTH);
}
private void setupDocking() {
dockControl = new CControl(this);
dockContent = dockControl.createContentArea("main");
......@@ -554,7 +634,7 @@ public class DebuggerMain extends JFrame {
//TODO statusBar.publishSuccessMessage("Interpreter finished.");
//TODO btnInteractiveMode.setDisable(false);
assert model.getDebuggerFramework() != null;
btnInteractiveMode.setSelected(false);
//TODO btnInteractiveMode.setSelected(false);
PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
assert statePointer != null;
State<KeyData> lastState = statePointer.getStateAfterStmt();
......@@ -1133,7 +1213,7 @@ public class DebuggerMain extends JFrame {
}
public void interactiveMode(ActionEvent actionEvent) {
if (btnInteractiveMode.isSelected()) {
/*TODO if (btnInteractiveMode.isSelected()) {
assert model.getDebuggerFramework() != null;
interactiveModeController.setDebuggerFramework(model.getDebuggerFramework());
interactiveModeController.setKeYServices(this.getFacade().getService());
......@@ -1146,7 +1226,7 @@ public class DebuggerMain extends JFrame {
} else {
interactiveModeController.stop();
//TODO interactive_undo.setDisable(true);
}
}*/
}
......@@ -1350,12 +1430,8 @@ public class DebuggerMain extends JFrame {
}
*/
ContractChooser cc = null;
try {
cc = new ContractChooser(FACADE.getService(), FACADE.getContractsForJavaFile(model.getJavaFile()));
} catch (ProblemLoaderException e) {
e.printStackTrace();
}
//TODO ContractChooser cc = null;
//TODO cc = new ContractChooser(FACADE.getService(), FACADE.getContractsForJavaFile(model.getJavaFile()));
/*TODO cc.showAndWait().ifPresent(result -> {
model.setChosenContract(result);
......@@ -1522,4 +1598,23 @@ public class DebuggerMain extends JFrame {
}
}
//endregion
//region: Actions
public class DummyAction extends AbstractAction {
public DummyAction(String name) {
super(name);
}
@Override
public void actionPerformed(ActionEvent e) {
JOptionPane.showMessageDialog(DebuggerMain.this, "TODO!");
}
}
private class ToggleViewAction extends DummyAction {
public ToggleViewAction(String name) {
super(name);
}
}
//endregion
}
......@@ -4,11 +4,9 @@ import com.google.common.eventbus.EventBus;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.macros.scripts.ScriptCommand;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
......@@ -17,8 +15,8 @@ import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.AllArgsConstructor;
import lombok.Data;
import lombok.RequiredArgsConstructor;
import org.antlr.v4.runtime.Token;
import javax.swing.*;
import java.util.List;
/**
......@@ -44,7 +42,7 @@ public class Events {
@Data
@RequiredArgsConstructor
public static class FocusScriptArea {
private final ScriptArea scriptArea;
private final /*TODO ScriptArea */ JTextArea scriptArea;
}
......
......@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import edu.kit.iti.formal.psdbg.gui.controls.Utils;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
......@@ -36,7 +35,7 @@ public class ScriptExecutionController {
* @param addInitBreakpoint
*/
public void executeScript(boolean addInitBreakpoint) {
/*TODO
if (mainCtrl.getModel().getDebuggerFramework() != null) {
Alert alert = new Alert(Alert.AlertType.CONFIRMATION, "Interpreter is already running \nDo you want to abort it?",
ButtonType.CANCEL, ButtonType.YES);
......@@ -70,6 +69,7 @@ public class ScriptExecutionController {
// else getProofState() == VIRGIN!
executeScript(mainCtrl.FACADE.buildInterpreter(), addInitBreakpoint);
*/
}
/**
* Execute the script that with using the interpreter that is build using the interpreterbuilder
......@@ -78,8 +78,8 @@ public class ScriptExecutionController {
* @param
*/
private void executeScript(InterpreterBuilder ib, boolean addInitBreakpoint) {
/*TODO
try {
Set<Breakpoint> breakpoints = mainCtrl.getScriptController().getBreakpoints();
// get possible scripts and the main script!
List<ProofScript> scripts = mainCtrl.getScriptController().getCombinedAST();
......@@ -104,13 +104,13 @@ public class ScriptExecutionController {
LOGGER.error(e);
Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
}
*/
}
public void executeScriptFromSavePoint(InterpreterBuilder ib, SavePoint point) {
try {
/*TODO try {
Set<Breakpoint> breakpoints = mainCtrl.getScriptController().getBreakpoints();
// get possible scripts and the main script!
List<ProofScript> scripts = mainCtrl.getScriptController().getCombinedAST();
......@@ -145,7 +145,7 @@ public class ScriptExecutionController {
LOGGER.error(e);
Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
}
*/
}
......@@ -159,7 +159,6 @@ public class ScriptExecutionController {
private ASTNode calculateDiff (ASTDiff dff) {
return null;
}
......
package edu.kit.iti.formal.psdbg.gui.model;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import javax.swing.*;
public enum InterpreterThreadState {
NO_THREAD(MaterialDesignIcon.FLASK_EMPTY),
WAIT(MaterialDesignIcon.CLOCK_ALERT),
RUNNING(MaterialDesignIcon.RUN),
ERROR(MaterialDesignIcon.EXCLAMATION),
FINISHED(MaterialDesignIcon.CHECK);
NO_THREAD(null),
WAIT(null),
RUNNING(null),
ERROR(null),
FINISHED(null);
private final MaterialDesignIcon icon;
private final Icon icon;
InterpreterThreadState(MaterialDesignIcon icon) {
InterpreterThreadState(Icon icon) {
this.icon = icon;
}
public MaterialDesignIcon getIcon() {
public Icon getIcon() {
return icon;
}
}
package edu.kit.iti.formal.psdbg.gui.model;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import lombok.AllArgsConstructor;
import lombok.Data;
......@@ -8,6 +7,7 @@ import lombok.RequiredArgsConstructor;
import lombok.ToString;
import javax.annotation.Nonnull;
import javax.swing.*;
import java.util.Collection;
import java.util.Optional;
......@@ -25,7 +25,8 @@ public class MainScriptIdentifier {
private String sourceName;
private int lineNumber;
private String scriptName;
private ScriptArea scriptArea;
//TODO private ScriptArea scriptArea;
private JTextArea scriptArea;
/**
......
......@@ -3,13 +3,13 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.speclang.Contract;
import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleListProperty;
import javafx.collections.ObservableList;
import javafx.scene.control.*;
import javafx.scene.text.Text;
import javafx.scene.text.TextFlow;
import javafx.stage.Modality;
import javax.swing.*;
import java.util.List;
/**
......@@ -23,18 +23,14 @@ import java.util.List;
* @author S. Grebing
* @author A. Weigl
*/
public class ContractChooser extends Dialog<Contract> {
public class ContractChooser extends JDialog {
private final List<Contract> items;
private final MultipleSelectionModel<Contract> selectionModel;
private final ObjectProperty<ObservableList<Contract>> items;
private final ListView<Contract> listOfContractsView = new ListView<>();
private final JList<Contract> listOfContractsView = new JList<>();
private final Services services;
public ContractChooser(Services services,
SimpleListProperty<Contract> contracts) {
public ContractChooser(Services services, List<Contract> contracts) {
this(services);
listOfContractsView.itemsProperty().bind(contracts);
}
......
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