diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index f7128dd0f673767bd36cdbdb2296b83ba2c1aa5d..b4ebe3a1423be882fa2fdedad7491141acc30664 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -145,7 +145,6 @@ public class DebuggerMain implements Initializable { } ); - //Debugging Utils.addDebugListener(javaCode); Utils.addDebugListener(executeNotPossible, "executeNotPossible"); @@ -203,9 +202,6 @@ public class DebuggerMain implements Initializable { imodel.goalsProperty().addListener((observable, oldValue, newValue) -> statusBar.setNumberOfGoals(newValue.size())); - - - /*proofTreeController.currentExecutionEndProperty().addListener((observable, oldValue, newValue) -> { scriptController.getMainScript().getScriptArea().removeExecutionMarker(); LineMapping lm = new LineMapping(scriptController.getMainScript().getScriptArea().getText()); @@ -281,90 +277,21 @@ public class DebuggerMain implements Initializable { } - /* public InspectionViewsController getInspectionViewsController() { - return inspectionViewsController; - } - - public KeYProofFacade getFacade() { - return FACADE; - } - - */ //region Actions: Execution /** * When play button is used */ - @FXML - public void executeScript() { - executorHelper(); - } - - private void executorHelper() { - if (proofTreeController.isAlreadyExecuted()) { - File file; - boolean isKeyfile = false; - if (getJavaFile() != null) { - file = getJavaFile(); - } else { - isKeyfile = true; - file = getKeyFile(); - } - - - Task reloading = reloadEnvironment(file, isKeyfile); - reloading.setOnSucceeded(event -> { - statusBar.publishMessage("Cleared and Reloaded Environment"); - executeScript(FACADE.buildInterpreter(), false); - }); - - reloading.setOnFailed(event -> { - event.getSource().exceptionProperty().get(); - Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment", - (Throwable) event.getSource().exceptionProperty().get() - ); - }); - - ProgressBar bar = new ProgressBar(); - bar.progressProperty().bind(reloading.progressProperty()); - executorService.execute(reloading); - } else { - executeScript(FACADE.buildInterpreter(), false); - } - - } public File getJavaFile() { return javaFile.get(); } //region Actions: Menu - /* @FXML - public void closeProgram() { - System.exit(0); - }*/ - - /* @FXML - public void openScript() { - File scriptFile = openFileChooserOpenDialog("Select Script File", - "Proof Script File", "kps"); - if (scriptFile != null) { - openScript(scriptFile); - } - }*/ - - - /* private void saveScript(File scriptFile) { - try { - scriptController.saveCurrentScriptAs(scriptFile); - } catch (IOException e) { - Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save to file " + scriptFile.getName(), e); - } - } - @FXML + /*@FXML public void saveAsScript() throws IOException { File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps"); if (f != null) { @@ -375,17 +302,7 @@ public class DebuggerMain implements Initializable { } }*/ - /* public void openScript(File scriptFile) { - assert scriptFile != null; - setInitialDirectory(scriptFile.getParentFile()); - try { - String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset()); - ScriptArea area = scriptController.createNewTab(scriptFile); - } catch (IOException e) { - Utils.showExceptionDialog("Exception occured", "", - "Could not load sourceName " + scriptFile, e); - } - }*/ + public void setJavaFile(File javaFile) { this.javaFile.set(javaFile); @@ -423,20 +340,62 @@ public class DebuggerMain implements Initializable { return task; } + @FXML + public void executeScript() { + executorHelper(false); + } + + private void executorHelper(boolean addInitBreakpoint) { + + if (proofTreeController.isAlreadyExecuted()) { + File file; + boolean isKeyfile = false; + if (getJavaFile() != null) { + file = getJavaFile(); + } else { + isKeyfile = true; + file = getKeyFile(); + } + + + Task reloading = reloadEnvironment(file, isKeyfile); + reloading.setOnSucceeded(event -> { + statusBar.publishMessage("Cleared and Reloaded Environment"); + executeScript(FACADE.buildInterpreter(), addInitBreakpoint); + }); + + reloading.setOnFailed(event -> { + event.getSource().exceptionProperty().get(); + Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment", + (Throwable) event.getSource().exceptionProperty().get() + ); + }); + + ProgressBar bar = new ProgressBar(); + bar.progressProperty().bind(reloading.progressProperty()); + executorService.execute(reloading); + } else { + + executeScript(FACADE.buildInterpreter(), addInitBreakpoint); + } + + } + /** * Execute the script that with using the interpreter that is build using the interpreterbuilder * * @param ib - * @param debugMode + * @param */ - private void executeScript(InterpreterBuilder ib, boolean debugMode) { + private void executeScript(InterpreterBuilder ib, boolean addInitBreakpoint) { Set breakpoints = scriptController.getBreakpoints(); if (proofTreeController.isAlreadyExecuted()) { proofTreeController.saveGraphs(); } - this.debugMode.set(debugMode); + + this.debugMode.set(addInitBreakpoint); statusBar.publishMessage("Parse ..."); try { @@ -460,6 +419,7 @@ public class DebuggerMain implements Initializable { } } + statusBar.publishMessage("Creating new Interpreter instance ..."); ib.setScripts(scripts); KeyInterpreter currentInterpreter = ib.build(); @@ -468,7 +428,9 @@ public class DebuggerMain implements Initializable { proofTreeController.setMainScript(scripts.get(n)); statusBar.publishMessage("Executing script " + scripts.get(n).getName()); - + if (addInitBreakpoint) { + breakpoints.add(new Breakpoint(scriptController.getMainScript().getScriptArea().getFilePath(), scriptController.getMainScript().getLineNumber())); + } proofTreeController.executeScript(this.debugMode.get(), statusBar, breakpoints); //highlight signature of main script //scriptController.setDebugMark(scripts.get(0).getStartPosition().getLineNumber()); @@ -477,6 +439,22 @@ public class DebuggerMain implements Initializable { } } + @FXML + public void executeStepwise() { + executorHelper(true); + //executeScript(FACADE.buildInterpreter(), true); + } + + @FXML + public void executeToBreakpoint() { + Set breakpoints = scriptController.getBreakpoints(); + if (breakpoints.size() == 0) { + System.out.println(scriptController.mainScriptProperty().get().getLineNumber()); + //we need to add breakpoint at end if no breakpoint exists + } + executorHelper(false); + } + public void openKeyFile(File keyFile) { if (keyFile != null) { setKeyFile(keyFile); @@ -510,41 +488,21 @@ public class DebuggerMain implements Initializable { } } - /* @FXML - protected void loadKeYFile() { - File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps"); - openKeyFile(keyFile); - } - */ - @FXML - public void executeToBreakpoint() { - Set breakpoints = scriptController.getBreakpoints(); - if (breakpoints.size() == 0) { - //we need to add breakpoint at end if no breakpoint exists - } - executorHelper(); + protected void loadKeYFile() { + File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps"); + openKeyFile(keyFile); } + + //endregion //region Santa's Little Helper - @FXML - public void executeInDebugMode() { - executeScript(FACADE.buildInterpreter(), true); - } - @FXML - public void saveScript() { - try { - scriptController.saveCurrentScript(); - } catch (IOException e) { - Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save current script", e); - } - } public void openJavaFile() { loadJavaFile(); @@ -629,7 +587,7 @@ public class DebuggerMain implements Initializable { } } - /* @FXML + @FXML public void saveScript() { try { scriptController.saveCurrentScript(); @@ -638,7 +596,7 @@ public class DebuggerMain implements Initializable { } } - */ + @FXML public void saveAsScript() throws IOException { File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps"); @@ -675,11 +633,6 @@ public class DebuggerMain implements Initializable { } } - @FXML - protected void loadKeYFile() { - File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps"); - openKeyFile(keyFile); - } /** * Save KeY proof as proof file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java index 01cb2bdc9d42ff96f910e5faad14bbc1bf14390e..f7174ad1c23262c5dda45a9732a83c1e401f1be3 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java @@ -4,6 +4,7 @@ import com.google.common.eventbus.Subscribe; import com.google.common.graph.MutableValueGraph; import edu.kit.iti.formal.psdbg.InterpretingService; import edu.kit.iti.formal.psdbg.gui.controls.DebuggerStatusBar; +import edu.kit.iti.formal.psdbg.gui.controls.Utils; import edu.kit.iti.formal.psdbg.gui.model.Breakpoint; import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; @@ -270,11 +271,11 @@ public class ProofTreeController { blocker.deinstall(); blocker.install(currentInterpreter); - if (!debugMode) { +/* if (!debugMode) { statusBar.setText("Starting in execution mode for script " + mainScript.getName()); statusBar.indicateProgress(); blocker.getStepUntilBlock().set(-1); - } else { + } else {*/ statusBar.setText("Starting in debug mode for script " + mainScript.getName()); statusBar.indicateProgress(); setCurrentHighlightNode(mainScript.get()); @@ -287,8 +288,7 @@ public class ProofTreeController { this.stateGraphWrapper.install(currentInterpreter); this.stateGraphWrapper.addChangeListener(graphChangedListener); statusBar.stopProgress(); - blocker.getStepUntilBlock().set(1); - } + //} //create interpreter service and start if (interpreterService.getState() == Worker.State.SUCCEEDED @@ -302,6 +302,10 @@ public class ProofTreeController { interpreterService.start(); interpreterService.setOnSucceeded(event -> { statusBar.setText("Executed until end of script."); + //TODO is this the right position?? + if (currentGoals.isEmpty()) { + Utils.showClosedProofDialog(mainScript.get().getName()); + } statusBar.stopProgress(); }); interpreterService.setOnFailed(event -> { diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java index de6081d941de064d3085eb697f4195135271e933..9b67cd037f41f3ca5f06d1c1a77c562e3024a319 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java @@ -58,12 +58,14 @@ public class ScriptController { @Subscribe public void handle(Events.NewNodeExecuted newNode) { logger.debug("Handling new node added event!"); + ASTNode scriptNode = newNode.getCorrespondingASTNode(); ScriptArea editor = findEditor(scriptNode); editor.removeExecutionMarker(); LineMapping lm = new LineMapping(editor.getText()); int pos = lm.getLineEnd(scriptNode.getStartPosition().getLineNumber() - 1); - editor.insertExecutionMarker(pos); + System.out.println(pos); + // editor.insertExecutionMarker(pos); } private ScriptArea findEditor(ASTNode node) { diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml index 8667a8eaccae61eaa17c70cd0c4c277f317553d7..07ce7434add85f636a31d07296a0c8ee0b99882b 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml @@ -99,7 +99,7 @@