Commit 07008761 authored by Sarah Grebing's avatar Sarah Grebing

interim

parent 2978eada
......@@ -14,6 +14,10 @@ public class StepIntoReverseCommand<T> extends DebuggerCommand<T> {
PTreeNode<T> statementBefore = statePointer.getStepInvOver();
dbg.setStatePointer(statementBefore);
} else {
if (statePointer.isLastNode() || statePointer.isFirstNode()) {
System.out.println("We need Sonderbehandlung here");
}
}
}
......
......@@ -957,11 +957,22 @@ public class DebuggerMain implements Initializable {
public void stepIntoReverse(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepIntoReverser");
try {
if (model.getDebuggerFramework().getStatePointer().isAtomic()) {
model.getDebuggerFramework().getStatePointerListener()
.add(new StepIntoReverseHandler(model.getStatePointer()));
PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
if (statePointer.getStepInvInto() == null) {
if (statePointer.getStepInvOver() != null) {
if (statePointer.getStepInvOver().isAtomic()) {
model.getDebuggerFramework().getStatePointerListener()
.add(new StepIntoReverseHandler(model.getStatePointer()));
}
model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
} else {
if (statePointer.isLastNode() || statePointer.isFirstNode()) {
LOGGER.error("We need a special treatment");
} else {
LOGGER.error("There is no state to step into reverse");
}
}
}
model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
} catch (DebuggerException e) {
Utils.showExceptionDialog("", "", "", e);
LOGGER.error(e);
......@@ -1232,7 +1243,6 @@ public class DebuggerMain implements Initializable {
Proof proof = beforeNode.getData().getProof();
Node pnode = beforeNode.getData().getNode();
// stateAfterStmt.forEach(keyDataGoalNode -> System.out.println("keyDataGoalNode.getData().getNode().serialNr() = " + keyDataGoalNode.getData().getNode().serialNr()));
ptree.setProof(proof);
ptree.setRoot(pnode);
......
// Please select one of the following scripts.
//
script autoScript(){
auto;
}
script test1234(){
impRight;
autoScript;
//auto;
}
script test23(){
impRight;
x:term := find(match `?rt ==>`);
impLeft formula=x;
//x:term := find(match `?rt ==>`);
//impLeft formula=x;
impLeft formula=find(match `?rt ==>`);
cases{
case match `q==>`:
......
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