Skip to content

P
ProofScriptParser
Commit 96b2b783 authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

planning for conceptual merge of actions

parent b8ec7a67
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 373 additions and 290 deletions
src/main/java/edu/kit/formal/gui/controls/LineMapping.java
View file @ 96b2b783
......@@ -8,6 +8,9 @@ import java.util.List;
* @version 1 (04.06.17)
*/
public class LineMapping {
/**
* Position of new lines in the given string value.
*/
private List<Integer> marks = new ArrayList<>();
public LineMapping(String value) {
......@@ -29,14 +32,14 @@ public class LineMapping {
return marks.size();
}
public int getLineStart(int line) {
return marks.get(line);
}
public int getLineEnd(int line) {
return getLineStart(line + 1) - 1;
}
public int getLineStart(int line) {
return marks.get(line);
}
public int getCharInLine(int caretPosition) {
return caretPosition - getLineStart(getLine(caretPosition));
}
......
src/main/java/edu/kit/formal/gui/controls/ScriptArea.java
View file @ 96b2b783
......@@ -149,29 +149,43 @@ public class ScriptArea extends CodeArea {
}
private void highlightNonExecutionArea() {
if (hasExecutionMarker()) {
getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> {
span.getStyle().add("NON_EXE_AREA");
});
//setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA"));
}
}
private void installPopup() {
javafx.stage.Popup popup = new javafx.stage.Popup();
setMouseOverTextDelay(Duration.ofSeconds(1));
addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_BEGIN, e -> {
int chIdx = e.getCharacterIndex();
popup.getContent().setAll(
createPopupInformation(chIdx)
);
private boolean hasExecutionMarker() {
return getText().contains(EXECUTION_MARKER);
Point2D pos = e.getScreenPosition();
popup.show(this, pos.getX(), pos.getY() + 10);
});
/*
addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_END, e -> {
popup.hide();
});*/
popup.setAutoHide(true);
}
public void showContextMenu(MouseEvent mouseEvent) {
if (contextMenu.isShowing())
contextMenu.hide();
private void updateMainScriptMarker() {
try {
MainScriptIdentifier ms = mainScript.get();
LOGGER.debug("ScriptArea.updateMainScriptMarker");
if (mouseEvent.getButton() == MouseButton.SECONDARY) {
contextMenu.setAutoHide(true);
contextMenu.show(this, mouseEvent.getScreenX(), mouseEvent.getScreenY());
mouseEvent.consume();
} else {
if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) {
System.out.println(ms);
CharStream stream = CharStreams.fromString(getText(), filePath.get().getAbsolutePath());
Optional<ProofScript> ps = ms.find(Facade.getAST(stream));
if (ps.isPresent()) {
setMainMarker(ps.get().getStartPosition().getLineNumber());
return;
}
}
setMainMarker(-1);
} catch (NullPointerException e) {
}
}
......@@ -190,44 +204,30 @@ public class ScriptArea extends CodeArea {
});
}
private void updateMainScriptMarker() {
private void highlightProblems() {
LinterStrategy ls = LinterStrategy.getDefaultLinter();
try {
MainScriptIdentifier ms = mainScript.get();
LOGGER.debug("ScriptArea.updateMainScriptMarker");
if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) {
System.out.println(ms);
CharStream stream = CharStreams.fromString(getText(), filePath.get().getAbsolutePath());
Optional<ProofScript> ps = ms.find(Facade.getAST(stream));
if (ps.isPresent()) {
setMainMarker(ps.get().getStartPosition().getLineNumber());
return;
problems.setAll(ls.check(Facade.getAST(CharStreams.fromString(getText()))));
for (LintProblem p : problems) {
for (Token tok : p.getMarkTokens()) {
Set<String> problem = new HashSet<>();
problem.add("problem");
setStyle(tok.getStartIndex(),
tok.getStopIndex() + 1, problem);
}
}
setMainMarker(-1);
} catch (NullPointerException e) {
} catch (Exception e) {
//catch parsing exceptions
}
}
private void installPopup() {
javafx.stage.Popup popup = new javafx.stage.Popup();
setMouseOverTextDelay(Duration.ofSeconds(1));
addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_BEGIN, e -> {
int chIdx = e.getCharacterIndex();
popup.getContent().setAll(
createPopupInformation(chIdx)
);
Point2D pos = e.getScreenPosition();
popup.show(this, pos.getX(), pos.getY() + 10);
});
/*
addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_END, e -> {
popup.hide();
});*/
popup.setAutoHide(true);
private void highlightNonExecutionArea() {
if (hasExecutionMarker()) {
getStyleSpans(0, getExecutionMarkerPosition()).forEach(span -> {
span.getStyle().add("NON_EXE_AREA");
});
//setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA"));
}
}
private Node createPopupInformation(int chIdx) {
......@@ -245,20 +245,30 @@ public class ScriptArea extends CodeArea {
return box;
}
private void highlightProblems() {
LinterStrategy ls = LinterStrategy.getDefaultLinter();
try {
problems.setAll(ls.check(Facade.getAST(CharStreams.fromString(getText()))));
for (LintProblem p : problems) {
for (Token tok : p.getMarkTokens()) {
Set<String> problem = new HashSet<>();
problem.add("problem");
setStyle(tok.getStartIndex(),
tok.getStopIndex() + 1, problem);
}
}
} catch (Exception e) {
//catch parsing exceptions
public void setMainMarker(int lineNumber) {
gutter.lineAnnotations.forEach(a -> a.setMainScript(false));
if (lineNumber > 0)
gutter.getLineAnnotation(lineNumber - 1).setMainScript(true);
}
private boolean hasExecutionMarker() {
return getText().contains(EXECUTION_MARKER);
}
public int getExecutionMarkerPosition() {
return getText().lastIndexOf(EXECUTION_MARKER);
}
public void showContextMenu(MouseEvent mouseEvent) {
if (contextMenu.isShowing())
contextMenu.hide();
if (mouseEvent.getButton() == MouseButton.SECONDARY) {
contextMenu.setAutoHide(true);
contextMenu.show(this, mouseEvent.getScreenX(), mouseEvent.getScreenY());
mouseEvent.consume();
} else {
}
}
......@@ -274,11 +284,6 @@ public class ScriptArea extends CodeArea {
return mainScript;
}
public void setText(String text) {
clear();
insertText(0, text);
}
private void toggleBreakpoint(int idx) {
GutterAnnotation a = gutter.getLineAnnotation(idx);
a.setBreakpoint(!a.isBreakpoint());
......@@ -296,12 +301,6 @@ public class ScriptArea extends CodeArea {
return filePath;
}
public void setMainMarker(int lineNumber) {
gutter.lineAnnotations.forEach(a -> a.setMainScript(false));
if (lineNumber > 0)
gutter.getLineAnnotation(lineNumber - 1).setMainScript(true);
}
public Collection<? extends Breakpoint> getBreakpoints() {
List<Breakpoint> list = new ArrayList<>();
int line = 0;
......@@ -384,6 +383,11 @@ public class ScriptArea extends CodeArea {
//Events.unregister(this);
}
public void setText(String text) {
clear();
insertText(0, text);
}
private String getTextWithoutMarker() {
return getText().replace("" + EXECUTION_MARKER, "");
}
......@@ -403,7 +407,7 @@ public class ScriptArea extends CodeArea {
String tapName = tap.getApp().taclet().displayName();
SequentFormula seqForm = tap.getPio().sequentFormula();
//transofrm term to parsable string representation
//transform term to parsable string representation
String term = Utils.toPrettyTerm(seqForm.formula());
......@@ -429,12 +433,6 @@ public class ScriptArea extends CodeArea {
}
public int getExecutionMarkerPosition() {
return getText().lastIndexOf(EXECUTION_MARKER);
}
private static class GutterView extends HBox {
private final SimpleObjectProperty<GutterAnnotation> annotation = new SimpleObjectProperty<>();
......@@ -484,6 +482,10 @@ public class ScriptArea extends CodeArea {
addPlaceholder();
}
public GutterAnnotation getAnnotation() {
return annotation.get();
}
private void addPlaceholder() {
Label lbl = new Label();
lbl.setMinWidth(12);
......@@ -491,11 +493,6 @@ public class ScriptArea extends CodeArea {
getChildren().add(lbl);
}
public GutterAnnotation getAnnotation() {
return annotation.get();
}
public void setAnnotation(GutterAnnotation annotation) {
this.annotation.set(annotation);
}
......
src/main/java/edu/kit/formal/gui/controls/SequentView.java
View file @ 96b2b783
......@@ -59,6 +59,18 @@ public class SequentView extends CodeArea {
mouseEvent.consume();
}
private void hightlightRange(int start, int end) {
try {
clearHighlight();
setStyleClass(start, end, "sequent-highlight");
} catch (IllegalStateException e) {
}
}
private void clearHighlight() {
clearStyle(0, getLength());
}
public void onMouseClick(MouseEvent e) {
if (menu != null && menu.isShowing()) {
menu.hide();
......@@ -94,18 +106,6 @@ public class SequentView extends CodeArea {
}
private void hightlightRange(int start, int end) {
try {
clearHighlight();
setStyleClass(start, end, "sequent-highlight");
} catch (IllegalStateException e) {
}
}
private void clearHighlight() {
clearStyle(0, getLength());
}
public void update(Observable o) {
Services services = node.get().proof().getEnv().getServicesForEnvironment();
NamespaceSet nss = services.getNamespaces();
......@@ -130,8 +130,15 @@ public class SequentView extends CodeArea {
clear();
insertText(0, backend.getString());
if (node.get().isClosed()) {
System.out.println("Closed " + node.get().sequent());
this.setBorder(new Border(new BorderStroke(Color.GREEN, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
this.getStyleClass().add("closed-sequent-view");
} else {
this.setBorder(new Border(new BorderStroke(Color.BLACK, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
this.getStyleClass().remove("closed-sequent-view");
this.getStyleClass().add("sequent-view");
}
}
......
src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java
View file @ 96b2b783
package edu.kit.formal.interpreter.graphs;
import com.google.common.eventbus.Subscribe;
import com.google.common.graph.MutableValueGraph;
import edu.kit.formal.gui.controller.Events;
import edu.kit.formal.gui.controller.PuppetMaster;
import edu.kit.formal.gui.controls.DebuggerStatusBar;
import edu.kit.formal.gui.model.Breakpoint;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.InterpretingService;
import edu.kit.formal.interpreter.data.GoalNode;
......@@ -19,6 +21,7 @@ import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.util.List;
import java.util.Set;
/**
* Class controlling and maintaining proof tree structure for debugger and handling step functions for the debugger
......@@ -138,17 +141,18 @@ public class ProofTreeController {
}
/**
* Build the control flow graph for looking up step-edges for the given script inligning called script commands
* Sets the properties that may notify GUI about statechanges with new state values
*
* @param mainScript
* @param state
*/
private void buildControlFlowGraph(ProofScript mainScript) {
this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup());
mainScript.accept(controlFlowGraphVisitor);
System.out.println("CFG\n" + controlFlowGraphVisitor.asdot());
private void setNewState(State<KeyData> state) {
setCurrentGoals(state == null ? null : state.getGoals());
setCurrentSelectedGoal(state == null ? null : state.getSelectedGoalNode());
setCurrentHighlightNode(statePointer.getScriptstmt());
LOGGER.debug("New State from this command: {}@{}",
this.statePointer.getScriptstmt().getNodeName(),
this.statePointer.getScriptstmt().getStartPosition());
}
//TODO handle endpoint
......@@ -189,7 +193,7 @@ public class ProofTreeController {
/**
* Step Back one Node in the stategraph
*
* @return
* @return PTreeNode of current pointer
*/
public PTreeNode stepBack() {
PTreeNode current = this.statePointer;
......@@ -214,6 +218,17 @@ public class ProofTreeController {
return null;
}
/**
* Execute script with breakpoints
* @param debugMode
* @param statusBar
* @param breakpoints
*/
public void executeScript(boolean debugMode, DebuggerStatusBar statusBar, Set<Breakpoint> breakpoints) {
breakpoints.forEach(breakpoint -> blocker.addBreakpoint(breakpoint.getLineNumber()));
executeScript(debugMode, statusBar);
}
/**
* Execute the script that is identified by the mainscript.
* If this method is executed with debug mode true, it executes only statements after invoking the methods stepOver() and stepInto()
......@@ -243,6 +258,7 @@ public class ProofTreeController {
this.stateGraphWrapper.install(currentInterpreter);
this.stateGraphWrapper.addChangeListener(graphChangedListener);
blocker.getStepUntilBlock().set(1);
}
......@@ -265,19 +281,22 @@ public class ProofTreeController {
}
/**
* Sets the properties that may notify GUI about statechanges with new state values
* Build the control flow graph for looking up step-edges for the given script inligning called script commands
*
* @param state
* @param mainScript
*/
private void setNewState(State<KeyData> state) {
setCurrentGoals(state==null? null : state.getGoals());
setCurrentSelectedGoal(state==null?null:state.getSelectedGoalNode());
setCurrentHighlightNode(statePointer.getScriptstmt());
LOGGER.debug("New State from this command: {}@{}",
this.statePointer.getScriptstmt().getNodeName(),
this.statePointer.getScriptstmt().getStartPosition());
private void buildControlFlowGraph(ProofScript mainScript) {
this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup());
mainScript.accept(controlFlowGraphVisitor);
System.out.println("CFG\n" + controlFlowGraphVisitor.asdot());
}
/**
* Handle the event that the script was modified
*
* @param mod
*/
@Subscribe
public void handle(Events.ScriptModificationEvent mod) {
LOGGER.debug("ProofTreeController.handleScriptModificationEvent");
......@@ -287,6 +306,24 @@ public class ProofTreeController {
this.setCurrentGoals(currentInterpreter.getCurrentGoals());
}
/**
* Save all data structures to compare before reexecution
*/
public void saveGraphs() {
MutableValueGraph stateGraph = stateGraphWrapper.getStateGraph();
MutableValueGraph ctrlFlow = controlFlowGraphVisitor.getGraph();
}
private boolean compareCtrlFlowNodes(ControlFlowNode newNode, ControlFlowNode oldNode) {
return newNode.getScriptstmt().getNodeName().equals(oldNode.getScriptstmt().getNodeName());
}
private boolean comparePTreeNodes(PTreeNode newTreeNode, PTreeNode oldTreeNode) {
return false;
}
/**************************************************************************************************************
*
......
src/main/resources/DebuggerMain.fxml
View file @ 96b2b783
......@@ -4,7 +4,6 @@
<?import de.jensd.fx.glyphs.materialdesignicons.*?>
<?import edu.kit.formal.gui.controls.DebuggerStatusBar?>
<?import javafx.scene.control.*?>
<?import javafx.scene.input.KeyCodeCombination?>
<?import javafx.scene.layout.BorderPane?>
<?import javafx.scene.layout.VBox?>
<?import org.dockfx.DockPane?>
......@@ -92,13 +91,21 @@
</MenuItem>
<MenuItem
text="Run in debug mode"
text="Execute Script Stepwise"
onAction="#executeInDebugMode"
disable="${controller.executeNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="PLAY_PAUSE" size="24.0"/>
</graphic>
</MenuItem>
<MenuItem
text="Run to Breakpoint"
onAction="#executeToBreakpoint"
disable="${controller.executeNotPossible}">
<graphic>
<MaterialDesignIconView glyphName="FAST_FORWARD" size="24.0"/>
</graphic>
</MenuItem>
</items>
</SplitMenuButton>
......
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