Commit 439ada64 authored by Sarah Grebing's avatar Sarah Grebing

Merge remote-tracking branch 'origin/luongSavepoint' into luongSavepointTemp

# Conflicts:
#	ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
parents cbbe59a2 affd4938
......@@ -607,9 +607,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
va.declare(entry.getKey(), val.getType());
va.assign(entry.getKey(), val);
} catch (NullPointerException npe) {
System.out.println("Caught Nullpointer in evaluation of Stateless parameters: " + entry.toString()
);
Value val = evaluator.eval(entry.getValue());
va.declare(entry.getKey(), val.getType());
va.assign(entry.getKey(), val);
}
});
return va;
......
package edu.kit.iti.formal.psdbg.interpreter.data;
import com.google.errorprone.annotations.Var;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import lombok.AllArgsConstructor;
......@@ -16,7 +15,7 @@ public class SavePoint {
private final String name;
private int startOffset = -1;
private int endOffset = -1;
private int lineNumer = -1;
private int lineNumber = -1;
private ForceOption force = ForceOption.YES;
public SavePoint(CallStatement call) {
......@@ -28,7 +27,7 @@ public class SavePoint {
try {
startOffset = call.getRuleContext().getStart().getStartIndex();
endOffset = call.getRuleContext().getStart().getStopIndex();
lineNumer = call.getRuleContext().getStart().getLine();
lineNumber = call.getRuleContext().getStart().getLine();
} catch (NullPointerException npe) {
}
} else {
......
......@@ -9,7 +9,6 @@ import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
......@@ -23,6 +22,7 @@ import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
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.SavePoint;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
......@@ -42,11 +42,9 @@ import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import recoder.util.Debug;
import javax.annotation.Nullable;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.*;
import java.util.stream.Collectors;
@Getter
......@@ -77,6 +75,9 @@ public class InteractiveModeController {
private CasesStatement casesStatement;
@Setter @Nullable
private SavePoint savepoint; //not null if interactive mode started from savepoint
public void start(Proof currentProof, InspectionModel model) {
Events.register(this);
cases.clear();
......@@ -148,7 +149,15 @@ public class InteractiveModeController {
Events.unregister(this);
String c = getCasesAsString();
scriptController.getDockNode(scriptArea).undock();
Events.fire(new Events.InsertAtTheEndOfMainScript(c));
if(savepoint == null) {
Events.fire(new Events.InsertAtTheEndOfMainScript(c));
} else {
//TODO: insert Script after Savepoint
System.out.println("Interactive Script should be inserted in line " + savepoint.getLineNumber());
Events.fire(new Events.InsertAtTheEndOfMainScript(c));
}
}
@Subscribe
......
......@@ -65,6 +65,8 @@ import org.reactfx.collection.LiveList;
import org.reactfx.value.Val;
import java.io.File;
import java.nio.file.Files;
import java.nio.file.LinkOption;
import java.time.Duration;
import java.util.*;
import java.util.function.IntFunction;
......@@ -409,8 +411,25 @@ public class ScriptArea extends BorderPane {
gutter.lineAnnotations.forEach(a -> a.setMainScript(false));
if (lineNumber > 0)
gutter.getLineAnnotation(lineNumber - 1).setMainScript(true);
}
/**
* Set marker in gutter at the line of the Savepoint, which is loaded
* @param lineNumber line in where the marker is to be set
*/
public void setSavepointMarker(int lineNumber) {
gutter.lineAnnotations.forEach(a -> a.setSavepoint(false));
gutter.getLineAnnotation(lineNumber - 1).setSavepoint(true);
}
private void underline (int linenumber) {
}
private boolean hasExecutionMarker() {
return getText().contains(EXECUTION_MARKER);
}
......@@ -592,6 +611,10 @@ public class ScriptArea extends BorderPane {
MaterialDesignIcon.CHECK, "12"
);
private MaterialDesignIconView iconSavepoint = new MaterialDesignIconView(
MaterialDesignIcon.CONTENT_SAVE, "12"
);
private Label lineNumber = new Label("not set");
public GutterView(GutterAnnotation ga) {
......@@ -600,6 +623,7 @@ public class ScriptArea extends BorderPane {
old.breakpoint.removeListener(this::update);
old.breakpoint.removeListener(this::update);
old.mainScript.removeListener(this::update);
old.savepoint.removeListener(this::update);
lineNumber.textProperty().unbind();
}
......@@ -607,6 +631,7 @@ public class ScriptArea extends BorderPane {
nv.mainScript.addListener(this::update);
nv.breakpoint.addListener(this::update);
nv.conditional.addListener(this::update);
nv.savepoint.addListener(this::update);
lineNumber.textProperty().bind(nv.textProperty());
......@@ -618,6 +643,7 @@ public class ScriptArea extends BorderPane {
public void update(Observable o) {
getChildren().setAll(lineNumber);
if (getAnnotation().isMainScript()) getChildren().add(iconMainScript);
else if (getAnnotation().isSavepoint()) getChildren().add(iconSavepoint);
else addPlaceholder();
if (getAnnotation().isBreakpoint())
getChildren().add(getAnnotation().getConditional()
......@@ -658,6 +684,8 @@ public class ScriptArea extends BorderPane {
private BooleanProperty mainScript = new SimpleBooleanProperty();
private SimpleBooleanProperty savepoint = new SimpleBooleanProperty();
public String getText() {
return text.get();
}
......@@ -713,6 +741,19 @@ public class ScriptArea extends BorderPane {
public BooleanProperty mainScriptProperty() {
return mainScript;
}
public boolean isSavepoint() {
return savepoint.get();
}
public SimpleBooleanProperty savepointProperty() {
return savepoint;
}
public void setSavepoint(boolean savepoint) {
this.savepoint.set(savepoint);
}
}
public static class BreakpointDialog extends BorderPane {
......@@ -831,6 +872,13 @@ public class ScriptArea extends BorderPane {
@FXML
public void setMainScript(ActionEvent event) {
LOGGER.debug("ScriptAreaContextMenu.setMainScript");
// Check if script is saved
if(!filePath.getValue().isFile()) {
Utils.showInfoDialog("Saving Script", "Save Script", "Script has to be saved first before it can be executed.");
return;
}
List<ProofScript> ast = Facade.getAST(getText());
int pos = currentMouseOver.get().getInsertionIndex();
ast.stream().filter(ps ->
......@@ -841,6 +889,8 @@ public class ScriptArea extends BorderPane {
new MainScriptIdentifier(filePath.get().getAbsolutePath(),
proofScript.getStartPosition().getLineNumber(),
proofScript.getName(), ScriptArea.this)));
}
@FXML
......
......@@ -10,11 +10,10 @@ import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier;
import edu.kit.iti.formal.psdbg.gui.controller.Events;
import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.beans.property.ListProperty;
import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleListProperty;
......@@ -93,6 +92,35 @@ public class ScriptController {
}
}
/*
public int getLineOfSavepoint(SavePoint sp) {
Optional<ProofScript> ms = getMainScript(). find(getCombinedAST());
if(ms.isPresent()) {
List<CallStatement> list = ms.get().getBody().stream()
.filter(SavePoint::isSaveCommand)
.map(a -> (CallStatement) a).
collect(Collectors.toList());
if(!list.isEmpty()) {
for(int i = 0; i < list.size(); i++) {
if(true) {
Parameters param = list.get(i).getParameters();
String splistname = ((StringLiteral) param.get(new Variable("#2"))).getText();
if(splistname.equals(sp.getName())) {
int index = ms.get().getBody().indexOf(list.get(i));
return ms.get().getBody().get(index).getStartPosition().getLineNumber();
}
}
}
}
}
return -1;
}
*/
private void addDefaultInlineActions() {
actionSuppliers.add(new FindLabelInGoalList());
actionSuppliers.add(new FindTermLiteralInSequence());
......
......@@ -51,7 +51,7 @@ public class SequentOptionsMenu extends ContextMenu {
} catch (Exception e) {
Utils.showInfoDialog("Please Select a Goal first." ,
"Please Select a Goal node from the list first to open the SequentMatcher Window.",
"Please Select a Goal node from the list first to open the SequentMatcher Window.", e);
"Please Select a Goal node from the list first to open the SequentMatcher Window.");
// e.printStackTrace();
// System.out.println(e);
}
......
......@@ -211,7 +211,7 @@ public class Utils {
StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw);
ex.printStackTrace(pw);
String exceptionText = sw.toString();
alert.setWidth(400);
......@@ -224,15 +224,12 @@ public class Utils {
alert.showAndWait();
}
public static void showInfoDialog(String title, String headerText, String contentText, Throwable ex) {
public static void showInfoDialog(String title, String headerText, String contentText) {
Alert alert = new Alert(Alert.AlertType.INFORMATION);
alert.setTitle(title);
alert.setHeaderText(headerText);
alert.setContentText(contentText);
StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw);
ex.printStackTrace(pw);
String exceptionText = sw.toString();
alert.setWidth(400);
......
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