Skip to content
GitLab
Commit f56281e7 authored by Alexander Weigl's avatar Alexander Weigl
Browse files

Merge branch 'master' of git.scc.kit.edu:xt9634/ProofScriptParser 

* 'master' of git.scc.kit.edu:xt9634/ProofScriptParser:
  New Script Tabs loadable and concept for loading a file again is implementend: if file is already laoded and loaded again, it is overwritten (Decision for the beginning); part for right side is coming in the next days ;-)
  New Tabs loadable and concept for loading a file again is implementend: if file is already laoded and loaded again, it is overwritten (Decision for the beginning)
  small improvements
  Better StatusBar, little refactoring in contract chooser
  Empty tab pane has buttons now, need to add the appropriate Action
  Empty TabPane (not final yet)
  Fixed issue back
  Initial Tab for scriptArea
  Added tabbedpane in fxml for scriptarea and model skelett for inspectionviewmodel
  CodeArea's syntax highlightning
  added first part of parser testcases
parents 30833094 b03739c9
Pipeline #11076 failed with stage
in 2 minutes and 21 seconds
Hide whitespace changes
Inline Side-by-side
pom.xml
View file @ f56281e7
......@@ -99,6 +99,26 @@
</configuration>
</plugin>
<plugin>
<groupId>org.lesscss</groupId>
<artifactId>lesscss-maven-plugin</artifactId>
<version>1.7.0.1.1</version>
<executions>
<execution>
<phase>generate-resources</phase>
<goals>
<goal>compile</goal>
</goals>
<configuration>
<outputDirectory>${project.build.outputDirectory}</outputDirectory>
<sourceDirectory>${project.build.sourceDirectory}/../resources</sourceDirectory>
<compress>false</compress>
</configuration>
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.antlr</groupId>
<artifactId>antlr4-maven-plugin</artifactId>
......@@ -283,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 @ f56281e7
......@@ -7,23 +7,23 @@ package edu.kit.formal.gui;
*/
import de.uka.ilkd.key.util.KeYConstants;
import edu.kit.formal.gui.controller.DebuggerMainWindowController;
import javafx.application.Application;
import javafx.fxml.FXMLLoader;
import javafx.scene.Parent;
import javafx.scene.Scene;
import javafx.scene.SceneBuilder;
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);
......@@ -31,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,11 +41,20 @@ public class ProofScriptDebugger extends Application {
//DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
Scene scene = new Scene(root);
scene.getStylesheets().addAll(
"/proofscriptdebugger.css"
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 @ f56281e7
......@@ -5,37 +5,59 @@ 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;
/**
* WozardPane to dosplay all available contracts
* 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
*/
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,
......@@ -52,14 +74,14 @@ public class ContractChooser extends Dialog<Contract> {
return items.get();
}
public ObjectProperty<ObservableList<Contract>> itemsProperty() {
return items;
}
public void setItems(ObservableList<Contract> items) {
this.items.set(items);
}
public ObjectProperty<ObservableList<Contract>> itemsProperty() {
return items;
}
private class ContractListCell extends ListCell<Contract> {
ContractListCell(ListView<Contract> contractListView) {
itemProperty().addListener((observable, oldValue, newValue) -> render());
......@@ -226,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 @ f56281e7
......@@ -4,10 +4,7 @@ import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.pp.ProgramPrinter;
import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.formal.gui.controls.GoalOptionsMenu;
import edu.kit.formal.gui.controls.JavaArea;
import edu.kit.formal.gui.controls.ScriptArea;
import edu.kit.formal.gui.controls.SequentView;
import edu.kit.formal.gui.controls.*;
import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.InterpreterBuilder;
......@@ -36,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;
......@@ -55,23 +54,26 @@ import java.util.concurrent.Executors;
* @author Alexander Weigl
*/
public class DebuggerMainWindowController implements Initializable {
private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
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
private SplitPane splitPane;
/***********************************************************************************************************
* Code Area
* **********************************************************************************************************/
//@FXML
//private ScriptArea scriptArea;
@FXML
private ScrollPane scrollPaneCode;
@FXML
private ScriptArea scriptArea;
private ScriptTabsController tabPane;
//@FXML
//private Tab startTab;
/***********************************************************************************************************
* MenuBar
* **********************************************************************************************************/
......@@ -98,21 +100,15 @@ public class DebuggerMainWindowController implements Initializable {
private ExecutorService executorService = Executors.newFixedThreadPool(2);
private KeYProofFacade facade = new KeYProofFacade();
private ContractLoaderService contractLoaderService = new ContractLoaderService();
/**
* Model for the DebuggerController containing the neccessary
* 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 final PuppetMaster blocker = new PuppetMaster();
@FXML
private DebuggerStatusBar statusBar;
private File initialDirectory;
......@@ -122,10 +118,40 @@ public class DebuggerMainWindowController implements Initializable {
@FXML
private SequentView sequentView;
private InterpretingService interpreterService = new InterpretingService();
private ObservableBooleanValue executeNotPossible = interpreterService.runningProperty().or(facade.readyToExecuteProperty().not());
public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) {
Alert alert = new Alert(Alert.AlertType.ERROR);
alert.setTitle(title);
alert.setHeaderText(headerText);
alert.setContentText(contentText);
StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw);
ex.printStackTrace(pw);
String exceptionText = sw.toString();
Label label = new Label("The exception stacktrace was:");
TextArea textArea = new TextArea(exceptionText);
textArea.setEditable(false);
textArea.setWrapText(true);
textArea.setMaxWidth(Double.MAX_VALUE);
textArea.setMaxHeight(Double.MAX_VALUE);
GridPane.setVgrow(textArea, Priority.ALWAYS);
GridPane.setHgrow(textArea, Priority.ALWAYS);
GridPane expContent = new GridPane();
expContent.setMaxWidth(Double.MAX_VALUE);
expContent.add(label, 0, 0);
expContent.add(textArea, 0, 1);
alert.getDialogPane().setExpandableContent(expContent);
alert.showAndWait();
}
/**
* @param location
......@@ -133,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 {
......@@ -157,7 +187,9 @@ public class DebuggerMainWindowController implements Initializable {
javaSourceCode.insertText(0, writer.toString());
});
scriptArea.getMarkedLines().addListener(new SetChangeListener<Integer>() {
// scriptArea.getMarkedLines().addListener(new SetChangeListener<Integer>() {
tabPane.getActiveScriptAreaTab().getScriptArea().getMarkedLines().addListener(new SetChangeListener<Integer>() {
@Override
public void onChanged(Change<? extends Integer> change) {
blocker.getBreakpoints().clear();
......@@ -185,8 +217,27 @@ public class DebuggerMainWindowController implements Initializable {
});
goalView.setCellFactory(GoalNodeListCell::new);
}
CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane);
/* startTab.textProperty().bind(new StringBinding() {
{
super.bind(model.scriptFileProperty());
}
@Override
protected String computeValue() {
if (model.scriptFileProperty().getValue() != null) {
System.out.println(model.scriptFileProperty());
return model.scriptFileProperty().get().getName();
} else {
return "Untitled";
}
}
});*/
}
//region Actions: Execution
@FXML
......@@ -203,7 +254,7 @@ public class DebuggerMainWindowController implements Initializable {
int line = lm.getLine(scriptArea.getCaretPosition());
int inLine = lm.getCharInLine(scriptArea.getCaretPosition());
*/
ib.ignoreLinesUntil(scriptArea.getCaretPosition());
ib.ignoreLinesUntil(tabPane.getActiveScriptAreaTab().getScriptArea().getCaretPosition());
executeScript(ib, true);
......@@ -213,15 +264,18 @@ public class DebuggerMainWindowController implements Initializable {
public void executeInDebugMode() {
executeScript(facade.buildInterpreter(), true);
}
//endregion
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(scriptArea.getText());
lblStatusMessage.setText("Creating new Interpreter instance ...");
List<ProofScript> scripts = Facade.getAST(tabPane.getActiveScriptAreaTab().getScriptArea().getText());
statusBar.publishMessage("Creating new Interpreter instance ...");
ib.setScripts(scripts);
ib.captureHistory();
Interpreter<KeyData> currentInterpreter = ib.build();
if (debugMode) {
......@@ -235,7 +289,6 @@ public class DebuggerMainWindowController implements Initializable {
showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
}
}
//endregion
//region Actions: Menu
@FXML
......@@ -263,7 +316,7 @@ public class DebuggerMainWindowController implements Initializable {
private void saveScript(File scriptFile) {
try {
FileUtils.write(scriptFile, scriptArea.getText(), Charset.defaultCharset());
FileUtils.write(scriptFile, tabPane.getActiveScriptAreaTab().getScriptArea().getText(), Charset.defaultCharset());
} catch (IOException e) {
showExceptionDialog("Could not save file", "blubb", "...fsfsfsf fsa", e);
}
......@@ -281,7 +334,8 @@ public class DebuggerMainWindowController implements Initializable {
assert scriptFile != null;
try {
String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset());
openScript(code);
tabPane.createNewTab(scriptFile.getAbsolutePath());
openScript(code, tabPane.getActiveScriptAreaTab().getScriptArea());
model.setScriptFile(scriptFile);
} catch (IOException e) {
showExceptionDialog("Exception occured", "",
......@@ -289,10 +343,14 @@ public class DebuggerMainWindowController implements Initializable {
}
}
private void openScript(String code) {
private void openScript(String code, ScriptArea area) {
model.setScriptFile(null);
scriptArea.clear();
scriptArea.setText(code);
if (area.textProperty().getValue() != "") {
System.out.println(area.textProperty().getValue());
area.deleteText(0, area.textProperty().getValue().length());
}
area.setText(code);
}
@FXML
......@@ -302,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());
});
......@@ -322,7 +380,9 @@ public class DebuggerMainWindowController implements Initializable {
public void saveProof(ActionEvent actionEvent) {
}
//endregion
//region Santa's Little Helper
@FXML
protected void loadJavaFile() {
......@@ -332,9 +392,6 @@ public class DebuggerMainWindowController implements Initializable {
contractLoaderService.start();
}
}
//endregion
//region Santa's Little Helper
/**
* Creates a filechooser dialog
......@@ -382,6 +439,32 @@ public class DebuggerMainWindowController implements Initializable {
goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
}
public KeYProofFacade getFacade() {
return facade;
}
//region Property
public boolean isDebugMode() {
return debugMode.get();
}
//endregion
public void setDebugMode(boolean debugMode) {
this.debugMode.set(debugMode);
}
public SimpleBooleanProperty debugModeProperty() {
return debugMode;
}
public Boolean getExecuteNotPossible() {
return executeNotPossible.get();
}
public ObservableBooleanValue executeNotPossibleProperty() {
return executeNotPossible;
}
public class ContractLoaderService extends Service<List<Contract>> {
@Override
protected Task<List<Contract>> createTask() {
......@@ -395,9 +478,9 @@ public class DebuggerMainWindowController implements Initializable {
@Override
protected void succeeded() {
lblStatusMessage.setText("Contract loaded");
statusBar.publishMessage("Contract loaded");
model.getLoadedContracts().setAll(getValue());
//FIXME
//FIXME model braucht contracts nicht
ContractChooser cc = new ContractChooser(facade.getService(), model.loadedContractsProperty());
cc.showAndWait().ifPresent(result -> {
......@@ -412,54 +495,6 @@ public class DebuggerMainWindowController implements Initializable {
}
}
public KeYProofFacade getFacade() {
return facade;
}
public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) {
Alert alert = new Alert(Alert.AlertType.ERROR);
alert.setTitle(title);
alert.setHeaderText(headerText);
alert.setContentText(contentText);
StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw);
ex.printStackTrace(pw);
String exceptionText = sw.toString();
Label label = new Label("The exception stacktrace was:");
TextArea textArea = new TextArea(exceptionText);
textArea.setEditable(false);
textArea.setWrapText(true);
textArea.setMaxWidth(Double.MAX_VALUE);
textArea.setMaxHeight(Double.MAX_VALUE);
GridPane.setVgrow(textArea, Priority.ALWAYS);
GridPane.setHgrow(textArea, Priority.ALWAYS);
GridPane expContent = new GridPane();
expContent.setMaxWidth(Double.MAX_VALUE);
expContent.add(label, 0, 0);
expContent.add(textArea, 0, 1);
alert.getDialogPane().setExpandableContent(expContent);
alert.showAndWait();
}
//endregion
//region Property
public boolean isDebugMode() {