Commit 4efda617 authored by Sarah Grebing's avatar Sarah Grebing

first ideas for reloading after executing. Need to clear inspection view or create new tab.

parent 385d3f9a
Pipeline #12746 failed with stage
in 1 minute and 28 seconds
...@@ -224,9 +224,55 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -224,9 +224,55 @@ public class DebuggerMainWindowController implements Initializable {
//region Actions: Execution //region Actions: Execution
@FXML @FXML
public void executeScript() { public void executeScript() {
executeScript(FACADE.buildInterpreter(), false); if (proofTreeController.isAlreadyExecuted()) {
File file;
boolean isKeyfile = false;
if (getJavaFile() != null) {
file = getJavaFile();
} else {
isKeyfile = true;
file = getKeyFile();
}
Task<Void> 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 Task<Void> reloadEnvironment(File file, boolean keyfile) {
Task<Void> task = new Task<Void>() {
@Override
protected Void call() throws Exception {
FACADE.reloadEnvironment();
if (keyfile) {
openKeyFile(file);
} else {
openJavaFile(file);
}
return null;
}
};
return task;
} }
@FXML @FXML
public void executeScriptFromCursor() { public void executeScriptFromCursor() {
InterpreterBuilder ib = FACADE.buildInterpreter(); InterpreterBuilder ib = FACADE.buildInterpreter();
...@@ -252,9 +298,11 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -252,9 +298,11 @@ public class DebuggerMainWindowController implements Initializable {
* @param debugMode * @param debugMode
*/ */
private void executeScript(InterpreterBuilder ib, boolean debugMode) { private void executeScript(InterpreterBuilder ib, boolean debugMode) {
this.debugMode.set(debugMode); this.debugMode.set(debugMode);
statusBar.publishMessage("Parse ..."); statusBar.publishMessage("Parse ...");
try { try {
List<ProofScript> scripts = scriptController.getCombinedAST(); List<ProofScript> scripts = scriptController.getCombinedAST();
statusBar.publishMessage("Creating new Interpreter instance ..."); statusBar.publishMessage("Creating new Interpreter instance ...");
ib.setScripts(scripts); ib.setScripts(scripts);
...@@ -288,14 +336,19 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -288,14 +336,19 @@ public class DebuggerMainWindowController implements Initializable {
@FXML @FXML
public void saveScript() { public void saveScript() {
scriptController.saveCurrentScript(); try {
scriptController.saveCurrentScript();
} catch (IOException e) {
Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save current script", e);
}
} }
private void saveScript(File scriptFile) { private void saveScript(File scriptFile) {
try { try {
scriptController.saveCurrentScriptAs(scriptFile); scriptController.saveCurrentScriptAs(scriptFile);
} catch (IOException e) { } catch (IOException e) {
Utils.showExceptionDialog("Could not save sourceName", "blubb", "...fsfsfsf fsa", e); Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save to file " + scriptFile.getName(), e);
} }
} }
...@@ -351,9 +404,18 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -351,9 +404,18 @@ public class DebuggerMainWindowController implements Initializable {
} }
} }
/**
* Save KeY proof as proof file
*
* @param actionEvent
*/
public void saveProof(ActionEvent actionEvent) { public void saveProof(ActionEvent actionEvent) {
LOGGER.error("saveProof not implemented!!!"); LOGGER.error("saveProof not implemented!!!");
} }
//endregion //endregion
//region Santa's Little Helper //region Santa's Little Helper
......
...@@ -103,6 +103,12 @@ public class ScriptController { ...@@ -103,6 +103,12 @@ public class ScriptController {
} }
} }
/**
* Create new DockNode for ScriptArea Tab
*
* @param area ScriptAreaTab
* @return
*/
private DockNode createDockNode(ScriptArea area) { private DockNode createDockNode(ScriptArea area) {
DockNode dockNode = new DockNode(area, area.getFilePath().getName(), new MaterialDesignIconView(MaterialDesignIcon.FILE_DOCUMENT)); DockNode dockNode = new DockNode(area, area.getFilePath().getName(), new MaterialDesignIconView(MaterialDesignIcon.FILE_DOCUMENT));
dockNode.closedProperty().addListener(o -> { dockNode.closedProperty().addListener(o -> {
......
...@@ -5,6 +5,7 @@ import edu.kit.formal.gui.controls.Utils; ...@@ -5,6 +5,7 @@ import edu.kit.formal.gui.controls.Utils;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State; import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty; import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Service; import javafx.concurrent.Service;
import javafx.concurrent.Task; import javafx.concurrent.Task;
...@@ -30,15 +31,23 @@ public class InterpretingService extends Service<State<KeyData>> { ...@@ -30,15 +31,23 @@ public class InterpretingService extends Service<State<KeyData>> {
* The blocker, necessary for controlling how far the script should be interpreted * The blocker, necessary for controlling how far the script should be interpreted
*/ */
private PuppetMaster blocker; private PuppetMaster blocker;
/**
* Property that is set if this service has run successfully
*/
private SimpleBooleanProperty hasRunSucessfully = new SimpleBooleanProperty(false);
public InterpretingService(PuppetMaster blocker) { public InterpretingService(PuppetMaster blocker) {
this.blocker = blocker; this.blocker = blocker;
} }
public SimpleBooleanProperty hasRunSucessfullyProperty() {
return hasRunSucessfully;
}
@Override @Override
protected void succeeded() { protected void succeeded() {
System.out.println("Finished executing"); System.out.println("Finished executing");
hasRunSucessfully.setValue(true);
updateView(); updateView();
} }
......
...@@ -82,8 +82,6 @@ public class KeYProofFacade { ...@@ -82,8 +82,6 @@ public class KeYProofFacade {
/** /**
* Build the KeYInterpreter that handles the execution of the loaded key problem sourceName * Build the KeYInterpreter that handles the execution of the loaded key problem sourceName
* *
* @param keYFile
* @param scriptText
*/ */
public InterpreterBuilder buildInterpreter() { public InterpreterBuilder buildInterpreter() {
assert readyToExecute.getValue(); assert readyToExecute.getValue();
...@@ -101,6 +99,18 @@ public class KeYProofFacade { ...@@ -101,6 +99,18 @@ public class KeYProofFacade {
} }
/**
* Reload all KeY structure if proof should be reloaded
*
* @param fileToLoad
*/
public void reloadEnvironment() {
setProof(null);
setEnvironment(null);
setContract(null);
pma = null;
}
//region Getter and Setters //region Getter and Setters
public Services getService() { public Services getService() {
//FIXME if key api relaxed //FIXME if key api relaxed
......
...@@ -47,6 +47,10 @@ public class ProofTreeController { ...@@ -47,6 +47,10 @@ public class ProofTreeController {
*/ */
private InterpretingService interpreterService = new InterpretingService(blocker); private InterpretingService interpreterService = new InterpretingService(blocker);
private ReadOnlyBooleanProperty alreadyExecuted = interpreterService.hasRunSucessfullyProperty();
/** /**
* To identify when interpreterservice is running * To identify when interpreterservice is running
*/ */
...@@ -216,6 +220,7 @@ public class ProofTreeController { ...@@ -216,6 +220,7 @@ public class ProofTreeController {
*/ */
public void executeScript(boolean debugMode) { public void executeScript(boolean debugMode) {
Events.register(this); Events.register(this);
blocker.deinstall(); blocker.deinstall();
blocker.install(currentInterpreter); blocker.install(currentInterpreter);
if (!debugMode) { if (!debugMode) {
...@@ -234,7 +239,7 @@ public class ProofTreeController { ...@@ -234,7 +239,7 @@ public class ProofTreeController {
} }
//create interpreter service and start //create interpreter service and start
if (interpreterService.getState() == Worker.State.SUCCEEDED) { if (interpreterService.getState() == Worker.State.SUCCEEDED || interpreterService.getState() == Worker.State.CANCELLED) {
interpreterService.reset(); interpreterService.reset();
} }
interpreterService.interpreterProperty().set(currentInterpreter); interpreterService.interpreterProperty().set(currentInterpreter);
...@@ -330,4 +335,10 @@ public class ProofTreeController { ...@@ -330,4 +335,10 @@ public class ProofTreeController {
public ObjectProperty<ASTNode> currentHighlightNodeProperty() { public ObjectProperty<ASTNode> currentHighlightNodeProperty() {
return currentHighlightNode; return currentHighlightNode;
} }
public boolean isAlreadyExecuted() {
return alreadyExecuted.get();
}
} }
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