Better StatusBar, little refactoring in contract chooser

src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java

@@ -14,6 +14,8 @@ import javafx.scene.Scene;
 import javafx.stage.Stage;
 
 import java.io.IOException;
+import java.util.Locale;
+import java.util.logging.Level;
 import java.util.logging.Logger;
 
 public class ProofScriptDebugger extends Application {
@@ -29,12 +31,7 @@ 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"));
             Parent root = fxmlLoader.load();
@@ -43,10 +40,18 @@ public class ProofScriptDebugger extends Application {
             scene.getStylesheets().addAll(
                     getClass().getResource("debugger-ui.css").toExternalForm()
             );
-
             primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION);
             primaryStage.setScene(scene);
             primaryStage.show();
+
+
+            logger.info("Start: " + NAME);
+            logger.info("Version: " + VERSION);
+            logger.info("KeY: " + KeYConstants.COPYRIGHT);
+            logger.info("KeY Version: " + KeYConstants.VERSION);
+            logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
+            logger.log(Level.SEVERE, "sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
+
         } catch (IOException e) {
             e.printStackTrace();
         }

src/main/java/edu/kit/formal/gui/controller/ContractChooser.java

@@ -5,12 +5,22 @@ import de.uka.ilkd.key.speclang.Contract;
 import javafx.beans.property.ObjectProperty;
 import javafx.beans.property.SimpleListProperty;
 import javafx.collections.ObservableList;
+import javafx.event.EventHandler;
 import javafx.scene.control.*;
 import javafx.scene.layout.VBox;
+import javafx.stage.Modality;
 import lombok.Getter;
 
+import java.awt.event.KeyEvent;
+
 /**
+ * A Contract Chooser is a modal dialog, which shows a list of contracts and lets the user select one.
+ * <p>
+ * <p>
+ * <p>
+ * <p>
  * WizardPane to display all available contracts
+ *
  * @author S. Grebing
  * @author A. Weigl
  */
@@ -18,26 +28,36 @@ public class ContractChooser extends Dialog<Contract> {
     @Getter
     private final MultipleSelectionModel<Contract> selectionModel;
     private final ObjectProperty<ObservableList<Contract>> items;
-    private final ListView<Contract> listOfContractsView;
+    private final ListView<Contract> listOfContractsView = new ListView<>();
     private final Services services;
 
     public ContractChooser(Services services) {
         super();
+        this.services = services;
+
         setTitle("Key Contract Chooser");
         setHeaderText("Please select a contract");
-        this.services = services;
-        listOfContractsView = new ListView<>();
+        setResizable(true);
+
+        initModality(Modality.APPLICATION_MODAL);
+
         selectionModel = listOfContractsView.getSelectionModel();
         items = listOfContractsView.itemsProperty();
+
         DialogPane dpane = new DialogPane();
         dpane.setContent(listOfContractsView);
+        dpane.setPrefSize(680, 320);
         setDialogPane(dpane);
+
         listOfContractsView.setCellFactory(ContractListCell::new);
-        setResizable(true);
-        dpane.setPrefSize(680, 320);
 
         setResultConverter((value) -> value == ButtonType.OK ? listOfContractsView.getSelectionModel().getSelectedItem() : null);
         dpane.getButtonTypes().addAll(ButtonType.OK, ButtonType.CANCEL);
+
+        final Button okButton = (Button) dpane.lookupButton(ButtonType.OK);
+        okButton.setDefaultButton(true);
+
+        listOfContractsView.setOnKeyPressed(event -> okButton.fire());
     }
 
     public ContractChooser(Services services,
@@ -228,10 +248,16 @@ public class ContractChooser extends Dialog<Contract> {
                 return;
             }
 
+            VBox box = new VBox();
             Label head = new Label(getItem().getDisplayName() + "\n");
-            head.setWrapText(true);
-            head.setStyle("-fx-font-weight: bold; -fx-font-size: 120%");
-            setGraphic(new VBox(head, new Label(getItem().getPlainText(services))));
+            head.getStyleClass().add("title");
+
+            Label contract = new Label(getItem().getPlainText(services));
+            contract.getStyleClass().add("contract");
+
+            setGraphic(
+                    new VBox(head, contract)
+            );
         }
     }
 }

src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java

@@ -56,6 +56,7 @@ public class DebuggerMainWindowController implements Initializable {
     private final PuppetMaster blocker = new PuppetMaster();
     private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
     private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
+
     @FXML
     private Pane rootPane;
     @FXML
@@ -101,12 +102,11 @@ public class DebuggerMainWindowController implements Initializable {
      * references to objects needed for controlling backend through UI
      */
     private RootModel model = new RootModel();
+
+
     @FXML
-    private Label lblStatusMessage;
-    @FXML
-    private Label lblCurrentNodes;
-    @FXML
-    private Label lblFilename;
+    private DebuggerStatusBar statusBar;
+
     private File initialDirectory;
 
     @FXML
@@ -156,11 +156,15 @@ 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"));
         });
 
 
@@ -258,10 +262,10 @@ public class DebuggerMainWindowController implements Initializable {
     private void executeScript(InterpreterBuilder ib, boolean debugMode) {
         this.debugMode.set(debugMode);
         blocker.deinstall();
-        lblStatusMessage.setText("Parse ...");
+        statusBar.publishMessage("Parse ...");
         try {
             List<ProofScript> scripts = Facade.getAST(scriptArea.getText());
-            lblStatusMessage.setText("Creating new Interpreter instance ...");
+            statusBar.publishMessage("Creating new Interpreter instance ...");
             ib.setScripts(scripts);
             ib.captureHistory();
 
@@ -344,7 +348,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());
             });
 
@@ -462,7 +466,7 @@ public class DebuggerMainWindowController implements Initializable {
 
         @Override
         protected void succeeded() {
-            lblStatusMessage.setText("Contract loaded");
+            statusBar.publishMessage("Contract loaded");
             model.getLoadedContracts().setAll(getValue());
             //FIXME model braucht contracts nicht
             ContractChooser cc = new ContractChooser(facade.getService(), model.loadedContractsProperty());

src/main/java/edu/kit/formal/gui/controls/DebuggerStatusBar.java

+package edu.kit.formal.gui.controls;
+
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
+import javafx.beans.binding.StringBinding;
+import javafx.beans.property.ListProperty;
+import javafx.beans.property.SimpleListProperty;
+import javafx.beans.property.SimpleObjectProperty;
+import javafx.beans.property.SimpleStringProperty;
+import javafx.beans.value.ChangeListener;
+import javafx.beans.value.ObservableStringValue;
+import javafx.beans.value.ObservableValue;
+import javafx.collections.FXCollections;
+import javafx.collections.ObservableList;
+import javafx.event.ActionEvent;
+import javafx.event.EventHandler;
+import javafx.scene.Node;
+import javafx.scene.control.*;
+import javafx.scene.input.MouseButton;
+import javafx.scene.input.MouseEvent;
+import javafx.scene.layout.BorderPane;
+import javafx.stage.Modality;
+import javafx.util.Callback;
+import org.controlsfx.control.StatusBar;
+
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.util.Date;
+import java.util.LinkedList;
+import java.util.logging.*;
+
+/**
+ * Created by weigl on 09.06.2017.
+ */
+public class DebuggerStatusBar extends StatusBar {
+    private Label lblCurrentNodes = new Label("#nodes: %s");
+    private ProgressIndicator progressIndicator = new ProgressIndicator();
+    private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
+    private EventHandler<MouseEvent> toolTipHandler = event -> {
+        publishMessage(((Control) event.getTarget()).getTooltip().getText());
+    };
+
+    private final ContextMenu contextMenu = createContextMenu();
+    private final Dialog<Void> loggerDialog = createDialog();
+
+    public DebuggerStatusBar() {
+        listenOnField("psdbg");
+
+        getRightItems().addAll(
+                lblCurrentNodes,
+                progressIndicator
+        );
+
+        setOnMouseClicked(event -> {
+            if (event.getButton() == MouseButton.SECONDARY) {
+                contextMenu.show(this, event.getScreenX(), event.getScreenY());
+            }
+        });
+    }
+
+    private final Handler loggerHandler = new Handler() {
+        @Override
+        public void publish(LogRecord record) {
+            publishMessage(record.getMessage());
+        }
+
+        @Override
+        public void flush() {
+
+        }
+
+        @Override
+        public void close() throws SecurityException {
+
+        }
+    };
+
+    public void publishMessage(String format, Object... args) {
+        String msg = String.format(format, args);
+        setText(msg);
+    }
+
+    public EventHandler<MouseEvent> getTooltipHandler() {
+        return toolTipHandler;
+    }
+
+    public void listenOnField(ObservableStringValue value) {
+        value.addListener((observable, oldValue, newValue) -> {
+            publishMessage(newValue);
+        });
+    }
+
+    public void listenOnField(Logger logger) {
+        logger.addHandler(loggerHandler);
+        logger.addHandler(logCatchHandler);
+
+        logger.info("Listener added");
+    }
+
+    public void listenOnField(String loggerCategory) {
+        listenOnField(Logger.getLogger(loggerCategory));
+    }
+
+    public void indicateProgress() {
+        progressIndicator.setProgress(-1);
+    }
+
+    public void stopProgress() {
+        progressIndicator.setProgress(100);
+    }
+
+    public ContextMenu createContextMenu() {
+        ContextMenu cm = new ContextMenu();
+        Menu viewOptions = new Menu("View Options");
+        MenuItem showLog = new MenuItem("Show Log", new MaterialDesignIconView(MaterialDesignIcon.FORMAT_LIST_BULLETED));
+        showLog.setOnAction(this::showLog);
+        cm.getItems().addAll(viewOptions, showLog);
+        return cm;
+    }
+
+    private void showLog(ActionEvent actionEvent) {
+        loggerDialog.show();
+    }
+
+    public Dialog<Void> createDialog() {
+        final TableView<LogRecord> recordView = new TableView<>(logCatchHandler.recordsProperty());
+        recordView.setEditable(false);
+        recordView.setSortPolicy(param -> false);
+
+        TableColumn<LogRecord, Date> dateColumn = new TableColumn<>("Date");
+        TableColumn<LogRecord, Level> levelColumn = new TableColumn<>("Level");
+        //TableColumn<LogRecord, String> classColumn = new TableColumn<>("Class");
+        TableColumn<LogRecord, String> messageColumn = new TableColumn<>("Message");
+
+        recordView.getColumns().setAll(dateColumn, levelColumn, messageColumn);
+
+
+        dateColumn.setCellValueFactory(
+                param -> new SimpleObjectProperty<>(new Date(param.getValue().getMillis())
+                ));
+
+        levelColumn.setCellValueFactory(
+                param -> new SimpleObjectProperty<>(param.getValue().getLevel())
+        );
+
+        messageColumn.setCellValueFactory(
+                param -> {
+                    String s = formatter.formatMessage(param.getValue());
+                    if (param.getValue().getThrown() != null) {
+                        StringWriter sw = new StringWriter();
+                        PrintWriter pw = new PrintWriter(sw);
+                        pw.println();
+                        param.getValue().getThrown().printStackTrace(pw);
+                        pw.close();
+                        s += "\n" + sw.toString();
+                    }
+                    return new SimpleStringProperty(s);
+                }
+        );
+
+
+        Dialog<Void> dialog = new Dialog<>();
+        dialog.setResizable(true);
+        dialog.initModality(Modality.NONE);
+        dialog.setHeaderText("Logger Records");
+        DialogPane dpane = dialog.getDialogPane();
+        dpane.setContent(new BorderPane(recordView));
+        dpane.getButtonTypes().setAll(ButtonType.CLOSE);
+        return dialog;
+    }
+
+    public static class LogCatchHandlerFX extends Handler {
+        private ListProperty<LogRecord> records = new SimpleListProperty<>(FXCollections.observableList(
+                new LinkedList<>() //remove of head
+        ));
+
+        private int maxRecords = 5000;
+
+        @Override
+        public void publish(LogRecord record) {
+            records.add(record);
+            while (records.size() > maxRecords)
+                records.remove(0);
+        }
+
+        @Override
+        public void flush() {
+
+        }
+
+        @Override
+        public void close() throws SecurityException {
+
+        }
+
+        public ObservableList<LogRecord> getRecords() {
+            return records.get();
+        }
+
+        public ListProperty<LogRecord> recordsProperty() {
+            return records;
+        }
+
+        public void setRecords(ObservableList<LogRecord> records) {
+            this.records.set(records);
+        }
+
+        public int getMaxRecords() {
+            return maxRecords;
+        }
+
+        public void setMaxRecords(int maxRecords) {
+            this.maxRecords = maxRecords;
+        }
+    }
+
+    static SimpleFormatter formatter = new SimpleFormatter();
+
+    private static class LogRecordCellFactory extends ListCell<LogRecord> {
+        public LogRecordCellFactory(ListView<LogRecord> view) {
+        }
+
+        @Override
+        protected void updateItem(LogRecord item, boolean empty) {
+            if (empty)
+                super.updateItem(item, empty);
+            else {
+                Label lbl = new Label(formatter.format(item));
+                lbl.setWrapText(true);
+                lbl.getStyleClass().add(item.getLevel().getName());
+                setGraphic(lbl);
+            }
+        }
+    }
+}
+
+

src/main/resources/DebuggerMain.fxml

@@ -6,6 +6,7 @@
 <?import javafx.geometry.Insets?>
 <?import javafx.scene.control.*?>
 <?import javafx.scene.layout.*?>
+<?import org.controlsfx.control.StatusBar?>
 <BorderPane xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112"
             fx:controller="edu.kit.formal.gui.controller.DebuggerMainWindowController"
             prefWidth="1024" prefHeight="640">
@@ -185,12 +186,6 @@
         </MenuBar>
     </top>
     <bottom>
-        <HBox>
-            <Label fx:id="lblStatusMessage" HBox.hgrow="ALWAYS"/>
-            <Separator/>
-            <Label fx:id="lblCurrentNodes"/>
-            <Separator/>
-            <Label fx:id="lblFilename"/>
-        </HBox>
+        <DebuggerStatusBar fx:id="statusBar"/>
     </bottom>
 </BorderPane>

src/main/resources/edu/kit/formal/gui/debugger-ui.less

@@ -197,6 +197,18 @@
   }
 }
 
+.contract-chooser {
+  .head {
+    -fx-font-weight: bold;
+    -fx-font-size: 120%;
+  }
+
+  .contract {
+    -fx-wrap-text: true;
+    -fx-font-family: monospace;
+  }
+}
+
 .tab-pane {
   -fx-skin: "edu.kit.formal.gui.controls.CustomTabPaneSkin";
-}
\ No newline at end of file
+}