Commit de3bd0cf authored by Lulu Luong's avatar Lulu Luong

Savepoint: gutter annotation for skipping and selecting + adapt interactive dialog

parent 57cce75f
......@@ -60,7 +60,8 @@ public class SaveCommand implements CommandHandler<KeyData> {
Semaphore semaphore = new Semaphore(0);
Platform.runLater(() -> {
Alert a = new Alert(Alert.AlertType.CONFIRMATION);
a.setTitle("Foo");
a.setTitle("Overwrite proof file");
a.setContentText("Overwrite existing proof file \"" + sp.getName()+"\" (line "+ sp.getLineNumber() +") ?");
Optional<ButtonType> buttonType = a.showAndWait();
if(buttonType.isPresent() && buttonType.get() == ButtonType.OK){
execute.set(true);
......
......@@ -44,6 +44,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
goal = node;
}
/**
* Evaluation of an expression.
*
......@@ -78,10 +79,12 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
Value pattern = (Value) match.getPattern().accept(this);
if (match.isDerivable()) {
} else {
if (pattern.getType() == SimpleType.STRING) {
va = matcher.matchLabel(goal, (String) pattern.getData());
} else if (TypeFacade.isTerm(pattern.getType())) {
va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature());
if (goal != null) {
if (pattern.getType() == SimpleType.STRING) {
va = matcher.matchLabel(goal, (String) pattern.getData());
} else if (TypeFacade.isTerm(pattern.getType())) {
va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature());
}
}
}
......@@ -109,7 +112,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
@Override
public Value visit(Variable variable) {
//get variable value
Value v = state.getValue(variable);
Value v = (state != null)? state.getValue(variable) : null;
if (v != null) {
return v;
} else {
......@@ -153,8 +156,8 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
if (t != null)
newVal = ((Value) t.accept(this)).getData().toString();
else
newVal = state.getValue(new Variable(name)).getData().toString();
m.appendReplacement(newTerm, newVal);
if (state != null) newVal = state.getValue(new Variable(name)).getData().toString();
m.appendReplacement(newTerm, newVal);
}
m.appendTail(newTerm);
return new Value<>(TypeFacade.ANY_TERM, newTerm.toString());
......
......@@ -599,7 +599,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
private VariableAssignment evaluateParametersStateLess(Parameters parameters) {
VariableAssignment va = new VariableAssignment();
Evaluator<T> evaluator = createEvaluator(null, null);
Evaluator<T> evaluator = new Evaluator<>(null, null);
parameters.entrySet().forEach(entry -> {
try {
......
......@@ -1173,6 +1173,11 @@ public class DebuggerMain implements Initializable {
LOGGER.info("Reloaded Successfully");
statusBar.publishMessage("Reloaded Sucessfully");
}
//TODO: check again
scriptController.getMainScript().getScriptArea().setSavepointMarker(selected.getLineNumber());
scriptController.getMainScript().getScriptArea().getCodeArea().setStyleClass(selected.getStartOffset(), selected.getEndOffset() + 1, "problem");
} catch (ProofInputException | ProblemLoaderException e) {
LOGGER.error(e);
Utils.showExceptionDialog("Loading Error", "Could not clear Environment",
......
......@@ -160,5 +160,7 @@ public class ScriptExecutionController {
}
//TODO: calc diff
}
......@@ -424,12 +424,13 @@ public class ScriptArea extends BorderPane {
}
private void underline (int linenumber) {
public void setAlertMarker(int lineNumber) {
gutter.getLineAnnotation(lineNumber - 1).setAlert(true);
}
private boolean hasExecutionMarker() {
return getText().contains(EXECUTION_MARKER);
}
......@@ -615,6 +616,10 @@ public class ScriptArea extends BorderPane {
MaterialDesignIcon.CONTENT_SAVE, "12"
);
private MaterialDesignIconView iconSkippedSave = new MaterialDesignIconView(
MaterialDesignIcon.ALERT, "12"
);
private Label lineNumber = new Label("not set");
public GutterView(GutterAnnotation ga) {
......@@ -645,6 +650,8 @@ public class ScriptArea extends BorderPane {
if (getAnnotation().isMainScript()) getChildren().add(iconMainScript);
else if (getAnnotation().isSavepoint()) getChildren().add(iconSavepoint);
else addPlaceholder();
if (getAnnotation().isAlert()) getChildren().add(iconSkippedSave);
else addPlaceholder();
if (getAnnotation().isBreakpoint())
getChildren().add(getAnnotation().getConditional()
? iconConditionalBreakPoint
......@@ -686,6 +693,21 @@ public class ScriptArea extends BorderPane {
private SimpleBooleanProperty savepoint = new SimpleBooleanProperty();
//for now specifically for skipped saved commands
private SimpleBooleanProperty alert = new SimpleBooleanProperty();
public boolean isAlert() {
return alert.get();
}
public SimpleBooleanProperty alertProperty() {
return alert;
}
public void setAlert(boolean alert) {
this.alert.set(alert);
}
public String getText() {
return text.get();
}
......
......@@ -73,6 +73,8 @@ public class ScriptController {
if (o != null)
o.getScriptArea().textProperty().removeListener(a -> updateSavePoints());
n.getScriptArea().textProperty().addListener(a -> updateSavePoints());
updateSavePoints();
});
......@@ -87,39 +89,19 @@ public class ScriptController {
.map(a -> (CallStatement) a)
.map(SavePoint::new)
.collect(Collectors.toList());
mainScriptSavePoints.setAll(list);
loggerConsole.info("Found savepoints: " + list);
}
}
/*
public int getLineOfSavepoint(SavePoint sp) {
Optional<ProofScript> ms = getMainScript(). find(getCombinedAST());
//set alert gutter annotations
List<SavePoint> noForceSp = mainScriptSavePoints.stream()
.filter(a -> a.getForce().equals(SavePoint.ForceOption.NO))
.collect(Collectors.toList());
noForceSp.forEach( e -> getMainScript().getScriptArea().setAlertMarker(e.getLineNumber()));
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();
}
}
}
}
loggerConsole.info("Found savepoints: " + list);
}
return -1;
}
*/
private void addDefaultInlineActions() {
actionSuppliers.add(new FindLabelInGoalList());
......@@ -348,6 +330,7 @@ public class ScriptController {
}
public void setMainScript(ProofScript proofScript) {
MainScriptIdentifier msi = new MainScriptIdentifier();
msi.setLineNumber(proofScript.getStartPosition().getLineNumber());
msi.setScriptName(proofScript.getName());
......
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