From 30714eeed8f6ec3f331d93533e2352573b4a081e Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 9 Jul 2017 01:48:41 +0200 Subject: [PATCH] A lot of simplifications --- .../kit/formal/gui/ProofScriptDebugger.java | 8 +- .../gui/controller/ContractChooser.java | 6 + .../DebuggerMainWindowController.java | 385 ++++++++++-------- .../formal/gui/controller/ListGoalView.java | 66 --- ...ectionViewTab.java => InspectionView.java} | 21 +- .../controls/InspectionViewsController.java | 28 +- .../kit/formal/gui/controls/ScriptArea.java | 50 ++- .../formal/gui/controls/ScriptController.java | 131 ++---- .../edu/kit/formal/gui/controls/Utils.java | 168 ++++++++ .../kit/formal/gui/controls/WelcomePane.java | 15 +- .../kit/formal/gui/model/InspectionModel.java | 27 ++ .../edu/kit/formal/gui/model/RootModel.java | 152 ------- .../interpreter/InterpretingService.java | 4 +- .../graphs/ProofTreeController.java | 11 +- ...ectionViewTab.fxml => InspectionView.fxml} | 0 .../gui/controls/InspectionViewTabPane.fxml | 2 +- .../kit/formal/gui/controls/WelcomePane.fxml | 74 ++-- .../edu/kit/formal/gui/debugger-ui.less | 9 + src/main/resources/log4j2.properties | 32 +- 19 files changed, 601 insertions(+), 588 deletions(-) delete mode 100644 src/main/java/edu/kit/formal/gui/controller/ListGoalView.java rename src/main/java/edu/kit/formal/gui/controls/{InspectionViewTab.java => InspectionView.java} (85%) delete mode 100644 src/main/java/edu/kit/formal/gui/model/RootModel.java rename src/main/resources/edu/kit/formal/gui/controls/{InspectionViewTab.fxml => InspectionView.fxml} (100%) diff --git a/src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java b/src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java index 29b963a8..ca8f618d 100644 --- a/src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java +++ b/src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java @@ -8,6 +8,7 @@ package edu.kit.formal.gui; import de.uka.ilkd.key.util.KeYConstants; import javafx.application.Application; +import javafx.application.Platform; import javafx.fxml.FXMLLoader; import javafx.scene.Parent; import javafx.scene.Scene; @@ -39,6 +40,7 @@ public class ProofScriptDebugger extends Application { Parent root = fxmlLoader.load(); //DebuggerMainWindowController controller = fxmlLoader.getController(); Scene scene = new Scene(root); + primaryStage.setOnCloseRequest(event -> Platform.exit()); scene.getStylesheets().addAll( getClass().getResource("debugger-ui.css").toExternalForm(), DockNode.class.getResource("default.css").toExternalForm() @@ -55,10 +57,14 @@ public class ProofScriptDebugger extends Application { logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION); //logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj")); + } catch (IOException e) { e.printStackTrace(); } + } - + @Override + public void stop() throws Exception { + System.exit(0);//needed, else non-termination of process } } diff --git a/src/main/java/edu/kit/formal/gui/controller/ContractChooser.java b/src/main/java/edu/kit/formal/gui/controller/ContractChooser.java index 4f2135ca..961185b9 100644 --- a/src/main/java/edu/kit/formal/gui/controller/ContractChooser.java +++ b/src/main/java/edu/kit/formal/gui/controller/ContractChooser.java @@ -12,6 +12,7 @@ import javafx.stage.Modality; import lombok.Getter; import java.awt.event.KeyEvent; +import java.util.List; /** * A Contract Chooser is a modal dialog, which shows a list of contracts and lets the user select one. @@ -66,6 +67,11 @@ public class ContractChooser extends Dialog { listOfContractsView.itemsProperty().bind(contracts); } + public ContractChooser(Services service, List contracts) { + this(service); + listOfContractsView.itemsProperty().get().setAll(contracts); + } + public MultipleSelectionModel getSelectionModel() { return selectionModel; } diff --git a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java index 70fa62ba..2c4fa63e 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -5,7 +5,7 @@ import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.speclang.Contract; import edu.kit.formal.gui.controls.*; -import edu.kit.formal.gui.model.RootModel; +import edu.kit.formal.gui.model.InspectionModel; import edu.kit.formal.interpreter.Interpreter; import edu.kit.formal.interpreter.InterpreterBuilder; import edu.kit.formal.interpreter.KeYProofFacade; @@ -13,18 +13,16 @@ import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.graphs.PTreeNode; import edu.kit.formal.interpreter.graphs.ProofTreeController; import edu.kit.formal.proofscriptparser.ast.ProofScript; -import javafx.beans.property.SimpleBooleanProperty; +import javafx.beans.property.*; +import javafx.beans.value.ChangeListener; import javafx.beans.value.ObservableBooleanValue; +import javafx.beans.value.ObservableValue; import javafx.concurrent.Service; import javafx.concurrent.Task; import javafx.event.ActionEvent; import javafx.fxml.FXML; import javafx.fxml.Initializable; -import javafx.scene.control.*; -import javafx.scene.image.Image; -import javafx.scene.layout.GridPane; -import javafx.scene.layout.Pane; -import javafx.scene.layout.Priority; +import javafx.scene.control.ProgressBar; import javafx.stage.FileChooser; import org.antlr.v4.runtime.RecognitionException; import org.apache.commons.io.FileUtils; @@ -33,12 +31,9 @@ import org.apache.logging.log4j.Logger; import org.dockfx.DockNode; import org.dockfx.DockPane; import org.dockfx.DockPos; -import org.dockfx.demo.DockFX; import java.io.File; import java.io.IOException; -import java.io.PrintWriter; -import java.io.StringWriter; import java.net.URL; import java.nio.charset.Charset; import java.util.List; @@ -53,146 +48,130 @@ import java.util.concurrent.Executors; * @author Alexander Weigl */ public class DebuggerMainWindowController implements Initializable { - private static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class); - - private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false); - - - @FXML - private Pane rootPane; - - @FXML - private DockPane dockStation; + protected static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class); private ScriptController scriptController; + private final ProofTreeController proofTreeController = new ProofTreeController(); + private final InspectionViewsController inspectionViewsController = new InspectionViewsController(); + private final ExecutorService executorService = Executors.newFixedThreadPool(2); + private final KeYProofFacade facade = new KeYProofFacade(); + private final ContractLoaderService contractLoaderService = new ContractLoaderService(); - /*********************************************************************************************************** - * MenuBar - * **********************************************************************************************************/ @FXML - private MenuBar menubar; - @FXML - private Menu fileMenu; - @FXML - private MenuItem closeMenuItem; - /*********************************************************************************************************** - * ToolBar - * **********************************************************************************************************/ - @FXML - private ToolBar toolbar; - @FXML - private SplitMenuButton buttonStartInterpreter; + private DebuggerStatusBar statusBar; @FXML - private Button startDebugMode; - /*********************************************************************************************************** - * GoalView - * **********************************************************************************************************/ - - private final InspectionViewsController inspectionViewsController = new InspectionViewsController(); - - /** - * - */ + private DockPane dockStation; private JavaArea javaArea = new JavaArea(); private DockNode javaAreaDock = new DockNode(javaArea, "Java Source", new MaterialDesignIconView(MaterialDesignIcon.CODEPEN) ); + private WelcomePane welcomePane = new WelcomePane(this); + private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT)); + private DockNode activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock(); - 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 + * Property: current loaded javaFile */ - private RootModel model = new RootModel(); - - - @FXML - private DebuggerStatusBar statusBar; - - private File initialDirectory; - + private final ObjectProperty javaFile = new SimpleObjectProperty<>(this, "javaFile"); /** - * Controller for debugging functions + * Property: current loaded KeY File */ - private ProofTreeController pc = new ProofTreeController(); - - //TODO - private ObservableBooleanValue executeNotPossible = pc.executeNotPossibleProperty().or(facade.readyToExecuteProperty().not()); + private final ObjectProperty keyFile = new SimpleObjectProperty<>(this, "keyFile"); - private WelcomePane welcomePane = new WelcomePane(this); - private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT)); - private DockNode activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock(); + /** + * Chosen contract for problem + */ + private final ObjectProperty chosenContract = new SimpleObjectProperty<>(this, "chosenContract"); + private BooleanProperty debugMode = new SimpleBooleanProperty(this, "debugMode", false); - 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(); + /** + * True, iff the execution is not possible + */ + private ObservableBooleanValue executeNotPossible = proofTreeController.executeNotPossibleProperty().or(facade.readyToExecuteProperty().not()); - Label label = new Label("The exception stacktrace was:"); - TextArea textArea = new TextArea(exceptionText); - textArea.setEditable(false); - textArea.setWrapText(true); + /** + * + */ + private ObjectProperty initialDirectory = new SimpleObjectProperty<>(this, "initialDirectory"); - textArea.setMaxWidth(Double.MAX_VALUE); - textArea.setMaxHeight(Double.MAX_VALUE); - GridPane.setVgrow(textArea, Priority.ALWAYS); - GridPane.setHgrow(textArea, Priority.ALWAYS); + /** + * + */ + private StringProperty javaCode = new SimpleStringProperty(this, "javaCode"); - 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 - * @param resources - */ @Override public void initialize(URL location, ResourceBundle resources) { setDebugMode(false); scriptController = new ScriptController(dockStation); - Image dockImage = new Image(DockFX.class.getResource("docknode.png").toExternalForm()); + //register the welcome dock in the center welcomePaneDock.dock(dockStation, DockPos.LEFT); + registerToolbarToStatusBar(); + marriageProofTreeControllerWithActiveInspectionView(); + //statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a")); - /* - toolbar.getChildrenUnmodifiable().forEach( - n -> n.setOnMouseEntered(statusBar.getTooltipHandler())); + javaCode.addListener(new ChangeListener() { + @Override + public void changed(ObservableValue observable, String oldValue, String newValue) { + try { + javaArea.setText(newValue); + } catch (Exception e) { + LOGGER.catching(e); + } + } + }); - buttonStartInterpreter.setOnMouseEntered(statusBar.getTooltipHandler()); - */ + //Debugging + Utils.addDebugListener(javaCode); + Utils.addDebugListener(executeNotPossible, "executeNotPossible"); + + } - model.scriptFileProperty().addListener((observable, oldValue, newValue) -> { - statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a")); + /** + * Connects the proof tree controller with the model of the active inspection view model. + */ + private void marriageProofTreeControllerWithActiveInspectionView() { + InspectionModel imodel = getInspectionViewsController().getActiveInspectionViewTab().getModel(); + + //set all listeners + proofTreeController.currentGoalsProperty().addListener((o, old, fresh) -> { + if (fresh != null) { + imodel.setGoals(fresh); + } }); - /** - * create a new inspectionviewtab that is the main tab and not closable - */ - inspectionViewsController.connectActiveView(model); + proofTreeController.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> { + if (newValue != null) { + imodel.setCurrentInterpreterGoal(newValue); + } + }); - /*pc.goalsProperty().addListener((o, old, fresh) -> { - model.currentGoalNodesProperty().setAll(fresh); + proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> { + scriptController.getDebugPositionHighlighter().highlight(newValue); }); - model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty());*/ - //model.currentGoalNodesProperty().bind(pc.goalsProperty()); - //CustomTabPaneSkin skin = new CustomTabPaneSkin(scriptController); + Utils.addDebugListener(proofTreeController.currentGoalsProperty()); + Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty()); + Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty()); + } + + /** + * If the mouse moves other toolbar button, the help text should display in the status bar + */ + private void registerToolbarToStatusBar() { + /*toolbar.getChildrenUnmodifiable().forEach( + n -> n.setOnMouseEntered(statusBar.getTooltipHandler())); + + buttonStartInterpreter.setOnMouseEntered(statusBar.getTooltipHandler()); + */ } //region Actions: Execution @@ -233,33 +212,15 @@ public class DebuggerMainWindowController implements Initializable { List scripts = scriptController.getCombinedAST(); statusBar.publishMessage("Creating new Interpreter instance ..."); ib.setScripts(scripts); - Interpreter currentInterpreter = ib.build(); - pc.setCurrentInterpreter(currentInterpreter); - pc.setMainScript(scripts.get(0)); - - pc.executeScript(this.debugMode.get()); - //set all listeners - pc.currentGoalsProperty().addListener((o, old, fresh) -> { - if (fresh != null) { - model.setCurrentGoalNodes(fresh); - // model.currentGoalNodesProperty().setAll(fresh); - } - }); - pc.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> { - if (newValue != null) { - model.setCurrentSelectedGoalNode(newValue); - } - }); - - pc.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> { - scriptController.getDebugPositionHighlighter().highlight(newValue); - }); + proofTreeController.setCurrentInterpreter(currentInterpreter); + proofTreeController.setMainScript(scripts.get(0)); + proofTreeController.executeScript(this.debugMode.get()); //highlight signature of main script //scriptController.setDebugMark(scripts.get(0).getStartPosition().getLineNumber()); } catch (RecognitionException e) { - showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); + Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); } } @@ -270,7 +231,7 @@ public class DebuggerMainWindowController implements Initializable { } @FXML - protected void openScript() { + public void openScript() { File scriptFile = openFileChooserOpenDialog("Select Script File", "Proof Script File", "kps"); if (scriptFile != null) { @@ -280,18 +241,14 @@ public class DebuggerMainWindowController implements Initializable { @FXML public void saveScript() { - if (model.getScriptFile() != null) { - saveScript(model.getScriptFile()); - } else { - saveAsScript(); - } + scriptController.saveCurrentScript(); } private void saveScript(File scriptFile) { try { scriptController.saveCurrentScriptAs(scriptFile); } catch (IOException e) { - showExceptionDialog("Could not save sourceName", "blubb", "...fsfsfsf fsa", e); + Utils.showExceptionDialog("Could not save sourceName", "blubb", "...fsfsfsf fsa", e); } } @@ -305,26 +262,16 @@ public class DebuggerMainWindowController implements Initializable { public void openScript(File scriptFile) { assert scriptFile != null; + setInitialDirectory(scriptFile.getParentFile() ); try { String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset()); ScriptArea area = scriptController.createNewTab(scriptFile); - openScript(code, area); - model.setScriptFile(scriptFile); } catch (IOException e) { - showExceptionDialog("Exception occured", "", + Utils.showExceptionDialog("Exception occured", "", "Could not load sourceName " + scriptFile, e); } } - public void openScript(String code, ScriptArea area) { - model.setScriptFile(null); - if (!area.textProperty().getValue().isEmpty()) { - area.deleteText(0, area.textProperty().getValue().length()); - } - area.setText(code); - - } - @FXML protected void loadKeYFile() { File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "script"); @@ -333,16 +280,17 @@ public class DebuggerMainWindowController implements Initializable { public void openKeyFile(File keyFile) { if (keyFile != null) { - this.model.setKeYFile(keyFile); + setKeyFile(keyFile); + setInitialDirectory(keyFile.getParentFile()); Task task = facade.loadKeyFileTask(keyFile); task.setOnSucceeded(event -> { statusBar.publishMessage("Loaded key sourceName: %s", keyFile); - model.getCurrentGoalNodes().setAll(facade.getPseudoGoals()); + getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(facade.getPseudoGoals()); }); task.setOnFailed(event -> { event.getSource().exceptionProperty().get(); - showExceptionDialog("Could not load sourceName", "Key sourceName loading error", "", + Utils.showExceptionDialog("Could not load sourceName", "Key sourceName loading error", "", (Throwable) event.getSource().exceptionProperty().get() ); }); @@ -354,7 +302,7 @@ public class DebuggerMainWindowController implements Initializable { } public void saveProof(ActionEvent actionEvent) { - + LOGGER.error("saveProof not implemented!!!"); } //endregion @@ -368,7 +316,8 @@ public class DebuggerMainWindowController implements Initializable { public void openJavaFile(File javaFile) { if (javaFile != null) { - model.setJavaFile(javaFile); + setJavaFile(javaFile); + initialDirectory.set(javaFile.getParentFile()); contractLoaderService.start(); } } @@ -385,7 +334,7 @@ public class DebuggerMainWindowController implements Initializable { FileChooser fileChooser = getFileChooser(title, description, fileEndings); // File sourceName = fileChooser.showSaveDialog(inspectionViewsController.getInspectionViewTab().getGoalView().getScene().getWindow()); File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow()); - if (file != null) initialDirectory = file.getParentFile(); + if (file != null) setInitialDirectory(file.getParentFile()); return file; } @@ -393,7 +342,7 @@ public class DebuggerMainWindowController implements Initializable { FileChooser fileChooser = getFileChooser(title, description, fileEndings); //File sourceName = fileChooser.showOpenDialog(inspectionViewsController.getInspectionViewTab().getGoalView().getScene().getWindow()); File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow()); - if (file != null) initialDirectory = file.getParentFile(); + if (file != null) setInitialDirectory(file.getParentFile()); return file; } @@ -401,23 +350,24 @@ public class DebuggerMainWindowController implements Initializable { FileChooser fileChooser = new FileChooser(); fileChooser.setTitle(title); fileChooser.setSelectedExtensionFilter(new FileChooser.ExtensionFilter(description, fileEndings)); - if (initialDirectory == null) - initialDirectory = new File("src/test/resources/edu/kit/formal/interpreter/contraposition/"); + if (initialDirectory.get() == null) + setInitialDirectory(new File("src/test/resources/edu/kit/formal/interpreter/contraposition/")); - if (!initialDirectory.exists()) - initialDirectory = new File("."); + if (!initialDirectory.get().exists()) + setInitialDirectory(new File(".")); - fileChooser.setInitialDirectory(initialDirectory); + fileChooser.setInitialDirectory(initialDirectory.get()); return fileChooser; } public void stepOver(ActionEvent actionEvent) { - PTreeNode newState = pc.stepOver(); + LOGGER.debug("DebuggerMainWindowController.stepOver"); + PTreeNode newState = proofTreeController.stepOver(); } public void stepBack(ActionEvent actionEvent) { - - PTreeNode newState = pc.stepBack(); + LOGGER.debug("DebuggerMainWindowController.stepBack"); + PTreeNode newState = proofTreeController.stepBack(); } @@ -435,7 +385,7 @@ public class DebuggerMainWindowController implements Initializable { this.debugMode.set(debugMode); } - public SimpleBooleanProperty debugModeProperty() { + public BooleanProperty debugModeProperty() { return debugMode; } @@ -493,33 +443,116 @@ public class DebuggerMainWindowController implements Initializable { public class ContractLoaderService extends Service> { @Override protected Task> createTask() { - return facade.getContractsForJavaFileTask(model.getJavaFile()); + return facade.getContractsForJavaFileTask(getJavaFile()); } @Override protected void failed() { - showExceptionDialog("", "", "", exceptionProperty().get()); + Utils.showExceptionDialog("", "", "", exceptionProperty().get()); } @Override protected void succeeded() { statusBar.publishMessage("Contract loaded"); - model.getLoadedContracts().setAll(getValue()); - //FIXME model braucht contracts nicht - ContractChooser cc = new ContractChooser(facade.getService(), model.loadedContractsProperty()); + List contracts = getValue(); + ContractChooser cc = new ContractChooser(facade.getService(), contracts); cc.showAndWait().ifPresent(result -> { - model.setChosenContract(result); + setChosenContract(result); try { facade.activateContract(result); - model.getCurrentGoalNodes().setAll(facade.getPseudoGoals()); + getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(facade.getPseudoGoals()); } catch (ProofInputException e) { - showExceptionDialog("", "", "", e); + Utils.showExceptionDialog("", "", "", e); } }); } } + public ScriptController getScriptController() { + return scriptController; + } + + public ProofTreeController getProofTreeController() { + return proofTreeController; + } + + public InspectionViewsController getInspectionViewsController() { + return inspectionViewsController; + } + + public ExecutorService getExecutorService() { + return executorService; + } + + public ContractLoaderService getContractLoaderService() { + return contractLoaderService; + } + + public DebuggerStatusBar getStatusBar() { + return statusBar; + } + + public DockPane getDockStation() { + return dockStation; + } + + public JavaArea getJavaArea() { + return javaArea; + } + + public WelcomePane getWelcomePane() { + return welcomePane; + } + + public File getJavaFile() { + return javaFile.get(); + } + + public ObjectProperty javaFileProperty() { + return javaFile; + } + + public File getKeyFile() { + return keyFile.get(); + } + + public ObjectProperty keyFileProperty() { + return keyFile; + } + + public Contract getChosenContract() { + return chosenContract.get(); + } + + public ObjectProperty chosenContractProperty() { + return chosenContract; + } + + public void setJavaFile(File javaFile) { + this.javaFile.set(javaFile); + } + + public void setKeyFile(File keyFile) { + this.keyFile.set(keyFile); + } + + public void setChosenContract(Contract chosenContract) { + this.chosenContract.set(chosenContract); + } + + public File getInitialDirectory() { + return initialDirectory.get(); + } + + public ObjectProperty initialDirectoryProperty() { + return initialDirectory; + } + + public void setInitialDirectory(File initialDirectory) { + this.initialDirectory.set(initialDirectory); + } + //endregion } diff --git a/src/main/java/edu/kit/formal/gui/controller/ListGoalView.java b/src/main/java/edu/kit/formal/gui/controller/ListGoalView.java deleted file mode 100644 index b77bd0ef..00000000 --- a/src/main/java/edu/kit/formal/gui/controller/ListGoalView.java +++ /dev/null @@ -1,66 +0,0 @@ -package edu.kit.formal.gui.controller; - -import edu.kit.formal.gui.controls.Utils; -import edu.kit.formal.gui.model.RootModel; -import edu.kit.formal.interpreter.data.GoalNode; -import edu.kit.formal.interpreter.data.KeyData; -import javafx.beans.property.SimpleListProperty; -import javafx.fxml.FXML; -import javafx.fxml.FXMLLoader; -import javafx.scene.control.ListCell; -import javafx.scene.control.ListView; -import javafx.scene.control.TextArea; -import javafx.scene.layout.VBox; - -import java.io.IOException; - -/** - * Created by sarah on 5/27/17. - */ -public class ListGoalView extends VBox { - protected SimpleListProperty> localGoalListProperty = new SimpleListProperty<>(); - @FXML - private ListView> listOfGoalsView; - @FXML - private TextArea goalNodeView; - - private RootModel rootModel; - - public ListGoalView() { - Utils.createWithFXML(this); - listOfGoalsView.setCellFactory(list -> new GoalNodeCell()); - } - - - public void setRootModel(RootModel rootModel) { - this.rootModel = rootModel; - } - - /** - * Set Bindings and listener - */ - /* public void init() { - listOfGoalsView.itemsProperty().bind(this.rootModel.currentGoalNodesProperty()); - - listOfGoalsView.getSelectionModel().selectedItemProperty().addListener(new ChangeListener>() { - @Override - public void changed(ObservableValue> observable, GoalNode oldValue, GoalNode newValue) { - goalNodeView.setText(newValue.toCellTextForKeYData()); - } - }); - - } -*/ - - private static class GoalNodeCell extends ListCell> { - - @Override - protected void updateItem(GoalNode item, boolean empty) { - super.updateItem(item, empty); - if (item != null) { - setText(item.toListLabelForKeYData()); - } - } - - } -} diff --git a/src/main/java/edu/kit/formal/gui/controls/InspectionViewTab.java b/src/main/java/edu/kit/formal/gui/controls/InspectionView.java similarity index 85% rename from src/main/java/edu/kit/formal/gui/controls/InspectionViewTab.java rename to src/main/java/edu/kit/formal/gui/controls/InspectionView.java index 12d38664..de90cc2b 100644 --- a/src/main/java/edu/kit/formal/gui/controls/InspectionViewTab.java +++ b/src/main/java/edu/kit/formal/gui/controls/InspectionView.java @@ -1,7 +1,6 @@ package edu.kit.formal.gui.controls; 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; @@ -20,7 +19,7 @@ import javafx.scene.layout.BorderPane; * * @author S. Grebing */ -public class InspectionViewTab extends BorderPane { +public class InspectionView extends BorderPane { public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu(); @FXML @@ -33,8 +32,7 @@ public class InspectionViewTab extends BorderPane { new InspectionModel() ); - public InspectionViewTab() { - super(); + public InspectionView() { Utils.createWithFXML(this); model.get().selectedGoalNodeToShowProperty().bind( @@ -85,21 +83,6 @@ public class InspectionViewTab extends BorderPane { goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY()); } - public void refresh(RootModel model) { - /* IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget(); - StringWriter writer = new StringWriter(); - ProgramPrinter pp = new ProgramPrinter(writer); - try { - pp.printFullMethodSignature(method); - pp.printStatementBlock(method.getBody()); - writer.flush(); - } catch (IOException e) { - e.printStackTrace(); - } - */ - - } - /** * Cells for GoalView */ diff --git a/src/main/java/edu/kit/formal/gui/controls/InspectionViewsController.java b/src/main/java/edu/kit/formal/gui/controls/InspectionViewsController.java index 693d965b..3c143c11 100644 --- a/src/main/java/edu/kit/formal/gui/controls/InspectionViewsController.java +++ b/src/main/java/edu/kit/formal/gui/controls/InspectionViewsController.java @@ -1,13 +1,17 @@ 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 + * This controller manages a list of {@link InspectionView} and the associated {@link DockNode}s. + * + * Espeically, this class holds the active tab, which is connected with the {@link edu.kit.formal.interpreter.graphs.ProofTreeController}, + * and shows the current interpreter state. + * + * @author weigl */ public class InspectionViewsController { @@ -16,23 +20,31 @@ public class InspectionViewsController { * 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 InspectionView activeInterpreterTab = new InspectionView(); private final DockNode activeInterpreterTabDock = new DockNode(activeInterpreterTab, "Active"); + private final ObservableMap inspectionViews = new SimpleMapProperty<>(FXCollections.observableHashMap()); - private final ObservableMap inspectionViews = new SimpleMapProperty<>(FXCollections.observableHashMap()); - - public InspectionViewTab getActiveInspectionViewTab() { + public InspectionView getActiveInspectionViewTab() { return this.activeInterpreterTab; } + public DockNode getActiveInterpreterTabDock() { return activeInterpreterTabDock; } - public void connectActiveView(RootModel model) { + + public DockNode newPostMortemInspector() { + InspectionView iv = new InspectionView(); + DockNode dn = new DockNode(iv, "post mortem: "); + inspectionViews.put(iv, dn); + return dn; + } + + /*public void connectActiveView(DebuggerModel model) { getActiveInspectionViewTab().getGoalView().itemsProperty().bind(model.currentGoalNodesProperty()); model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> { getActiveInspectionViewTab().getGoalView().getSelectionModel().select(fresh); }); - } + }*/ } diff --git a/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java b/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java index d4c54445..1b28c060 100644 --- a/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java +++ b/src/main/java/edu/kit/formal/gui/controls/ScriptArea.java @@ -34,6 +34,8 @@ import lombok.RequiredArgsConstructor; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.Token; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; import org.controlsfx.control.PopOver; import org.fxmisc.richtext.CharacterHit; import org.fxmisc.richtext.CodeArea; @@ -49,19 +51,26 @@ import java.util.*; import java.util.function.IntFunction; /** - * ScriptArea is the textarea on the left side of the GUI. + * ScriptArea is the {@link CodeArea} for writing Proof Scripts. + *

* It displays the script code and allows highlighting of lines and setting of breakpoints */ public class ScriptArea extends CodeArea { - private final ObjectProperty filePath = new SimpleObjectProperty<>(); + private static final Logger LOGGER = LogManager.getLogger(ScriptArea.class); + /** + * Underlying filepath, should not be null + */ + private final ObjectProperty filePath = new SimpleObjectProperty<>(new File(Utils.getRandomName())); + /** + * If true, the content was changed since last save. + */ private final BooleanProperty dirty = new SimpleBooleanProperty(this, "dirty", false); /** - * Lines to highlight? + * CSS classes for regions, used for "manually" highlightning. e.g. debugging marker */ - private final SetProperty markedRegions = - new SimpleSetProperty<>(FXCollections.observableSet()); + private final SetProperty markedRegions = new SimpleSetProperty<>(FXCollections.observableSet()); /** * set by {@link ScriptController} */ @@ -71,7 +80,7 @@ public class ScriptArea extends CodeArea { private ANTLR4LexerHighlighter highlighter; private ListProperty problems = new SimpleListProperty<>(FXCollections.observableArrayList()); private SimpleObjectProperty currentMouseOver = new SimpleObjectProperty<>(); - private ScriptAreaContextMenu contextMenu; + private ScriptAreaContextMenu contextMenu = new ScriptAreaContextMenu(); public ScriptArea() { @@ -84,8 +93,11 @@ public class ScriptArea extends CodeArea { highlighter = new ANTLR4LexerHighlighter( (String val) -> new ScriptLanguageLexer(CharStreams.fromString(val))); this.setParagraphGraphicFactory(gutter); - //getStylesheets().add(getClass().getResource("script-keywords.css").toExternalForm()); getStyleClass().add("script-area"); + installPopup(); + + setOnMouseClicked(this::showContextMenu); + textProperty().addListener((prop, oldValue, newValue) -> { dirty.set(true); updateMainScriptMarker(); @@ -105,8 +117,6 @@ public class ScriptArea extends CodeArea { return Optional.empty(); } }).subscribe(s -> setStyleSpans(0, s));*/ - getStyleClass().add("script-area"); - installPopup(); this.addEventHandler(MouseEvent.MOUSE_PRESSED, (MouseEvent e) -> { @@ -118,10 +128,20 @@ public class ScriptArea extends CodeArea { this.moveTo(characterPosition, NavigationActions.SelectionPolicy.CLEAR); }); - mainScript.addListener((observable) -> - updateMainScriptMarker()); + mainScript.addListener((observable) -> updateMainScriptMarker()); + } + + 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 { - contextMenu = new ScriptAreaContextMenu(); + } } private void updateHighlight() { @@ -517,7 +537,7 @@ public class ScriptArea extends CodeArea { } public void setMainScript(ActionEvent event) { - System.out.println("ScriptAreaContextMenu.setMainScript"); + LOGGER.debug("ScriptAreaContextMenu.setMainScript"); List ast = Facade.getAST(getText()); int pos = currentMouseOver.get().getInsertionIndex(); ast.stream().filter(ps -> @@ -531,6 +551,10 @@ public class ScriptArea extends CodeArea { } public void showPostMortem(ActionEvent event) { + LOGGER.debug("ScriptAreaContextMenu.showPostMortem " + event); + + + //TODO forward to ProofTreeController, it jumps to the node and this should be done via the callbacks. /*ScriptArea area = ScriptArea.this; diff --git a/src/main/java/edu/kit/formal/gui/controls/ScriptController.java b/src/main/java/edu/kit/formal/gui/controls/ScriptController.java index afbf3eda..3f70bc7d 100644 --- a/src/main/java/edu/kit/formal/gui/controls/ScriptController.java +++ b/src/main/java/edu/kit/formal/gui/controls/ScriptController.java @@ -13,6 +13,8 @@ import javafx.beans.value.ChangeListener; import javafx.beans.value.ObservableValue; import javafx.collections.FXCollections; import javafx.collections.ObservableMap; +import org.antlr.v4.runtime.CharStream; +import org.antlr.v4.runtime.CharStreams; import org.apache.commons.io.FileUtils; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -34,8 +36,8 @@ public class ScriptController { public static final String LINE_HIGHLIGHT_POSTMORTEM = "line-highlight-postmortem"; private static Logger logger = LogManager.getLogger(ScriptController.class); private final DockPane parent; - private ObjectProperty mainScript = new SimpleObjectProperty<>(); private final ObservableMap openScripts = FXCollections.observableMap(new HashMap<>()); + private ObjectProperty mainScript = new SimpleObjectProperty<>(); private ScriptArea lastScriptArea; private ASTNodeHighlighter postMortemHighlighter = new ASTNodeHighlighter(LINE_HIGHLIGHT_POSTMORTEM); @@ -59,7 +61,7 @@ public class ScriptController { return openScripts.get(editor); } - public ScriptArea createNewTab(File filePath) { + public ScriptArea createNewTab(File filePath) throws IOException { filePath = filePath.getAbsoluteFile(); if (findEditor(filePath) == null) { ScriptArea area = new ScriptArea(); @@ -67,6 +69,16 @@ public class ScriptController { area.setFilePath(filePath); DockNode dockNode = createDockNode(area); openScripts.put(area, dockNode); + + if (filePath.exists()) { + String code = FileUtils.readFileToString(filePath, "utf-8"); + if (!area.textProperty().getValue().isEmpty()) { + area.deleteText(0, area.textProperty().getValue().length()); + } + area.setText(code); + } + + return area; } else { logger.info("File already exists. Will not load it again"); @@ -90,7 +102,7 @@ public class ScriptController { area.dirtyProperty().addListener(new ChangeListener() { @Override public void changed(ObservableValue observable, Boolean oldValue, Boolean newValue) { - if(newValue) + if (newValue) dockNode.setGraphic(new MaterialDesignIconView(MaterialDesignIcon.FILE_DOCUMENT)); else dockNode.setGraphic(new MaterialDesignIconView(MaterialDesignIcon.FILE_DOCUMENT_BOX)); @@ -107,7 +119,6 @@ public class ScriptController { return dockNode; } - public Set getBreakpoints() { HashSet breakpoints = new HashSet<>(); openScripts.keySet().forEach(tab -> @@ -125,7 +136,6 @@ public class ScriptController { .orElse(null); } - public void saveCurrentScriptAs(File scriptFile) throws IOException { for (ScriptArea area : openScripts.keySet()) { if (area.isFocused()) { @@ -139,101 +149,16 @@ public class ScriptController { public List getCombinedAST() { ArrayList all = new ArrayList<>(); for (ScriptArea area : openScripts.keySet()) { - all.addAll(Facade.getAST(area.getText())); + //absolute path important to find area later by token + CharStream stream = CharStreams.fromString(area.getText(), area.getFilePath().getAbsolutePath()); + all.addAll(Facade.getAST(stream)); } return all; } - private String[] ADJECTIVES = - ("abandoned,able,absolute,adorable,adventurous,academic,acceptable,acclaimed,accomplished,accurate,aching,acidic,acrobatic,active,actual,adept,admirable,admired," + - "adolescent,adorable,adored,advanced,afraid,affectionate,aged,aggravating,aggressive,agile,agitated,agonizing,agreeable,ajar,alarmed,alarming,alert," + - "alienated,alive,all,altruistic,amazing,ambitious,ample,amused,amusing,anchored,ancient,angelic,angry,anguished,animated,annual,another,antique,anxious," + - "any,apprehensive,appropriate,apt,arctic,arid,aromatic,artistic,ashamed,assured,astonishing,athletic,attached,attentive,attractive,austere,authentic,authorized," + - "automatic,avaricious,average,aware,awesome,awful,awkward,babyish,bad,back,baggy,bare,barren,basic,beautiful,belated,beloved,beneficial,better,best,bewitched," + - "big,big-hearted,biodegradable,bite-sized,bitter,black,black-and-white,bland,blank,blaring,bleak,blind,blissful,blond,blue,blushing,bogus,boiling,bold,bony," + - "boring,bossy,both,bouncy,bountiful,bowed,brave,breakable,brief,bright,brilliant,brisk,broken,bronze,brown,bruised,bubbly,bulky,bumpy,buoyant,burdensome,burly," + - "bustling,busy,buttery,buzzing,calculating,calm,candid,canine,capital,carefree,careful,careless,caring,cautious,cavernous,celebrated,charming,cheap,cheerful," + - "cheery,chief,chilly,chubby,circular,classic,clean,clear,clear-cut,clever,close,closed,cloudy,clueless,clumsy,cluttered,coarse,cold,colorful,colorless," + - "colossal,comfortable,common,compassionate,competent,complete,complex,complicated,composed,concerned,concrete,confused,conscious,considerate,constant,content," + - "conventional,cooked,cool,cooperative,coordinated,corny,corrupt,costly,courageous,courteous,crafty,crazy,creamy,creative,creepy,criminal,crisp,critical," + - "crooked,crowded,cruel,crushing,cuddly,cultivated,cultured,cumbersome,curly,curvy,cute,cylindrical,damaged,damp,dangerous,dapper,daring,darling,dark,dazzling" + - ",dead,deadly,deafening,dear,dearest,decent,decimal,decisive,deep,defenseless,defensive,defiant,deficient,definite,definitive,delayed,delectable,delicious," + - "delightful,delirious,demanding,dense,dental,dependable,dependent,descriptive,deserted,detailed,determined,devoted,different,difficult,digital,diligent,dim," + - "dimpled,dimwitted,direct,disastrous,discrete,disfigured,disgusting,disloyal,dismal,distant,downright,dreary,dirty,disguised,dishonest,dismal,distant,distinct," + - "distorted,dizzy,dopey,doting,double,downright,drab,drafty,dramatic,dreary,droopy,dry,dual,dull,dutiful,each,eager,earnest,early,easy,easy-going,ecstatic,edible" + - ",educated,elaborate,elastic,elated,elderly,electric,elegant,elementary,elliptical,embarrassed,embellished,eminent,emotional,empty,enchanted,enchanting,energetic," + - "enlightened,enormous,enraged,entire,envious,equal,equatorial,essential,esteemed,ethical,euphoric,even,evergreen,everlasting,every,evil,exalted,excellent,exemplary" + - ",exhausted,excitable,excited,exciting,exotic,expensive,experienced,expert,extraneous,extroverted,extra-large,extra-small,fabulous,failing,faint,fair,faithful,fake" + - ",false,familiar,famous,fancy,fantastic,far,faraway,far-flung,far-off,fast,fat,fatal,fatherly,favorable,favorite,fearful,fearless,feisty,feline,female,feminine,few," + - "fickle,filthy,fine,finished,firm,first,firsthand,fitting,fixed,flaky,flamboyant,flashy,flat,flawed,flawless,flickering,flimsy,flippant,flowery,fluffy,fluid," + - "flustered,focused,fond,foolhardy,foolish,forceful,forked,formal,forsaken,forthright,fortunate,fragrant,frail,frank,frayed,free,French,fresh,frequent,friendly," + - "frightened,frightening,frigid,frilly,frizzy,frivolous,front,frosty,frozen,frugal,fruitful,full,fumbling,functional,funny,fussy,fuzzy,gargantuan,gaseous,general" + - ",generous,gentle,genuine,giant,giddy,gigantic,gifted,giving,glamorous,glaring,glass,gleaming,gleeful,glistening,glittering,gloomy,glorious,glossy,glum,golden," + - "good,good-natured,gorgeous,graceful,gracious,grand,grandiose,granular,grateful,grave,gray,great,greedy,green,gregarious,grim,grimy,gripping,grizzled,gross" + - ",grotesque,grouchy,grounded,growing,growling,grown,grubby,gruesome,grumpy,guilty,gullible,gummy,hairy,half,handmade,handsome,handy,happy,happy-go-lucky,hard," + - "harmful,harmless,harmonious,harsh,hasty,hateful,haunting,healthy,heartfelt,hearty,heavenly,heavy,hefty,helpful,helpless,hidden,hideous,high,high-level,hilarious," + - "hoarse,hollow,homely,honest,honorable,honored,hopeful,horrible,hospitable,hot,huge,humble,humiliating,humming,humongous,hungry,hurtful,husky,icky,icy,ideal," + - "idealistic,identical,idle,idiotic,idolized,ignorant,ill,illegal,ill-fated,ill-informed,illiterate,illustrious,imaginary,imaginative,immaculate,immaterial,immediate" + - ",immense,impassioned,impeccable,impartial,imperfect,imperturbable,impish,impolite,important,impossible,impractical,impressionable,impressive,improbable,impure" + - ",inborn,incomparable,incompatible,incomplete,inconsequential,incredible,indelible,inexperienced,indolent,infamous,infantile,infatuated,inferior,infinite,informal" + - ",innocent,insecure,insidious,insignificant,insistent,instructive,insubstantial,intelligent,intent,intentional,interesting,internal,international,intrepid,ironclad" + - ",irresponsible,irritating,itchy,jaded,jagged,jam-packed,jaunty,jealous,jittery,joint,jolly,jovial,joyful,joyous,jubilant,judicious,juicy,jumbo,junior,jumpy,juvenile," + - "kaleidoscopic,keen,key,kind,kindhearted,kindly,klutzy,knobby,knotty,knowledgeable,knowing,known,kooky,kosher,lame,lanky,large,last,lasting,late,lavish,lawful,lazy,leading," + - "lean,leafy,left,legal,legitimate,light,lighthearted,likable,likely,limited,limp,limping,linear,lined,liquid,little,live,lively,livid,loathsome,lone,lonely,long," + - "loose,lopsided,lost,loud,lovable,lovely,loving,low,loyal,lucky,lumbering,luminous,lumpy,lustrous,luxurious,mad,made-up,magnificent,majestic,major,male,mammoth,married," + - "marvelous,masculine,massive,mature,meager,mealy,mean,measly,meaty,medical,mediocre,medium,meek,mellow,melodic,memorable,menacing,merry,messy,metallic,mild,milky,mindless," + - "miniature,minor,minty,miserable,miserly,misguided,misty,mixed,modern,modest,moist,monstrous,monthly,monumental,moral,mortified,motherly,motionless,mountainous,muddy,muffled," + - "multicolored,mundane,murky,mushy,musty,muted,mysterious,naive,narrow,nasty,natural,naughty,nautical,near,neat,necessary,needy,negative,neglected,negligible,neighboring," + - "nervous,new,next,nice,nifty,nimble,nippy,nocturnal,noisy,nonstop,normal,notable,noted,noteworthy,novel,noxious,numb,nutritious,nutty,obedient,obese,oblong,oily,oblong," + - "obvious,occasional,odd,oddball,offbeat,offensive,official,old,old-fashioned,only,open,optimal,optimistic,opulent,orange,orderly,organic,ornate,ornery,ordinary,original,other," + - "our,outlying,outgoing,outlandish,outrageous,outstanding,oval,overcooked,overdue,overjoyed,overlooked,palatable,pale,paltry,parallel,parched,partial,passionate,past,pastel," + - "peaceful,peppery,perfect,perfumed,periodic,perky,personal,pertinent,pesky,pessimistic,petty,phony,physical,piercing,pink,pitiful,plain,plaintive,plastic,playful,pleasant," + - "pleased,pleasing,plump,plush,polished,polite,political,pointed,pointless,poised,poor,popular,portly,posh,positive,possible,potable,powerful,powerless,practical,precious," + - "present,prestigious,pretty,precious,previous,pricey,prickly,primary,prime,pristine,private,prize,probable,productive,profitable,profuse,proper,proud,prudent,punctual,pungent," + - "puny,pure,purple,pushy,putrid,puzzled,puzzling,quaint,qualified,quarrelsome,quarterly,queasy,querulous,questionable,quick,quick-witted,quiet,quintessential,quirky,quixotic," + - "quizzical,radiant,ragged,rapid,rare,rash,raw,recent,reckless,rectangular,ready,real,realistic,reasonable,red,reflecting,regal,regular,reliable,relieved,remarkable,remorseful," + - "remote,repentant,required,respectful,responsible,repulsive,revolving,rewarding,rich,rigid,right,ringed,ripe,roasted,robust,rosy,rotating,rotten,rough,round,rowdy,royal,rubbery," + - "rundown,ruddy,rude,runny,rural,rusty,sad,safe,salty,same,sandy,sane,sarcastic,sardonic,satisfied,scaly,scarce,scared,scary,scented,scholarly,scientific,scornful,scratchy,scrawny," + - "second,secondary,second-hand,secret,self-assured,self-reliant,selfish,sentimental,separate,serene,serious,serpentine,several,severe,shabby,shadowy,shady,shallow,shameful,shameless," + - "sharp,shimmering,shiny,shocked,shocking,shoddy,short,short-term,showy,shrill,shy,sick,silent,silky,silly,silver,similar,simple,simplistic,sinful,single,sizzling,skeletal,skinny," + - "sleepy,slight,slim,slimy,slippery,slow,slushy,small,smart,smoggy,smooth,smug,snappy,snarling,sneaky,sniveling,snoopy,sociable,soft,soggy,solid,somber,some,spherical,sophisticated" + - ",sore,sorrowful,soulful,soupy,sour,Spanish,sparkling,sparse,specific,spectacular,speedy,spicy,spiffy,spirited,spiteful,splendid,spotless,spotted,spry,square,squeaky," + - "squiggly,stable,staid,stained,stale,standard,starchy,stark,starry,steep,sticky,stiff,stimulating,stingy,stormy,straight,strange,steel,strict,strident,striking,striped,strong," + - "studious,stunning,stupendous,stupid,sturdy,stylish,subdued,submissive,substantial,subtle,suburban,sudden,sugary,sunny,super,superb,superficial,superior,supportive,sure-footed" + - ",surprised,suspicious,svelte,sweaty,sweet,sweltering,swift,sympathetic,tall,talkative,tame,tan,tangible,tart,tasty,tattered,taut,tedious,teeming,tempting,tender,tense,tepid," + - "terrible,terrific,testy,thankful,that,these,thick,thin,third,thirsty,this,thorough,thorny,those,thoughtful,threadbare,thrifty,thunderous,tidy,tight,timely,tinted,tiny,tired,torn" + - ",total,tough,traumatic,treasured,tremendous,tragic,trained,tremendous,triangular,tricky,trifling,trim,trivial,troubled,true,trusting,trustworthy,trusty,truthful,tubby,turbulent" + - ",twin,ugly,ultimate,unacceptable,unaware,uncomfortable,uncommon,unconscious,understated,unequaled,uneven,unfinished,unfit,unfolded,unfortunate,unhappy,unhealthy,uniform," + - "unimportant,unique,united,unkempt,unknown,unlawful,unlined,unlucky,unnatural,unpleasant,unrealistic,unripe,unruly,unselfish,unsightly,unsteady,unsung,untidy,untimely,untried," + - "untrue,unused,unusual,unwelcome,unwieldy,unwilling,unwitting,unwritten,upbeat,upright,upset,urban,usable,used,useful,useless,utilized,utter,vacant,vague,vain,valid,valuable," + - "vapid,variable,vast,velvety,venerated,vengeful,verifiable,vibrant,vicious,victorious,vigilant,vigorous,villainous,violet,violent,virtual,virtuous,visible,vital,vivacious,vivid," + - "voluminous,wan,warlike,warm,warmhearted,warped,wary,wasteful,watchful,waterlogged,watery,wavy,wealthy,weak,weary,webbed,wee,weekly,weepy,weighty,weird,welcome,well-documented" + - ",well-groomed,well-informed,well-lit,well-made,well-off,well-to-do,well-worn,wet,which,whimsical,whirlwind,whispered,white,whole,whopping,wicked,wide,wide-eyed,wiggly,wild," + - "willing,wilted,winding,windy,winged,wiry,wise,witty,wobbly,woeful,wonderful,wooden,woozy,wordy,worldly,worn,worried,worrisome," + - "worse,worst,worthless,worthwhile,worthy,wrathful,wretched,writhing,wrong,wry,yawning,yearly,yellow,yellowish,young,youthful,yummy,zany,zealous,zesty,zigzag").split(","); - - private String[] ANIMALS = - ("Cat,Caterpillar,Cattle,Chamois,Cheetah,Chicken,Chimpanzee,Chinchilla,Chough,Coati,Cobra,Cockroach,Cod,Cormorant," + - "Coyote,Crab,Crane,Crocodile,Crow,Curlew,Deer,Dinosaur,,Dog,,Dogfish,Shark,Dolphin,Donkey," + - "Dotterel,Dove,Dragonfly,Duck,,Mallard,Dugong,Dunlin,Eagle,Echidna,Eel,Eland,Elephant,Elephant,seal,Elk," + - "Emu,Falcon,Ferret,Finch,Fish,,Flamingo,Fly,Fox,Frog,Gaur,Gazelle,Gerbil,Giant,panda,Giraffe,Gnat,Gnu,Goat" + - ",Goldfinch,Goosander,Goose,Gorilla,Goshawk,Grasshopper,Grouse,Guanaco,Guinea,fowl,Guinea,pig,Gull,Hamster,Hare,Hawk,Hedgehog," + - "Heron,Herring,Hippo,Hornet,Horse,,Hummingbird,Hyena,Ibex,Ibis,Jackal,Jaguar,Jay,Jellyfish,Kangaroo,Kinkajou,Koala,Komodo,dragon," + - "Kouprey,Kudu,Lapwing,Lark,Lemur,Leopard,Lion,Llama,Lobster,Locust,,Loris,Louse,Lyrebird,Magpie,Mallard,Duck,Mammoth,Manatee,Mandrill,Mink," + - "Mole,Mongoose,Monkey,Moose,Mouse,Mosquito,Narwhal,Newt,Nightingale,Octopus,Okapi,Opossum,Ostrich,Otter,Owl,Oyster,Panther,Parrot,Panda," + - "Partridge,Peafowl,Pelican,Penguin,Pheasant,Pig,Boar,Pigeon,,Polarbear,Horse,Porcupine,Porpoise,Prairie dog," + - "Quail,Quelea,Quetzal,Rabbit,,Raccoon,Ram,Sheep,Rat,,Raven,Red,deer,Red,panda,Reindeer,(caribou),Rhinoceros,Rook,Salamander,Salmon,Sandpiper," + - "Sardine,Sea,lion,Sea,urchin,Seahorse,Seal,Shark,Sheep,,Ram,Shrew,Skunk,Sloth,Snail,Snake,,Spider,,Squirrel,Starling,Stegosaurus,Swan,Tapir," + - "Tarsier,Termite,Tiger,Toad,Turkey,,Turtle,Vicuña,Wallaby,Walrus,Wasp,Water,buffalo,Weasel,Whale,Wolf,Wolverine,Wombat,Wren,Yak,Zebra").split(","); - - public String getRandomName() { - Random r = new Random(); - return (ADJECTIVES[r.nextInt(ADJECTIVES.length)] + "_" + ANIMALS[r.nextInt(ANIMALS.length)] + ".kps").toLowerCase(); - } - public ScriptArea newScript() { ScriptArea area = new ScriptArea(); - area.setFilePath(new File(getRandomName())); + area.setFilePath(new File(Utils.getRandomName())); openScripts.put(area, createDockNode(area)); return area; } @@ -242,6 +167,15 @@ public class ScriptController { return postMortemHighlighter; } + public void saveCurrentScript() { + //TODO + } + + private ScriptArea findEditor(ASTNode node) { + File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName()); + return findEditor(f); + } + public class ASTNodeHighlighter { public final String clazzName; private ScriptArea.RegionStyle lastRegion; @@ -252,7 +186,8 @@ public class ScriptController { } public void remove() { - lastScriptArea.getMarkedRegions().remove(lastRegion); + if (lastScriptArea != null) + lastScriptArea.getMarkedRegions().remove(lastRegion); } public void highlight(ASTNode node) { @@ -269,14 +204,10 @@ public class ScriptController { } private ScriptArea.RegionStyle asRegion(ASTNode node) { + assert node != null; return new ScriptArea.RegionStyle(node.getRuleContext().getStart().getStartIndex(), node.getRuleContext().getStop().getStopIndex(), clazzName); } } - - private ScriptArea findEditor(ASTNode node) { - File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName()); - return findEditor(f); - } } diff --git a/src/main/java/edu/kit/formal/gui/controls/Utils.java b/src/main/java/edu/kit/formal/gui/controls/Utils.java index 0b2af841..6bac68af 100644 --- a/src/main/java/edu/kit/formal/gui/controls/Utils.java +++ b/src/main/java/edu/kit/formal/gui/controls/Utils.java @@ -1,17 +1,122 @@ package edu.kit.formal.gui.controls; +import de.uka.ilkd.key.logic.op.IProgramMethod; +import de.uka.ilkd.key.pp.ProgramPrinter; +import de.uka.ilkd.key.speclang.Contract; +import javafx.beans.property.Property; +import javafx.beans.value.ChangeListener; +import javafx.beans.value.ObservableValue; import javafx.fxml.FXMLLoader; +import javafx.scene.control.Alert; +import javafx.scene.control.Label; +import javafx.scene.control.TextArea; +import javafx.scene.layout.GridPane; +import javafx.scene.layout.Priority; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; import java.io.IOException; +import java.io.PrintWriter; +import java.io.StringWriter; +import java.util.Random; /** * @author Alexander Weigl * @version 1 (05.06.17) */ public class Utils { + private static Logger logger = LogManager.getLogger(Utils.class); + + private static String[] ADJECTIVES = + ("abandoned,able,absolute,adorable,adventurous,academic,acceptable,acclaimed,accomplished,accurate,aching,acidic,acrobatic,active,actual,adept,admirable,admired," + + "adolescent,adorable,adored,advanced,afraid,affectionate,aged,aggravating,aggressive,agile,agitated,agonizing,agreeable,ajar,alarmed,alarming,alert," + + "alienated,alive,all,altruistic,amazing,ambitious,ample,amused,amusing,anchored,ancient,angelic,angry,anguished,animated,annual,another,antique,anxious," + + "any,apprehensive,appropriate,apt,arctic,arid,aromatic,artistic,ashamed,assured,astonishing,athletic,attached,attentive,attractive,austere,authentic,authorized," + + "automatic,avaricious,average,aware,awesome,awful,awkward,babyish,bad,back,baggy,bare,barren,basic,beautiful,belated,beloved,beneficial,better,best,bewitched," + + "big,big-hearted,biodegradable,bite-sized,bitter,black,black-and-white,bland,blank,blaring,bleak,blind,blissful,blond,blue,blushing,bogus,boiling,bold,bony," + + "boring,bossy,both,bouncy,bountiful,bowed,brave,breakable,brief,bright,brilliant,brisk,broken,bronze,brown,bruised,bubbly,bulky,bumpy,buoyant,burdensome,burly," + + "bustling,busy,buttery,buzzing,calculating,calm,candid,canine,capital,carefree,careful,careless,caring,cautious,cavernous,celebrated,charming,cheap,cheerful," + + "cheery,chief,chilly,chubby,circular,classic,clean,clear,clear-cut,clever,close,closed,cloudy,clueless,clumsy,cluttered,coarse,cold,colorful,colorless," + + "colossal,comfortable,common,compassionate,competent,complete,complex,complicated,composed,concerned,concrete,confused,conscious,considerate,constant,content," + + "conventional,cooked,cool,cooperative,coordinated,corny,corrupt,costly,courageous,courteous,crafty,crazy,creamy,creative,creepy,criminal,crisp,critical," + + "crooked,crowded,cruel,crushing,cuddly,cultivated,cultured,cumbersome,curly,curvy,cute,cylindrical,damaged,damp,dangerous,dapper,daring,darling,dark,dazzling" + + ",dead,deadly,deafening,dear,dearest,decent,decimal,decisive,deep,defenseless,defensive,defiant,deficient,definite,definitive,delayed,delectable,delicious," + + "delightful,delirious,demanding,dense,dental,dependable,dependent,descriptive,deserted,detailed,determined,devoted,different,difficult,digital,diligent,dim," + + "dimpled,dimwitted,direct,disastrous,discrete,disfigured,disgusting,disloyal,dismal,distant,downright,dreary,dirty,disguised,dishonest,dismal,distant,distinct," + + "distorted,dizzy,dopey,doting,double,downright,drab,drafty,dramatic,dreary,droopy,dry,dual,dull,dutiful,each,eager,earnest,early,easy,easy-going,ecstatic,edible" + + ",educated,elaborate,elastic,elated,elderly,electric,elegant,elementary,elliptical,embarrassed,embellished,eminent,emotional,empty,enchanted,enchanting,energetic," + + "enlightened,enormous,enraged,entire,envious,equal,equatorial,essential,esteemed,ethical,euphoric,even,evergreen,everlasting,every,evil,exalted,excellent,exemplary" + + ",exhausted,excitable,excited,exciting,exotic,expensive,experienced,expert,extraneous,extroverted,extra-large,extra-small,fabulous,failing,faint,fair,faithful,fake" + + ",false,familiar,famous,fancy,fantastic,far,faraway,far-flung,far-off,fast,fat,fatal,fatherly,favorable,favorite,fearful,fearless,feisty,feline,female,feminine,few," + + "fickle,filthy,fine,finished,firm,first,firsthand,fitting,fixed,flaky,flamboyant,flashy,flat,flawed,flawless,flickering,flimsy,flippant,flowery,fluffy,fluid," + + "flustered,focused,fond,foolhardy,foolish,forceful,forked,formal,forsaken,forthright,fortunate,fragrant,frail,frank,frayed,free,French,fresh,frequent,friendly," + + "frightened,frightening,frigid,frilly,frizzy,frivolous,front,frosty,frozen,frugal,fruitful,full,fumbling,functional,funny,fussy,fuzzy,gargantuan,gaseous,general" + + ",generous,gentle,genuine,giant,giddy,gigantic,gifted,giving,glamorous,glaring,glass,gleaming,gleeful,glistening,glittering,gloomy,glorious,glossy,glum,golden," + + "good,good-natured,gorgeous,graceful,gracious,grand,grandiose,granular,grateful,grave,gray,great,greedy,green,gregarious,grim,grimy,gripping,grizzled,gross" + + ",grotesque,grouchy,grounded,growing,growling,grown,grubby,gruesome,grumpy,guilty,gullible,gummy,hairy,half,handmade,handsome,handy,happy,happy-go-lucky,hard," + + "harmful,harmless,harmonious,harsh,hasty,hateful,haunting,healthy,heartfelt,hearty,heavenly,heavy,hefty,helpful,helpless,hidden,hideous,high,high-level,hilarious," + + "hoarse,hollow,homely,honest,honorable,honored,hopeful,horrible,hospitable,hot,huge,humble,humiliating,humming,humongous,hungry,hurtful,husky,icky,icy,ideal," + + "idealistic,identical,idle,idiotic,idolized,ignorant,ill,illegal,ill-fated,ill-informed,illiterate,illustrious,imaginary,imaginative,immaculate,immaterial,immediate" + + ",immense,impassioned,impeccable,impartial,imperfect,imperturbable,impish,impolite,important,impossible,impractical,impressionable,impressive,improbable,impure" + + ",inborn,incomparable,incompatible,incomplete,inconsequential,incredible,indelible,inexperienced,indolent,infamous,infantile,infatuated,inferior,infinite,informal" + + ",innocent,insecure,insidious,insignificant,insistent,instructive,insubstantial,intelligent,intent,intentional,interesting,internal,international,intrepid,ironclad" + + ",irresponsible,irritating,itchy,jaded,jagged,jam-packed,jaunty,jealous,jittery,joint,jolly,jovial,joyful,joyous,jubilant,judicious,juicy,jumbo,junior,jumpy,juvenile," + + "kaleidoscopic,keen,key,kind,kindhearted,kindly,klutzy,knobby,knotty,knowledgeable,knowing,known,kooky,kosher,lame,lanky,large,last,lasting,late,lavish,lawful,lazy,leading," + + "lean,leafy,left,legal,legitimate,light,lighthearted,likable,likely,limited,limp,limping,linear,lined,liquid,little,live,lively,livid,loathsome,lone,lonely,long," + + "loose,lopsided,lost,loud,lovable,lovely,loving,low,loyal,lucky,lumbering,luminous,lumpy,lustrous,luxurious,mad,made-up,magnificent,majestic,major,male,mammoth,married," + + "marvelous,masculine,massive,mature,meager,mealy,mean,measly,meaty,medical,mediocre,medium,meek,mellow,melodic,memorable,menacing,merry,messy,metallic,mild,milky,mindless," + + "miniature,minor,minty,miserable,miserly,misguided,misty,mixed,modern,modest,moist,monstrous,monthly,monumental,moral,mortified,motherly,motionless,mountainous,muddy,muffled," + + "multicolored,mundane,murky,mushy,musty,muted,mysterious,naive,narrow,nasty,natural,naughty,nautical,near,neat,necessary,needy,negative,neglected,negligible,neighboring," + + "nervous,new,next,nice,nifty,nimble,nippy,nocturnal,noisy,nonstop,normal,notable,noted,noteworthy,novel,noxious,numb,nutritious,nutty,obedient,obese,oblong,oily,oblong," + + "obvious,occasional,odd,oddball,offbeat,offensive,official,old,old-fashioned,only,open,optimal,optimistic,opulent,orange,orderly,organic,ornate,ornery,ordinary,original,other," + + "our,outlying,outgoing,outlandish,outrageous,outstanding,oval,overcooked,overdue,overjoyed,overlooked,palatable,pale,paltry,parallel,parched,partial,passionate,past,pastel," + + "peaceful,peppery,perfect,perfumed,periodic,perky,personal,pertinent,pesky,pessimistic,petty,phony,physical,piercing,pink,pitiful,plain,plaintive,plastic,playful,pleasant," + + "pleased,pleasing,plump,plush,polished,polite,political,pointed,pointless,poised,poor,popular,portly,posh,positive,possible,potable,powerful,powerless,practical,precious," + + "present,prestigious,pretty,precious,previous,pricey,prickly,primary,prime,pristine,private,prize,probable,productive,profitable,profuse,proper,proud,prudent,punctual,pungent," + + "puny,pure,purple,pushy,putrid,puzzled,puzzling,quaint,qualified,quarrelsome,quarterly,queasy,querulous,questionable,quick,quick-witted,quiet,quintessential,quirky,quixotic," + + "quizzical,radiant,ragged,rapid,rare,rash,raw,recent,reckless,rectangular,ready,real,realistic,reasonable,red,reflecting,regal,regular,reliable,relieved,remarkable,remorseful," + + "remote,repentant,required,respectful,responsible,repulsive,revolving,rewarding,rich,rigid,right,ringed,ripe,roasted,robust,rosy,rotating,rotten,rough,round,rowdy,royal,rubbery," + + "rundown,ruddy,rude,runny,rural,rusty,sad,safe,salty,same,sandy,sane,sarcastic,sardonic,satisfied,scaly,scarce,scared,scary,scented,scholarly,scientific,scornful,scratchy,scrawny," + + "second,secondary,second-hand,secret,self-assured,self-reliant,selfish,sentimental,separate,serene,serious,serpentine,several,severe,shabby,shadowy,shady,shallow,shameful,shameless," + + "sharp,shimmering,shiny,shocked,shocking,shoddy,short,short-term,showy,shrill,shy,sick,silent,silky,silly,silver,similar,simple,simplistic,sinful,single,sizzling,skeletal,skinny," + + "sleepy,slight,slim,slimy,slippery,slow,slushy,small,smart,smoggy,smooth,smug,snappy,snarling,sneaky,sniveling,snoopy,sociable,soft,soggy,solid,somber,some,spherical,sophisticated" + + ",sore,sorrowful,soulful,soupy,sour,Spanish,sparkling,sparse,specific,spectacular,speedy,spicy,spiffy,spirited,spiteful,splendid,spotless,spotted,spry,square,squeaky," + + "squiggly,stable,staid,stained,stale,standard,starchy,stark,starry,steep,sticky,stiff,stimulating,stingy,stormy,straight,strange,steel,strict,strident,striking,striped,strong," + + "studious,stunning,stupendous,stupid,sturdy,stylish,subdued,submissive,substantial,subtle,suburban,sudden,sugary,sunny,super,superb,superficial,superior,supportive,sure-footed" + + ",surprised,suspicious,svelte,sweaty,sweet,sweltering,swift,sympathetic,tall,talkative,tame,tan,tangible,tart,tasty,tattered,taut,tedious,teeming,tempting,tender,tense,tepid," + + "terrible,terrific,testy,thankful,that,these,thick,thin,third,thirsty,this,thorough,thorny,those,thoughtful,threadbare,thrifty,thunderous,tidy,tight,timely,tinted,tiny,tired,torn" + + ",total,tough,traumatic,treasured,tremendous,tragic,trained,tremendous,triangular,tricky,trifling,trim,trivial,troubled,true,trusting,trustworthy,trusty,truthful,tubby,turbulent" + + ",twin,ugly,ultimate,unacceptable,unaware,uncomfortable,uncommon,unconscious,understated,unequaled,uneven,unfinished,unfit,unfolded,unfortunate,unhappy,unhealthy,uniform," + + "unimportant,unique,united,unkempt,unknown,unlawful,unlined,unlucky,unnatural,unpleasant,unrealistic,unripe,unruly,unselfish,unsightly,unsteady,unsung,untidy,untimely,untried," + + "untrue,unused,unusual,unwelcome,unwieldy,unwilling,unwitting,unwritten,upbeat,upright,upset,urban,usable,used,useful,useless,utilized,utter,vacant,vague,vain,valid,valuable," + + "vapid,variable,vast,velvety,venerated,vengeful,verifiable,vibrant,vicious,victorious,vigilant,vigorous,villainous,violet,violent,virtual,virtuous,visible,vital,vivacious,vivid," + + "voluminous,wan,warlike,warm,warmhearted,warped,wary,wasteful,watchful,waterlogged,watery,wavy,wealthy,weak,weary,webbed,wee,weekly,weepy,weighty,weird,welcome,well-documented" + + ",well-groomed,well-informed,well-lit,well-made,well-off,well-to-do,well-worn,wet,which,whimsical,whirlwind,whispered,white,whole,whopping,wicked,wide,wide-eyed,wiggly,wild," + + "willing,wilted,winding,windy,winged,wiry,wise,witty,wobbly,woeful,wonderful,wooden,woozy,wordy,worldly,worn,worried,worrisome," + + "worse,worst,worthless,worthwhile,worthy,wrathful,wretched,writhing,wrong,wry,yawning,yearly,yellow,yellowish,young,youthful,yummy,zany,zealous,zesty,zigzag").split(","); + private static String[] ANIMALS = + ("Cat,Caterpillar,Cattle,Chamois,Cheetah,Chicken,Chimpanzee,Chinchilla,Chough,Coati,Cobra,Cockroach,Cod,Cormorant," + + "Coyote,Crab,Crane,Crocodile,Crow,Curlew,Deer,Dinosaur,,Dog,,Dogfish,Shark,Dolphin,Donkey," + + "Dotterel,Dove,Dragonfly,Duck,,Mallard,Dugong,Dunlin,Eagle,Echidna,Eel,Eland,Elephant,Elephant,seal,Elk," + + "Emu,Falcon,Ferret,Finch,Fish,,Flamingo,Fly,Fox,Frog,Gaur,Gazelle,Gerbil,Giant,panda,Giraffe,Gnat,Gnu,Goat" + + ",Goldfinch,Goosander,Goose,Gorilla,Goshawk,Grasshopper,Grouse,Guanaco,Guinea,fowl,Guinea,pig,Gull,Hamster,Hare,Hawk,Hedgehog," + + "Heron,Herring,Hippo,Hornet,Horse,,Hummingbird,Hyena,Ibex,Ibis,Jackal,Jaguar,Jay,Jellyfish,Kangaroo,Kinkajou,Koala,Komodo,dragon," + + "Kouprey,Kudu,Lapwing,Lark,Lemur,Leopard,Lion,Llama,Lobster,Locust,,Loris,Louse,Lyrebird,Magpie,Mallard,Duck,Mammoth,Manatee,Mandrill,Mink," + + "Mole,Mongoose,Monkey,Moose,Mouse,Mosquito,Narwhal,Newt,Nightingale,Octopus,Okapi,Opossum,Ostrich,Otter,Owl,Oyster,Panther,Parrot,Panda," + + "Partridge,Peafowl,Pelican,Penguin,Pheasant,Pig,Boar,Pigeon,,Polarbear,Horse,Porcupine,Porpoise,Prairie dog," + + "Quail,Quelea,Quetzal,Rabbit,,Raccoon,Ram,Sheep,Rat,,Raven,Red,deer,Red,panda,Reindeer,(caribou),Rhinoceros,Rook,Salamander,Salmon,Sandpiper," + + "Sardine,Sea,lion,Sea,urchin,Seahorse,Seal,Shark,Sheep,,Ram,Shrew,Skunk,Sloth,Snail,Snake,,Spider,,Squirrel,Starling,Stegosaurus,Swan,Tapir," + + "Tarsier,Termite,Tiger,Toad,Turkey,,Turtle,Vicuña,Wallaby,Walrus,Wasp,Water,buffalo,Weasel,Whale,Wolf,Wolverine,Wombat,Wren,Yak,Zebra").split(","); + private Utils() { } + + public static String getRandomName() { + Random r = new Random(); + return (ADJECTIVES[r.nextInt(ADJECTIVES.length)] + "_" + ANIMALS[r.nextInt(ANIMALS.length)] + ".kps").toLowerCase(); + } + public static void createWithFXML(Object node) { FXMLLoader loader = new FXMLLoader( node.getClass().getResource(node.getClass().getSimpleName() + ".fxml") @@ -24,4 +129,67 @@ public class Utils { throw new RuntimeException("Could not load fxml", e); } } + + public static String getJavaCode(Contract c) { + IProgramMethod method = (IProgramMethod) c.getTarget(); + StringWriter writer = new StringWriter(); + ProgramPrinter pp = new ProgramPrinter(writer); + try { + pp.printFullMethodSignature(method); + pp.printStatementBlock(method.getBody()); + writer.flush(); + } catch (IOException e) { + logger.catching(e); + } + return writer.toString(); + } + + 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(); + } + + public static void addDebugListener(Property property) { + property.addListener((ChangeListener) (observable, oldValue, newValue) -> { + String simpleName = property.getBean() != null ? property.getBean().getClass().getSimpleName() : ""; + logger.debug("Property '{}' of '{}' changed from {} to {}", + property.getName(), simpleName, oldValue, newValue); + }); + } + + public static void addDebugListener(Property property, java.util.function.Function conv) { + property.addListener((observable, oldValue, newValue) -> + logger.debug("Property '{}' of '%s' changed from {} to {}", property.getName(), + property.getBean().getClass().getSimpleName(), conv.apply(oldValue), conv.apply(newValue))); + } + + public static void addDebugListener(ObservableValue o, String id) { + o.addListener((ChangeListener) (observable, oldValue, newValue) -> + logger.debug("Observable {} changed from {} to {}", id, oldValue, newValue)); + } } diff --git a/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java b/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java index 46d0d0d0..5f27129a 100644 --- a/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java +++ b/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java @@ -1,9 +1,9 @@ package edu.kit.formal.gui.controls; import edu.kit.formal.gui.controller.DebuggerMainWindowController; +import javafx.event.ActionEvent; import javafx.scene.layout.AnchorPane; -import java.awt.event.ActionEvent; import java.io.File; /** @@ -17,7 +17,7 @@ public class WelcomePane extends AnchorPane { Utils.createWithFXML(this); } - public void loadContraPosition(javafx.event.ActionEvent event) { + public void loadContraPosition(ActionEvent event) { proofScriptDebugger.getWelcomePaneDock().close(); proofScriptDebugger.showActiveInspector(null); proofScriptDebugger.openScript( @@ -28,4 +28,15 @@ public class WelcomePane extends AnchorPane { new File("src/test/resources/edu/kit/formal/interpreter/contraposition/contraposition.key")); } + + public void loadJavaTest(ActionEvent event) { + proofScriptDebugger.getWelcomePaneDock().close(); + proofScriptDebugger.showActiveInspector(null); + proofScriptDebugger.openScript( + new File("src/test/resources/edu/kit/formal/interpreter/dbg.kps") + ); + + proofScriptDebugger.openJavaFile( + new File("src/test/resources/edu/kit/formal/interpreter/javaExample/TwoWaySwap.java")); + } } diff --git a/src/main/java/edu/kit/formal/gui/model/InspectionModel.java b/src/main/java/edu/kit/formal/gui/model/InspectionModel.java index becf5027..b33b3f56 100644 --- a/src/main/java/edu/kit/formal/gui/model/InspectionModel.java +++ b/src/main/java/edu/kit/formal/gui/model/InspectionModel.java @@ -24,6 +24,8 @@ public class InspectionModel { private final ObjectProperty node = new SimpleObjectProperty<>(); private final ListProperty> goals = new SimpleListProperty<>(); private final ObjectProperty> selectedGoalNodeToShow = new SimpleObjectProperty<>(); + private final ObjectProperty> currentInterpreterGoal = new SimpleObjectProperty<>(); + private final MapProperty colorofEachGoalNodeinListView = new SimpleMapProperty<>(FXCollections.observableHashMap()); //private final StringProperty javaString = new SimpleStringProperty(); private final SetProperty highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet()); @@ -31,6 +33,31 @@ public class InspectionModel { private final BooleanProperty isInterpreterTab = new SimpleBooleanProperty(); private ObjectProperty mode = new SimpleObjectProperty<>(); + + public GoalNode getCurrentInterpreterGoal() { + return currentInterpreterGoal.get(); + } + + public ObjectProperty> currentInterpreterGoalProperty() { + return currentInterpreterGoal; + } + + public void setCurrentInterpreterGoal(GoalNode currentInterpreterGoal) { + this.currentInterpreterGoal.set(currentInterpreterGoal); + } + + public Mode getMode() { + return mode.get(); + } + + public ObjectProperty modeProperty() { + return mode; + } + + public void setMode(Mode mode) { + this.mode.set(mode); + } + public ASTNode getNode() { return node.get(); } diff --git a/src/main/java/edu/kit/formal/gui/model/RootModel.java b/src/main/java/edu/kit/formal/gui/model/RootModel.java deleted file mode 100644 index e6463f43..00000000 --- a/src/main/java/edu/kit/formal/gui/model/RootModel.java +++ /dev/null @@ -1,152 +0,0 @@ -package edu.kit.formal.gui.model; - - -import de.uka.ilkd.key.speclang.Contract; -import edu.kit.formal.interpreter.data.GoalNode; -import edu.kit.formal.interpreter.data.KeyData; -import javafx.beans.property.ListProperty; -import javafx.beans.property.SimpleListProperty; -import javafx.beans.property.SimpleObjectProperty; -import javafx.collections.FXCollections; -import javafx.collections.ObservableList; - -import java.io.File; - -/** - * Model for the root window - * - * @author S. Grebing - */ -public class RootModel { - - /** - * Property: current loaded ScriptFile - */ - private final SimpleObjectProperty scriptFile = new SimpleObjectProperty<>(); - - - /** - * Property: current loaded javaFile - */ - private final SimpleObjectProperty javaFile = new SimpleObjectProperty<>(); - - /** - * Property: current loaded KeY File - */ - private final SimpleObjectProperty keYFile = new SimpleObjectProperty<>(); - - - /** - * ListProperty: list of goal nodes in the current state (depending on interpreter state) - */ - private final ListProperty> currentGoalNodes = new SimpleListProperty<>(FXCollections.observableArrayList()); - - /** - * Current SelectedGoalNode - */ - private final SimpleObjectProperty> currentSelectedGoalNode = new SimpleObjectProperty<>(); - - /** - * Loaded contracts - */ - private final SimpleListProperty loadedContracts = new SimpleListProperty<>(FXCollections.observableArrayList()); - - /** - * Chosen contract for problem - */ - private final SimpleObjectProperty chosenContract = new SimpleObjectProperty<>(); - - public RootModel() { - - } - - - /***************************************************************************************************************** - * Property Getter and Setter - ***************************************************************************************************************/ - public File getScriptFile() { - return scriptFile.get(); - } - - public void setScriptFile(File scriptFile) { - this.scriptFile.set(scriptFile); - } - - public SimpleObjectProperty scriptFileProperty() { - return scriptFile; - } - - public File getKeYFile() { - return keYFile.get(); - } - - public void setKeYFile(File keYFile) { - this.keYFile.set(keYFile); - } - - public SimpleObjectProperty keYFileProperty() { - return keYFile; - } - - public ObservableList> getCurrentGoalNodes() { - return currentGoalNodes.get(); - } - - public void setCurrentGoalNodes(ObservableList> currentGoalNodes) { - this.currentGoalNodes.set(currentGoalNodes); - } - - public ListProperty> currentGoalNodesProperty() { - return currentGoalNodes; - } - - public GoalNode getCurrentSelectedGoalNode() { - return currentSelectedGoalNode.get(); - } - - public void setCurrentSelectedGoalNode(GoalNode currentSelectedGoalNode) { - this.currentSelectedGoalNode.set(currentSelectedGoalNode); - } - - public SimpleObjectProperty> currentSelectedGoalNodeProperty() { - return currentSelectedGoalNode; - } - - public File getJavaFile() { - return javaFile.get(); - } - - public void setJavaFile(File javaFile) { - this.javaFile.set(javaFile); - } - - public SimpleObjectProperty javaFileProperty() { - return javaFile; - } - - public ObservableList getLoadedContracts() { - return loadedContracts.get(); - } - - public void setLoadedContracts(ObservableList loadedContracts) { - this.loadedContracts.set(loadedContracts); - } - - public SimpleListProperty loadedContractsProperty() { - return loadedContracts; - } - - public Contract getChosenContract() { - return chosenContract.get(); - } - - public void setChosenContract(Contract chosenContract) { - this.chosenContract.set(chosenContract); - } - - public SimpleObjectProperty chosenContractProperty() { - return chosenContract; - } - - -} diff --git a/src/main/java/edu/kit/formal/interpreter/InterpretingService.java b/src/main/java/edu/kit/formal/interpreter/InterpretingService.java index 21a346b5..e24120e6 100644 --- a/src/main/java/edu/kit/formal/interpreter/InterpretingService.java +++ b/src/main/java/edu/kit/formal/interpreter/InterpretingService.java @@ -1,7 +1,7 @@ package edu.kit.formal.interpreter; -import edu.kit.formal.gui.controller.DebuggerMainWindowController; import edu.kit.formal.gui.controller.PuppetMaster; +import edu.kit.formal.gui.controls.Utils; import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.State; import edu.kit.formal.proofscriptparser.ast.ProofScript; @@ -50,7 +50,7 @@ public class InterpretingService extends Service> { @Override protected void failed() { getException().printStackTrace(); - DebuggerMainWindowController.showExceptionDialog("Execution failed", "", "", getException()); + Utils.showExceptionDialog("Execution failed", "", "", getException()); updateView(); } diff --git a/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java b/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java index 7d7e8cc8..98821d72 100644 --- a/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java @@ -11,6 +11,8 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript; import javafx.application.Platform; import javafx.beans.property.*; import javafx.collections.FXCollections; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; import java.util.List; @@ -20,6 +22,7 @@ import java.util.List; * @author S. Grebing */ public class ProofTreeController { + private static final Logger LOGGER = LogManager.getLogger(ProofTreeController.class); /** * To control stepping @@ -240,10 +243,12 @@ public class ProofTreeController { * @param state */ private void setNewState(State state) { - this.setCurrentGoals(state.getGoals()); - this.setCurrentSelectedGoal(state.getSelectedGoalNode()); + setCurrentGoals(state.getGoals()); + setCurrentSelectedGoal(state.getSelectedGoalNode()); setCurrentHighlightNode(statePointer.getScriptstmt()); - System.out.println("New State from this command: " + this.statePointer.getScriptstmt().getNodeName() + "@" + this.statePointer.getScriptstmt().getStartPosition()); + LOGGER.debug("New State from this command: %s@%s", + this.statePointer.getScriptstmt().getNodeName(), + this.statePointer.getScriptstmt().getStartPosition()); } /************************************************************************************************************** diff --git a/src/main/resources/edu/kit/formal/gui/controls/InspectionViewTab.fxml b/src/main/resources/edu/kit/formal/gui/controls/InspectionView.fxml similarity index 100% rename from src/main/resources/edu/kit/formal/gui/controls/InspectionViewTab.fxml rename to src/main/resources/edu/kit/formal/gui/controls/InspectionView.fxml diff --git a/src/main/resources/edu/kit/formal/gui/controls/InspectionViewTabPane.fxml b/src/main/resources/edu/kit/formal/gui/controls/InspectionViewTabPane.fxml index eb1073f3..cb81a075 100644 --- a/src/main/resources/edu/kit/formal/gui/controls/InspectionViewTabPane.fxml +++ b/src/main/resources/edu/kit/formal/gui/controls/InspectionViewTabPane.fxml @@ -3,5 +3,5 @@ - + + + -