Commit ef5271b4 authored by Sarah Grebing's avatar Sarah Grebing

fix interactive mode

parent 6b3f4efe
Pipeline #17887 failed with stages
in 11 seconds
...@@ -39,7 +39,7 @@ import lombok.Setter; ...@@ -39,7 +39,7 @@ import lombok.Setter;
@RequiredArgsConstructor @RequiredArgsConstructor
@AllArgsConstructor @AllArgsConstructor
public abstract class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> { public abstract class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> {
protected Statements body; protected Statements body = new Statements();
/** /**
* {@inheritDoc} * {@inheritDoc}
......
...@@ -74,6 +74,8 @@ public class InteractiveModeController { ...@@ -74,6 +74,8 @@ public class InteractiveModeController {
private boolean moreThanOneMatch = false; private boolean moreThanOneMatch = false;
private CasesStatement casesStatement;
public void start(Proof currentProof, InspectionModel model) { public void start(Proof currentProof, InspectionModel model) {
Events.register(this); Events.register(this);
cases.clear(); cases.clear();
...@@ -83,7 +85,17 @@ public class InteractiveModeController { ...@@ -83,7 +85,17 @@ public class InteractiveModeController {
}); });
this.scriptArea = scriptController.newScript(); this.scriptArea = scriptController.newScript();
this.model = model; this.model = model;
casesStatement = new CasesStatement();
cases.forEach((k, v) -> {
val gcs = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
format(LabelFactory.getBranchingLabel(k))
));
gcs.setGuard(m);
gcs.setBody(v);
casesStatement.getCases().add(gcs);
});
savepointslist = new ArrayList<>(); savepointslist = new ArrayList<>();
savepointsstatement = new ArrayList<>(); savepointsstatement = new ArrayList<>();
nodeAtInteractionStart = debuggerFramework.getStatePointer(); nodeAtInteractionStart = debuggerFramework.getStatePointer();
...@@ -219,20 +231,8 @@ public class InteractiveModeController { ...@@ -219,20 +231,8 @@ public class InteractiveModeController {
} }
public String getCasesAsString() { public String getCasesAsString() {
CasesStatement c = new CasesStatement();
cases.forEach((k, v) -> {
val gcs = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
format(LabelFactory.getBranchingLabel(k))
));
gcs.setGuard(m);
gcs.setBody(v);
c.getCases().add(gcs);
});
PrettyPrinter pp = new PrettyPrinter(); PrettyPrinter pp = new PrettyPrinter();
c.accept(pp); casesStatement.accept(pp);
return pp.toString(); return pp.toString();
} }
...@@ -290,9 +290,14 @@ public class InteractiveModeController { ...@@ -290,9 +290,14 @@ public class InteractiveModeController {
for (Goal newGoalNode : ngoals) { for (Goal newGoalNode : ngoals) {
KeyData kdn = new KeyData(kd, newGoalNode.node()); KeyData kdn = new KeyData(kd, newGoalNode.node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed())); goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
cases.put(last.getData().getNode(), new Statements()); val caseForSubNode = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
format(LabelFactory.getBranchingLabel(newGoalNode.node()))
));
caseForSubNode.setGuard(m);
inner.getCases().add(caseForSubNode);
cases.put(last.getData().getNode(), caseForSubNode.getBody());
} }
} else { } else {
KeyData kdn = new KeyData(kd, ngoals.get(0).node()); KeyData kdn = new KeyData(kd, ngoals.get(0).node());
......
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