Skip to content

P
ProofScriptParser
Commit 54730de1 authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

Merge remote-tracking branch 'origin/master' 

# Conflicts:
#	src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
parents a37fadf5 433967fc
Hide whitespace changes
Inline Side-by-side
Showing with 478 additions and 66 deletions
pom.xml
View file @ 54730de1
......@@ -303,6 +303,20 @@
<version>0.9.2</version>
</dependency>
<dependency>
<groupId>org.apache.logging.log4j</groupId>
<artifactId>log4j-api</artifactId>
<version>2.8</version>
</dependency>
<dependency>
<groupId>org.apache.logging.log4j</groupId>
<artifactId>log4j-core</artifactId>
<version>2.8</version>
</dependency>
</dependencies>
......
src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java
View file @ 54730de1
......@@ -12,16 +12,18 @@ import javafx.fxml.FXMLLoader;
import javafx.scene.Parent;
import javafx.scene.Scene;
import javafx.stage.Stage;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.io.IOException;
import java.util.logging.Logger;
import java.util.Locale;
public class ProofScriptDebugger extends Application {
public static final String NAME = "Proof Script Debugger";
public static final String VERSION = "0.1";
public static final String KEY_VERSION = KeYConstants.VERSION;
private Logger logger = Logger.getLogger("psdbg");
private Logger logger = LogManager.getLogger("psdbg");
public static void main(String[] args) {
launch(args);
......@@ -29,11 +31,9 @@ public class ProofScriptDebugger extends Application {
@Override
public void start(Stage primaryStage) {
logger.info("Start: " + NAME);
logger.info("Version: " + VERSION);
logger.info("KeY: " + KeYConstants.COPYRIGHT);
logger.info("KeY Version: " + KeYConstants.VERSION);
logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
Locale.setDefault(Locale.ENGLISH);
try {
FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
......@@ -43,10 +43,18 @@ public class ProofScriptDebugger extends Application {
scene.getStylesheets().addAll(
getClass().getResource("debugger-ui.css").toExternalForm()
);
primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION);
primaryStage.setScene(scene);
primaryStage.show();
logger.info("Start: " + NAME);
logger.info("Version: " + VERSION);
logger.info("KeY: " + KeYConstants.COPYRIGHT);
logger.info("KeY Version: " + KeYConstants.VERSION);
logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
} catch (IOException e) {
e.printStackTrace();
}
......
src/main/java/edu/kit/formal/gui/controller/ContractChooser.java
View file @ 54730de1
......@@ -5,12 +5,22 @@ import de.uka.ilkd.key.speclang.Contract;
import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleListProperty;
import javafx.collections.ObservableList;
import javafx.event.EventHandler;
import javafx.scene.control.*;
import javafx.scene.layout.VBox;
import javafx.stage.Modality;
import lombok.Getter;
import java.awt.event.KeyEvent;
/**
* A Contract Chooser is a modal dialog, which shows a list of contracts and lets the user select one.
* <p>
* <p>
* <p>
* <p>
* WizardPane to display all available contracts
*
* @author S. Grebing
* @author A. Weigl
*/
......@@ -18,26 +28,36 @@ public class ContractChooser extends Dialog<Contract> {
@Getter
private final MultipleSelectionModel<Contract> selectionModel;
private final ObjectProperty<ObservableList<Contract>> items;
private final ListView<Contract> listOfContractsView;
private final ListView<Contract> listOfContractsView = new ListView<>();
private final Services services;
public ContractChooser(Services services) {
super();
this.services = services;
setTitle("Key Contract Chooser");
setHeaderText("Please select a contract");
this.services = services;
listOfContractsView = new ListView<>();
setResizable(true);
initModality(Modality.APPLICATION_MODAL);
selectionModel = listOfContractsView.getSelectionModel();
items = listOfContractsView.itemsProperty();
DialogPane dpane = new DialogPane();
dpane.setContent(listOfContractsView);
dpane.setPrefSize(680, 320);
setDialogPane(dpane);
listOfContractsView.setCellFactory(ContractListCell::new);
setResizable(true);
dpane.setPrefSize(680, 320);
setResultConverter((value) -> value == ButtonType.OK ? listOfContractsView.getSelectionModel().getSelectedItem() : null);
dpane.getButtonTypes().addAll(ButtonType.OK, ButtonType.CANCEL);
final Button okButton = (Button) dpane.lookupButton(ButtonType.OK);
okButton.setDefaultButton(true);
listOfContractsView.setOnKeyPressed(event -> okButton.fire());
}
public ContractChooser(Services services,
......@@ -228,10 +248,16 @@ public class ContractChooser extends Dialog<Contract> {
return;
}
VBox box = new VBox();
Label head = new Label(getItem().getDisplayName() + "\n");
head.setWrapText(true);
head.setStyle("-fx-font-weight: bold; -fx-font-size: 120%");
setGraphic(new VBox(head, new Label(getItem().getPlainText(services))));
head.getStyleClass().add("title");
Label contract = new Label(getItem().getPlainText(services));
contract.getStyleClass().add("contract");
setGraphic(
new VBox(head, contract)
);
}
}
}
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @ 54730de1
......@@ -33,6 +33,8 @@ import javafx.scene.layout.Priority;
import javafx.stage.FileChooser;
import org.antlr.v4.runtime.RecognitionException;
import org.apache.commons.io.FileUtils;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.io.File;
import java.io.IOException;
......@@ -52,9 +54,12 @@ import java.util.concurrent.Executors;
* @author Alexander Weigl
*/
public class DebuggerMainWindowController implements Initializable {
private static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class);
private final PuppetMaster blocker = new PuppetMaster();
private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
@FXML
private Pane rootPane;
@FXML
......@@ -100,12 +105,11 @@ public class DebuggerMainWindowController implements Initializable {
* references to objects needed for controlling backend through UI
*/
private RootModel model = new RootModel();
@FXML
private Label lblStatusMessage;
@FXML
private Label lblCurrentNodes;
@FXML
private Label lblFilename;
private DebuggerStatusBar statusBar;
private File initialDirectory;
@FXML
......@@ -155,18 +159,22 @@ public class DebuggerMainWindowController implements Initializable {
*/
@Override
public void initialize(URL location, ResourceBundle resources) {
setDebugMode(false);
toolbar.getChildrenUnmodifiable().forEach(
n -> n.setOnMouseEntered(statusBar.getTooltipHandler()));
buttonStartInterpreter.setOnMouseEntered(statusBar.getTooltipHandler());
model.scriptFileProperty().addListener((observable, oldValue, newValue) -> {
lblFilename.setText("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
});
model.chosenContractProperty().addListener(o -> {
IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
javaSourceCode.clear();
javaSourceCode.getMarkedLines().clear();
javaSourceCode.getLineToClass().clear();
StringWriter writer = new StringWriter();
ProgramPrinter pp = new ProgramPrinter(writer);
try {
......@@ -261,10 +269,10 @@ public class DebuggerMainWindowController implements Initializable {
private void executeScript(InterpreterBuilder ib, boolean debugMode) {
this.debugMode.set(debugMode);
blocker.deinstall();
lblStatusMessage.setText("Parse ...");
statusBar.publishMessage("Parse ...");
try {
List<ProofScript> scripts = Facade.getAST(tabPane.getActiveScriptAreaTab().getScriptArea().getText());
lblStatusMessage.setText("Creating new Interpreter instance ...");
List<ProofScript> scripts = Facade.getAST(scriptArea.getText());
statusBar.publishMessage("Creating new Interpreter instance ...");
ib.setScripts(scripts);
ib.captureHistory();
......@@ -352,7 +360,7 @@ public class DebuggerMainWindowController implements Initializable {
if (keyFile != null) {
Task<Void> task = facade.loadKeyFileTask(keyFile);
task.setOnSucceeded(event -> {
lblStatusMessage.setText("Loaded key file: " + keyFile);
statusBar.publishMessage("Loaded key file: %s", keyFile);
model.getCurrentGoalNodes().setAll(facade.getPseudoGoals());
});
......@@ -470,7 +478,7 @@ public class DebuggerMainWindowController implements Initializable {
@Override
protected void succeeded() {
lblStatusMessage.setText("Contract loaded");
statusBar.publishMessage("Contract loaded");
model.getLoadedContracts().setAll(getValue());
//FIXME model braucht contracts nicht
ContractChooser cc = new ContractChooser(facade.getService(), model.loadedContractsProperty());
......
src/main/java/edu/kit/formal/gui/controls/BaseCodeArea.java 0 → 100644
View file @ 54730de1
package edu.kit.formal.gui.controls;
import javafx.beans.property.BooleanProperty;
import javafx.beans.property.MapProperty;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleMapProperty;
import javafx.collections.FXCollections;
import javafx.collections.ObservableMap;
import org.antlr.v4.runtime.Token;
import org.fxmisc.richtext.CodeArea;
import java.util.Collections;
import java.util.Map;
/**
* A code area with support for line highlightning.
* Created by weigl on 10.06.2017.
*
* @author Alexander Weigl
*/
public class BaseCodeArea extends CodeArea {
protected MapProperty<Integer, String> lineToClass = new SimpleMapProperty<>(FXCollections.observableHashMap());
protected BooleanProperty enableLineHighlighting = new SimpleBooleanProperty();
protected BooleanProperty enableCurrentLineHighlighting = new SimpleBooleanProperty();
public BaseCodeArea() {
init();
}
public BaseCodeArea(String text) {
super(text);
init();
}
private void init() {
}
public void setText(String text) {
replaceText(text);
}
protected void highlightLines() {
if (enableLineHighlighting.get() || enableCurrentLineHighlighting.get()) {
LineMapping lm = new LineMapping(getText());
if (enableLineHighlighting.get()) {
for (Map.Entry<Integer, String> entry : lineToClass.entrySet()) {
hightlightLine(lm, entry.getKey(), entry.getValue());
}
}
if (enableCurrentLineHighlighting.get()) {
int caret = getCaretPosition();
hightlightLine(lm, lm.getLine(caret), "current-line");
}
}
}
public void jumpTo(Token token) {
//token.getStartIndex();
}
protected void hightlightLine(LineMapping lm, int line, String clazz) {
final int start = lm.getLineStart(line);
final int end = lm.getLineEnd(line);
setStyle(start, end, Collections.singleton(clazz));
}
public ObservableMap<Integer, String> getLineToClass() {
return lineToClass.get();
}
public MapProperty<Integer, String> lineToClassProperty() {
return lineToClass;
}
public void setLineToClass(ObservableMap<Integer, String> lineToClass) {
this.lineToClass.set(lineToClass);
}
public boolean isEnableLineHighlighting() {
return enableLineHighlighting.get();
}
public BooleanProperty enableLineHighlightingProperty() {
return enableLineHighlighting;
}
public void setEnableLineHighlighting(boolean enableLineHighlighting) {
this.enableLineHighlighting.set(enableLineHighlighting);
}
public boolean isEnableCurrentLineHighlighting() {
return enableCurrentLineHighlighting.get();
}
public BooleanProperty enableCurrentLineHighlightingProperty() {
return enableCurrentLineHighlighting;
}
public void setEnableCurrentLineHighlighting(boolean enableCurrentLineHighlighting) {
this.enableCurrentLineHighlighting.set(enableCurrentLineHighlighting);
}
}
src/main/java/edu/kit/formal/gui/controls/DebuggerStatusBar.java 0 → 100644
View file @ 54730de1
package edu.kit.formal.gui.controls;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import edu.kit.formal.gui.controller.DebuggerMainWindowController;
import javafx.beans.binding.StringBinding;
import javafx.beans.property.ListProperty;
import javafx.beans.property.SimpleListProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.beans.property.SimpleStringProperty;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableStringValue;
import javafx.beans.value.ObservableValue;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.scene.Node;
import javafx.scene.control.*;
import javafx.scene.input.MouseButton;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.BorderPane;
import javafx.stage.Modality;
import javafx.util.Callback;
import org.apache.logging.log4j.Level;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.apache.logging.log4j.core.Appender;
import org.apache.logging.log4j.core.Filter;
import org.apache.logging.log4j.core.Layout;
import org.apache.logging.log4j.core.LogEvent;
import org.apache.logging.log4j.core.appender.AbstractAppender;
import org.apache.logging.log4j.core.appender.ConsoleAppender;
import org.apache.logging.log4j.core.layout.PatternLayout;
import org.controlsfx.control.StatusBar;
import java.io.PrintWriter;
import java.io.Serializable;
import java.io.StringWriter;
import java.util.Date;
import java.util.LinkedList;
import java.util.logging.LogRecord;
/**
* Created by weigl on 09.06.2017.
*/
public class DebuggerStatusBar extends StatusBar {
private static final Logger LOGGER = LogManager.getLogger(DebuggerStatusBar.class);
private Label lblCurrentNodes = new Label("#nodes: %s");
private ProgressIndicator progressIndicator = new ProgressIndicator();
private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
private EventHandler<MouseEvent> toolTipHandler = event -> {
publishMessage(((Control) event.getTarget()).getTooltip().getText());
};
private final ContextMenu contextMenu = createContextMenu();
private final Dialog<Void> loggerDialog = createDialog();
public DebuggerStatusBar() {
listenOnField("psdbg");
getRightItems().addAll(
lblCurrentNodes,
progressIndicator
);
setOnMouseClicked(event -> {
if (event.getButton() == MouseButton.SECONDARY) {
contextMenu.show(this, event.getScreenX(), event.getScreenY());
}
});
}
private final Appender loggerHandler = createAppender();
private Appender createAppender() {
PatternLayout layout = PatternLayout.createDefaultLayout();
return new AbstractAppender("", null, layout) {
@Override
public void append(LogEvent event) {
publishMessage(event.getMessage().getFormattedMessage());
}
};
}
public void publishMessage(String format, Object... args) {
String msg = String.format(format, args);
setText(msg);
}
public EventHandler<MouseEvent> getTooltipHandler() {
return toolTipHandler;
}
public void listenOnField(ObservableStringValue value) {
value.addListener((observable, oldValue, newValue) -> {
publishMessage(newValue);
});
}
public void listenOnField(Logger logger) {
org.apache.logging.log4j.core.Logger plogger = ((org.apache.logging.log4j.core.Logger) logger); // Bypassing the public API
plogger.addAppender(loggerHandler);
plogger.addAppender(logCatchHandler);
logger.info("Listener added");
}
public void listenOnField(String loggerCategory) {
listenOnField(LogManager.getLogger(loggerCategory));
}
public void indicateProgress() {
progressIndicator.setProgress(-1);
}
public void stopProgress() {
progressIndicator.setProgress(100);
}
public ContextMenu createContextMenu() {
ContextMenu cm = new ContextMenu();
Menu viewOptions = new Menu("View Options");
MenuItem showLog = new MenuItem("Show Log", new MaterialDesignIconView(MaterialDesignIcon.FORMAT_LIST_BULLETED));
showLog.setOnAction(this::showLog);
cm.getItems().addAll(viewOptions, showLog);
return cm;
}
private void showLog(ActionEvent actionEvent) {
loggerDialog.show();
}
public Dialog<Void> createDialog() {
final TableView<LogEvent> recordView = new TableView<>(logCatchHandler.recordsProperty());
recordView.setEditable(false);
recordView.setSortPolicy(param -> false);
TableColumn<LogEvent, Date> dateColumn = new TableColumn<>("Date");
TableColumn<LogEvent, Level> levelColumn = new TableColumn<>("Level");
//TableColumn<LogRecord, String> classColumn = new TableColumn<>("Class");
TableColumn<LogEvent, String> messageColumn = new TableColumn<>("Message");
recordView.getColumns().setAll(dateColumn, levelColumn, messageColumn);
dateColumn.setCellValueFactory(
param -> new SimpleObjectProperty<>(new Date(param.getValue().getTimeMillis())
));
levelColumn.setCellValueFactory(
param -> new SimpleObjectProperty<>(param.getValue().getLevel())
);
messageColumn.setCellValueFactory(
param -> {
return new SimpleStringProperty(param.getValue().getMessage().getFormattedMessage());
/*String s = formatter.formatMessage(param.getValue());
if (param.getValue().getThrown() != null) {
StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw);
pw.println();
param.getValue().getThrown().printStackTrace(pw);
pw.close();
s += "\n" + sw.toString();
}
return new SimpleStringProperty(s);*/
}
);
Dialog<Void> dialog = new Dialog<>();
dialog.setResizable(true);
dialog.initModality(Modality.NONE);
dialog.setHeaderText("Logger Records");
DialogPane dpane = dialog.getDialogPane();
dpane.setContent(new BorderPane(recordView));
dpane.getButtonTypes().setAll(ButtonType.CLOSE);
return dialog;
}
public static class LogCatchHandlerFX extends AbstractAppender {
private ListProperty<LogEvent> records = new SimpleListProperty<>(FXCollections.observableList(
new LinkedList<>() //remove of head
));
private int maxRecords = 5000;
protected LogCatchHandlerFX() {
super("LogCatchHandlerFX", null, PatternLayout.createDefaultLayout());
}
@Override
public void append(LogEvent event) {
records.add(event);
while (records.size() > maxRecords)
records.remove(0);
}
public ObservableList<LogEvent> getRecords() {
return records.get();
}
public ListProperty<LogEvent> recordsProperty() {
return records;
}
public void setRecords(ObservableList<LogEvent> records) {
this.records.set(records);
}
public int getMaxRecords() {
return maxRecords;
}
public void setMaxRecords(int maxRecords) {
this.maxRecords = maxRecords;
}
}
}
src/main/java/edu/kit/formal/gui/controls/JavaArea.java
View file @ 54730de1
......@@ -16,11 +16,8 @@ import java.util.Set;
* @author Alexander Weigl
* @version 1 (03.06.17)
*/
public class JavaArea extends CodeArea {
private static final Set<String> HIGHLIGHT_LINE_CLAZZ = Collections.singleton("hl-line");
public class JavaArea extends BaseCodeArea {
private ANTLR4LexerHighlighter highlighter = new ANTLR4LexerHighlighter((s) -> new Java8Lexer(CharStreams.fromString(s)));
private SimpleSetProperty<Integer> markedLines = new SimpleSetProperty<>(this, "markedLines",
FXCollections.observableSet());
public JavaArea() {
init();
......@@ -36,36 +33,13 @@ public class JavaArea extends CodeArea {
setParagraphGraphicFactory(LineNumberFactory.get(this));
setWrapText(true);
getStyleClass().add("java-area");
//getStylesheets().add(getClass().getResource("java-keywords.css").toExternalForm());
getStyleClass().add("java-area");
textProperty().addListener(
(a, b, c) -> updateView());
markedLines.addListener((SetChangeListener<Integer>) change -> updateView());
}
private void updateView() {
clearStyle(0, getText().length());
setStyleSpans(0, highlighter.highlight(textProperty().getValue()));
LineMapping lmap = new LineMapping(textProperty().getValue());
for (Integer line : markedLines) {
int start = lmap.getLineStart(line);
int end = lmap.getLineEnd(line);
setStyle(start, end, HIGHLIGHT_LINE_CLAZZ);
}
}
public ObservableSet<Integer> getMarkedLines() {
return markedLines.get();
}
public SimpleSetProperty<Integer> markedLinesProperty() {
return markedLines;
}
public void setMarkedLines(ObservableSet<Integer> markedLines) {
this.markedLines.set(markedLines);
highlightLines();
}
}
src/main/java/edu/kit/formal/interpreter/HistoryListener.java
View file @ 54730de1
......@@ -6,6 +6,7 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
......@@ -29,5 +30,40 @@ public class HistoryListener extends DefaultASTVisitor<Void> {
return null;
}
public State getLastStateFor(ASTNode node) {
int index = queueNode.lastIndexOf(node);
if (index == -1)
return null;
return queueState.get(index);
}
public List<State> getStates(ASTNode node) {
ArrayList<State> list = new ArrayList<>(queueState.size());
for (int i = 0; i < queueNode.size(); i++) {
if (node.equals(queueNode.get(i))) {
list.add(queueState.get(i));
}
}
return list;
}
public List<State> getStates(int caret) {
ArrayList<State> list = new ArrayList<>(queueState.size());
int nearestFoundCaret = -1;
for (int i = 0; i < queueNode.size(); i++) {
int currentPos = queueNode.get(i).getRuleCtx().start.getStartIndex();
if (currentPos > nearestFoundCaret && currentPos <= caret) {
list.clear();
nearestFoundCaret = currentPos;
}
if (currentPos