Skip to content

P
ProofScriptParser
Commit cce67d91 authored by Alexander Weigl's avatar Alexander Weigl
Browse files
Options

Merge branch 'docking' 

* docking:
  docking framework seems good
  set to correct module
  remove submodules
  embedd a docking framework
parents 2c0303f2 ca4ce23b
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 930 additions and 527 deletions
.gitmodules
View file @ cce67d91
[submodule "doc"]
path = doc
url = git@git.scc.kit.edu:xt9634/ProofScriptParser.wiki.git
[submodule "lib/DockFX"]
path = lib/DockFX
url = https://github.com/ClearControl/DockFX.git
DockFX @ bbbc5765
Subproject commit bbbc57653d6a0bc7463539de30fec075443c0843
pom.xml
View file @ cce67d91
......@@ -72,6 +72,49 @@
</pluginManagement>
<plugins>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>build-helper-maven-plugin</artifactId>
<version>1.7</version>
<executions>
<execution>
<id>released-version</id>
<goals>
<goal>released-version</goal>
</goals>
</execution>
<execution>
<id>add-source</id>
<phase>generate-sources</phase>
<goals>
<goal>add-source</goal>
</goals>
<configuration>
<sources>
<source>lib/DockFX/src/main/java</source>
</sources>
</configuration>
</execution>
<execution>
<id>add-resource</id>
<phase>generate-resources</phase>
<goals>
<goal>add-resource</goal>
</goals>
<configuration>
<resources>
<resource>
<directory>lib/DockFX/src/main/resources</directory>
</resource>
</resources>
</configuration>
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>jaxb2-maven-plugin</artifactId>
......
src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java
View file @ cce67d91
......@@ -14,6 +14,7 @@ import javafx.scene.Scene;
import javafx.stage.Stage;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.dockfx.DockNode;
import java.io.IOException;
import java.util.Locale;
......@@ -33,15 +34,14 @@ public class ProofScriptDebugger extends Application {
public void start(Stage primaryStage) {
Locale.setDefault(Locale.ENGLISH);
try {
FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
Parent root = fxmlLoader.load();
//DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
Scene scene = new Scene(root);
scene.getStylesheets().addAll(
getClass().getResource("debugger-ui.css").toExternalForm()
getClass().getResource("debugger-ui.css").toExternalForm(),
DockNode.class.getResource("default.css").toExternalForm()
);
primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION);
primaryStage.setScene(scene);
......
src/main/java/edu/kit/formal/gui/controls/InspectionViewTab.java
View file @ cce67d91
package edu.kit.formal.gui.controls;
import com.sun.org.apache.xpath.internal.operations.Mod;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.pp.ProgramPrinter;
import edu.kit.formal.gui.model.InspectionModel;
import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import javafx.beans.Observable;
import javafx.beans.property.BooleanProperty;
import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.ReadOnlyObjectProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.fxml.FXML;
import javafx.scene.Node;
import javafx.scene.control.ListCell;
import javafx.scene.control.ListView;
import javafx.scene.control.SplitPane;
import javafx.scene.control.Tab;
import javafx.scene.input.MouseEvent;
import java.io.IOException;
import java.io.StringWriter;
import javafx.scene.layout.BorderPane;
/**
* Right part of the splitpane that displays the different parts of a state
*
* @author S. Grebing
*/
public class InspectionViewTab extends Tab {
public class InspectionViewTab extends BorderPane {
public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
@FXML
private SectionPane sectionPaneJavaCode;
@FXML
private SplitPane lowerSplitPane;
@FXML
private SequentView sequentView;
@FXML
private JavaArea javaSourceCode;
@FXML
private ListView goalView;
private ObjectProperty<Mode> mode = new SimpleObjectProperty<>();
@FXML
private ListView<GoalNode<KeyData>> goalView;
private BooleanProperty showCode = new SimpleBooleanProperty(true);
private ObjectProperty<InspectionModel> model = new SimpleObjectProperty<>(
new InspectionModel()
);
public InspectionViewTab() {
super();
Utils.createWithFXML(this);
getGoalView().getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> {
if (newValue != null && newValue.getData() != null) {
getSequentView().setNode(newValue.getData().getNode());
}
});
model.get().selectedGoalNodeToShowProperty().bind(
goalView.getSelectionModel().selectedItemProperty()
);
model.get().selectedGoalNodeToShowProperty().addListener(
(observable, oldValue, newValue) -> {
goalView.getSelectionModel().select(newValue);
if (newValue != null && newValue.getData() != null) {
getSequentView().setNode(newValue.getData().getNode());
// TODO weigl: get marked lines of the program, and set it
model.get().highlightedJavaLinesProperty().get()
.clear();
}
});
model.get().goalsProperty().bindBidirectional(goalView.itemsProperty());
getGoalView().setCellFactory(GoalNodeListCell::new);
/*TODO redefine CSS bases on selected mode
mode.addListener(o -> {
getStyleClass().removeAll(
Mode.DEAD.name(),
......@@ -65,34 +67,14 @@ public class InspectionViewTab extends Tab {
Mode.POSTMORTEM.name()
);
getStyleClass().add(mode.get().name());
if (mode.get() == Mode.LIVING) {
MaterialDesignIconView icon = new MaterialDesignIconView(MaterialDesignIcon.RUN);
setClosable(false);
setGraphic(icon);
} else {
setGraphic(null);
setClosable(true);
}
});
showCode.addListener(o -> {
if (showCode.get())
lowerSplitPane.getItems().add(sectionPaneJavaCode);
else
lowerSplitPane.getItems().remove(sectionPaneJavaCode);
});
showCode.set(false);
*/
}
public SequentView getSequentView() {
return sequentView;
}
public JavaArea getJavaSourceCode() {
return javaSourceCode;
}
public ListView<GoalNode<KeyData>> getGoalView() {
return goalView;
......@@ -107,16 +89,8 @@ public class InspectionViewTab extends Tab {
goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
}
public void initialize(InspectionModel model) {
System.out.println("model");
}
public void refresh(RootModel model) {
IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
getJavaSourceCode().clear();
getJavaSourceCode().getLineToClass().clear();
//javaSourceCode.clear();
//javaSourceCode.getLineToClass().clear();
/* IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
StringWriter writer = new StringWriter();
ProgramPrinter pp = new ProgramPrinter(writer);
try {
......@@ -126,39 +100,10 @@ public class InspectionViewTab extends Tab {
} catch (IOException e) {
e.printStackTrace();
}
getJavaSourceCode().insertText(0, writer.toString());
// javaSourceCode.insertText(0, writer.toString());
*/
}
public Mode getMode() {
return mode.get();
}
public void setMode(Mode mode) {
this.mode.set(mode);
}
public ObjectProperty<Mode> modeProperty() {
return mode;
}
public boolean isShowCode() {
return showCode.get();
}
public void setShowCode(boolean showCode) {
this.showCode.set(showCode);
}
public BooleanProperty showCodeProperty() {
return showCode;
}
enum Mode {
LIVING, DEAD, POSTMORTEM,
}
/**
* Cells for GoalView
*/
......@@ -182,4 +127,12 @@ public class InspectionViewTab extends Tab {
setText(text);
}
}
public InspectionModel getModel() {
return model.get();
}
public ReadOnlyObjectProperty<InspectionModel> modelProperty() {
return model;
}
}
src/main/java/edu/kit/formal/gui/controls/InspectionViewsController.java 0 → 100644
View file @ cce67d91
package edu.kit.formal.gui.controls;
import edu.kit.formal.gui.model.RootModel;
import javafx.beans.property.SimpleMapProperty;
import javafx.collections.FXCollections;
import javafx.collections.ObservableMap;
import org.dockfx.DockNode;
/**
* TabPane on the right side of the GUI containing the inspection view as tabs
*/
public class InspectionViewsController {
/**
* active tab in which the interpreter resp. Debugger state is shown.
* This tab can be changed and later on in this tab it should be possible to select proof commands
* All other tabs are only post morten tabs which cannot be shown
*/
private final InspectionViewTab activeInterpreterTab = new InspectionViewTab();
private final DockNode activeInterpreterTabDock = new DockNode(activeInterpreterTab, "Active");
private final ObservableMap<InspectionViewTab, DockNode> inspectionViews = new SimpleMapProperty<>(FXCollections.observableHashMap());
public InspectionViewTab getActiveInspectionViewTab() {
return this.activeInterpreterTab;
}
public DockNode getActiveInterpreterTabDock() {
return activeInterpreterTabDock;
}
public void connectActiveView(RootModel model) {
getActiveInspectionViewTab().getGoalView().itemsProperty().bind(model.currentGoalNodesProperty());
model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> {
getActiveInspectionViewTab().getGoalView().getSelectionModel().select(fresh);
});
}
}
src/main/java/edu/kit/formal/gui/controls/ScriptArea.java
View file @ cce67d91
......@@ -9,11 +9,13 @@ import edu.kit.formal.proofscriptparser.ScriptLanguageLexer;
import edu.kit.formal.proofscriptparser.ast.ProofScript;
import edu.kit.formal.proofscriptparser.lint.LintProblem;
import edu.kit.formal.proofscriptparser.lint.LinterStrategy;
import javafx.beans.InvalidationListener;
import javafx.beans.Observable;
import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.*;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.collections.ObservableSet;
import javafx.event.ActionEvent;
import javafx.fxml.FXML;
import javafx.geometry.Insets;
......@@ -27,6 +29,8 @@ import javafx.scene.paint.Color;
import javafx.scene.paint.Paint;
import javafx.scene.text.Font;
import javafx.scene.text.FontPosture;
import lombok.Data;
import lombok.RequiredArgsConstructor;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.Token;
......@@ -52,13 +56,16 @@ import java.util.function.IntFunction;
*/
public class ScriptArea extends CodeArea {
private final ObjectProperty<File> filePath = new SimpleObjectProperty<>();
private final BooleanProperty dirty = new SimpleBooleanProperty(this, "dirty", false);
/**
* Lines to highlight?
*/
private final SetProperty<Integer> markedLines =
private final SetProperty<RegionStyle> markedRegions =
new SimpleSetProperty<>(FXCollections.observableSet());
/**
* set by {@link ScriptTabPane}
* set by {@link ScriptController}
*/
private final ObjectProperty<MainScriptIdentifier> mainScript = new SimpleObjectProperty<>();
......@@ -82,15 +89,13 @@ public class ScriptArea extends CodeArea {
//getStylesheets().add(getClass().getResource("script-keywords.css").toExternalForm());
getStyleClass().add("script-area");
textProperty().addListener((prop, oldValue, newValue) -> {
if (newValue.length() != 0) {
clearStyle(0, newValue.length());
StyleSpans<? extends Collection<String>> spans = highlighter.highlight(newValue);
if (spans != null) setStyleSpans(0, spans);
}
dirty.set(true);
updateMainScriptMarker();
updateHighlight();
highlightProblems();
updateMainScriptMarker();
});
markedRegions.addListener((InvalidationListener) o -> updateHighlight());
/* .successionEnds(Duration.ofMillis(100))
.hook(collectionRichTextChange -> this.getUndoManager().mark())
.supplyTask(this::computeHighlightingAsync).awaitLatest(richChanges())
......@@ -121,6 +126,19 @@ public class ScriptArea extends CodeArea {
contextMenu = new ScriptAreaContextMenu();
}
private void updateHighlight() {
String newValue = getText();
if (newValue.length() != 0) {
clearStyle(0, newValue.length());
StyleSpans<? extends Collection<String>> spans = highlighter.highlight(newValue);
if (spans != null) setStyleSpans(0, spans);
}
markedRegions.forEach(reg -> {
setStyle(reg.start, reg.stop, Collections.singleton(reg.clazzName));
});
}
private void updateMainScriptMarker() {
try {
MainScriptIdentifier ms = mainScript.get();
......@@ -211,52 +229,6 @@ public class ScriptArea extends CodeArea {
a.setBreakpoint(!a.isBreakpoint());
}
/**
* Highlight line given by the characterindex
*
* @param lineNumber
*/
public void highlightStmt(int lineNumber, String cssStyleTag) {
//calculate line number from characterindex
//int lineNumber = this.offsetToPosition(chrIdx, Bias.Forward).getMajor();
Paragraph<Collection<String>, StyledText<Collection<String>>, Collection<String>> paragraph = this.getParagraph(lineNumber);
//calculate start and endposition
//int startPos = getAbsolutePosition(this.offsetToPosition(chrIdx, Bias.Forward).getMajor(), 0);
int startPos = getAbsolutePosition(lineNumber, 0);
int length = paragraph.length();
//highlight line
this.setStyle(startPos, startPos + length, Collections.singleton(cssStyleTag));
}
/**
* Remove the highlighting of a statement
*
* @param lineNumber
*/
public void removeHighlightStmt(int lineNumber) {
highlightStmt(lineNumber, "line-unhighlight");
}
/**
* Set a mark in the gutter next to the definition of the main script
*
* @param lineNumberOfSigMainScript
*/
public void setDebugMark(int lineNumberOfSigMainScript) {
highlightStmt(lineNumberOfSigMainScript - 1, "line-highlight-mainScript");
}
public void removeDebugHighlight() {
// removeHighlightStmt(this.getMainScript().getLineNumber());
}
public void unsetDebugMark(int lineNumberOfSigMainScript) {
removeHighlightStmt(lineNumberOfSigMainScript - 1);
}
public File getFilePath() {
return filePath.get();
}
......@@ -316,7 +288,6 @@ public class ScriptArea extends CodeArea {
d.show((Node) event.getTarget(), event.getScreenX(), event.getScreenY());
}
private static class GutterView extends HBox {
private final SimpleObjectProperty<GutterAnnotation> annotation = new SimpleObjectProperty<>();
......@@ -562,12 +533,45 @@ public class ScriptArea extends CodeArea {
}
public void showPostMortem(ActionEvent event) {
ScriptArea area = ScriptArea.this;
//TODO forward to ProofTreeController, it jumps to the node and this should be done via the callbacks.
/*ScriptArea area = ScriptArea.this;
int chrIdx = currentMouseOver.get().getCharacterIndex().orElse(0);
if (chrIdx != 0) {
int lineNumber = area.offsetToPosition(chrIdx, Bias.Forward).getMajor();
area.highlightStmt(lineNumber, "line-highlight-postmortem");
}
}*/
}
}
}
\ No newline at end of file
}
public ObservableSet<RegionStyle> getMarkedRegions() {
return markedRegions.get();
}
public SetProperty<RegionStyle> markedRegionsProperty() {
return markedRegions;
}
public void setMarkedRegions(ObservableSet<RegionStyle> markedRegions) {
this.markedRegions.set(markedRegions);
}
public boolean isDirty() {
return dirty.get();
}
public BooleanProperty dirtyProperty() {
return dirty;
}
public void setDirty(boolean dirty) {
this.dirty.set(dirty);
}
@RequiredArgsConstructor
@Data
public static class RegionStyle {
public final int start, stop;
public final String clazzName;
}
}
src/main/java/edu/kit/formal/gui/controls/ScriptTabPane.java deleted 100644 → 0
View file @ 2c0303f2
package edu.kit.formal.gui.controls;
import edu.kit.formal.gui.model.Breakpoint;
import edu.kit.formal.gui.model.MainScriptIdentifier;
import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.scene.control.Tab;
import javafx.scene.control.TabPane;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.io.File;
import java.util.HashSet;
import java.util.Set;
/**
* Controller for TabPane
*
* @author Sarah Grebing
*/
public class ScriptTabPane extends TabPane {
private static Logger logger = LogManager.getLogger(ScriptTabPane.class);
private ObjectProperty<MainScriptIdentifier> mainScript = new SimpleObjectProperty<>();
public ScriptTabPane() {
Utils.createWithFXML(this);
}
/**
* Create a new tab with the specified title
*
* @param
*/
public ScriptArea createNewTab(String filePath) {
return createNewTab(new File(filePath));
}
public ScriptArea createNewTab(File filePath) {
filePath = filePath.getAbsoluteFile();
if (findTabForFile(filePath) == null) {
Tab newTab = new Tab(filePath.getName());
ScriptArea area = new ScriptArea();
newTab.setContent(area);
area.mainScriptProperty().bindBidirectional(mainScript);
area.setFilePath(filePath);
this.getTabs().add(newTab);
return area;
} else {
logger.info("File already exists. Will not load it again");
return findScriptAreaForFile(filePath);
}
}
public Set<Breakpoint> getBreakpoints() {
HashSet<Breakpoint> breakpoints = new HashSet<>();
getTabs().forEach(tab ->
breakpoints.addAll(((ScriptArea) tab.getContent()).getBreakpoints())
);
return breakpoints;
}
public ScriptArea findScriptAreaForFile(File filePath) {
Tab t = findTabForFile(filePath);
if (t == null) return null;
return ((ScriptArea) t.getContent());
}
public Tab findTabForFile(File filePath) {
return getTabs().stream()
.filter(tab -> {
File path = ((ScriptArea) tab.getContent()).getFilePath();
return filePath.equals(path);
})
.findAny()
.orElse(null);
}
public ScriptArea getSelectedScriptArea() {
return (ScriptArea) getSelectionModel().getSelectedItem().getContent();
}
}
src/main/java/edu/kit/formal/gui/controls/WelcomePane.java 0 → 100644
View file @ cce67d91
package edu.kit.formal.gui.controls;
import edu.kit.formal.gui.controller.DebuggerMainWindowController;
import javafx.scene.layout.AnchorPane;
import java.awt.event.ActionEvent;
import java.io.File;
/**
* Created by weigl on 7/7/17.
*/
public class WelcomePane extends AnchorPane {
private final DebuggerMainWindowController proofScriptDebugger;
public WelcomePane(DebuggerMainWindowController debugger) {
this.proofScriptDebugger = debugger;
Utils.createWithFXML(this);
}
public void loadContraPosition(javafx.event.ActionEvent event) {
proofScriptDebugger.getWelcomePaneDock().close();
proofScriptDebugger.showActiveInspector(null);
proofScriptDebugger.openScript(
new File("src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps")
);
proofScriptDebugger.openKeyFile(
new File("src/test/resources/edu/kit/formal/interpreter/contraposition/contraposition.key"));
}
}
src/main/java/edu/kit/formal/gui/model/InspectionModel.java
View file @ cce67d91
package edu.kit.formal.gui.model;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.proofscriptparser.ast.ASTNode;
import javafx.beans.property.SimpleListProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.beans.property.*;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.collections.ObservableMap;
import javafx.collections.ObservableSet;
import javafx.scene.paint.Color;
import java.util.Map;
import java.util.Set;
/**
* Model for the inspection view
*
* @author S.Grebing
* @author Alexander Weigl
*/
public class InspectionModel {
enum Mode {
LIVING, DEAD, POSTMORTEM,
}
private ASTNode node;
private SimpleListProperty<GoalNode> currentGoals;
private SimpleObjectProperty<GoalNode> selectedGoalNodeToShow;
private Map<GoalNode, Color> colorofEachGoalNodeinListView;
private boolean showJavaView;
private String javaString;
private Set<Integer> highlightedJavaLines;
private boolean closable;
private boolean isInterpreterTab;
private final ObjectProperty<ASTNode> node = new SimpleObjectProperty<>();
private final ListProperty<GoalNode<KeyData>> goals = new SimpleListProperty<>();
private final ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShow = new SimpleObjectProperty<>();
private final MapProperty<GoalNode, Color> colorofEachGoalNodeinListView = new SimpleMapProperty<>(FXCollections.observableHashMap());
//private final StringProperty javaString = new SimpleStringProperty();
private final SetProperty<Integer> highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet());
private final BooleanProperty closable = new SimpleBooleanProperty();
private final BooleanProperty isInterpreterTab = new SimpleBooleanProperty();
private ObjectProperty<Mode> mode = new SimpleObjectProperty<>();
public InspectionModel() {
public ASTNode getNode() {
return node.get();
}
/***************************************************************************************************************
* Getter and Setter
*
***************************************************************************************************************/
public ASTNode getNode() {
public ObjectProperty<ASTNode> nodeProperty() {
return node;
}
public void setNode(ASTNode node) {
this.node = node;
this.node.set(node);
}