Commit bd990c81 authored by Alexander Weigl's avatar Alexander Weigl

fixes for interactive mode

parent c09d5c41
Pipeline #16892 failed with stages
in 85 minutes and 33 seconds
...@@ -80,7 +80,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -80,7 +80,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
* starting point is a statement list * starting point is a statement list
*/ */
public void interpret(ProofScript script) { public void interpret(ProofScript script) {
enterScope(script); //enterScope(script);
if (stateStack.empty()) { if (stateStack.empty()) {
throw new InterpreterRuntimeException("no state on stack. call newState before interpret"); throw new InterpreterRuntimeException("no state on stack. call newState before interpret");
} }
...@@ -92,7 +92,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -92,7 +92,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
getSelectedNode().getAssignments().push(va)); getSelectedNode().getAssignments().push(va));
} }
script.accept(this); script.accept(this);
exitScope(script); //exitScope(script);
} }
/** /**
......
...@@ -43,11 +43,8 @@ public class InteractiveModeController { ...@@ -43,11 +43,8 @@ public class InteractiveModeController {
private static final Logger LOGGER = LogManager.getLogger(InteractiveModeController.class); private static final Logger LOGGER = LogManager.getLogger(InteractiveModeController.class);
private final Map<Node, Statements> cases = new HashMap<>(); private final Map<Node, Statements> cases = new HashMap<>();
private BooleanProperty activated = new SimpleBooleanProperty();
private final ScriptController scriptController; private final ScriptController scriptController;
private BooleanProperty activated = new SimpleBooleanProperty();
private ScriptArea scriptArea; private ScriptArea scriptArea;
private InspectionModel model; private InspectionModel model;
...@@ -157,10 +154,13 @@ public class InteractiveModeController { ...@@ -157,10 +154,13 @@ public class InteractiveModeController {
ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(g.node()); ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(g.node());
goals.remove(expandedNode); goals.remove(expandedNode);
GoalNode<KeyData> last = null;
for (Goal newGoalNode : ngoals) { for (Goal newGoalNode : ngoals) {
KeyData kdn = new KeyData(kd, newGoalNode.node()); KeyData kdn = new KeyData(kd, newGoalNode.node());
goals.add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed())); goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
} }
if (last != null)
model.setSelectedGoalNodeToShow(last);
} catch (Exception e) { } catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) { if (e.getClass().equals(ScriptException.class)) {
System.out.println("e.getMessage() = " + e.getMessage()); System.out.println("e.getMessage() = " + e.getMessage());
......
...@@ -142,12 +142,13 @@ public class ScriptArea extends BorderPane { ...@@ -142,12 +142,13 @@ public class ScriptArea extends BorderPane {
codeArea.setMinSize(scrollPane.getWidth(), scrollPane.getHeight()); codeArea.setMinSize(scrollPane.getWidth(), scrollPane.getHeight());
}); });
/*
scrollPane.estimatedScrollYProperty().addListener(new ChangeListener<Double>() { scrollPane.estimatedScrollYProperty().addListener(new ChangeListener<Double>() {
@Override @Override
public void changed(ObservableValue<? extends Double> observable, Double oldValue, Double newValue) { public void changed(ObservableValue<? extends Double> observable, Double oldValue, Double newValue) {
System.out.println("SCROLL:" + newValue); System.out.println("SCROLL:" + newValue);
} }
}); });*/
codeArea.setWrapText(true); codeArea.setWrapText(true);
gutter = new GutterFactory(); gutter = new GutterFactory();
......
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