small improvements

* log4j
* HistoryListener.java enhanced
* Pull line hightlightning from JavaArea.java

pom.xml

@@ -303,6 +303,20 @@
             <version>0.9.2</version>
         </dependency>
 
+        <dependency>
+            <groupId>org.apache.logging.log4j</groupId>
+            <artifactId>log4j-api</artifactId>
+            <version>2.8</version>
+        </dependency>
+
+        <dependency>
+            <groupId>org.apache.logging.log4j</groupId>
+            <artifactId>log4j-core</artifactId>
+            <version>2.8</version>
+        </dependency>
+
+
+
     </dependencies>
 
 

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

@@ -12,18 +12,18 @@ import javafx.fxml.FXMLLoader;
 import javafx.scene.Parent;
 import javafx.scene.Scene;
 import javafx.stage.Stage;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 
 import java.io.IOException;
 import java.util.Locale;
-import java.util.logging.Level;
-import java.util.logging.Logger;
 
 public class ProofScriptDebugger extends Application {
     public static final String NAME = "Proof Script Debugger";
     public static final String VERSION = "0.1";
     public static final String KEY_VERSION = KeYConstants.VERSION;
 
-    private Logger logger = Logger.getLogger("psdbg");
+    private Logger logger = LogManager.getLogger("psdbg");
 
     public static void main(String[] args) {
         launch(args);
@@ -32,6 +32,9 @@ public class ProofScriptDebugger extends Application {
     @Override
     public void start(Stage primaryStage) {
         Locale.setDefault(Locale.ENGLISH);
+
+        
+
         try {
             FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
             Parent root = fxmlLoader.load();
@@ -50,7 +53,7 @@ public class ProofScriptDebugger extends Application {
             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"));
+            logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
 
         } catch (IOException e) {
             e.printStackTrace();

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

@@ -34,6 +34,8 @@ import javafx.scene.layout.Priority;
 import javafx.stage.FileChooser;
 import org.antlr.v4.runtime.RecognitionException;
 import org.apache.commons.io.FileUtils;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 
 import java.io.File;
 import java.io.IOException;
@@ -53,6 +55,8 @@ import java.util.concurrent.Executors;
  * @author Alexander Weigl
  */
 public class DebuggerMainWindowController implements Initializable {
+    private static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class);
+
     private final PuppetMaster blocker = new PuppetMaster();
     private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
     private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
@@ -171,7 +175,7 @@ public class DebuggerMainWindowController implements Initializable {
         model.chosenContractProperty().addListener(o -> {
             IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
             javaSourceCode.clear();
-            javaSourceCode.getMarkedLines().clear();
+            javaSourceCode.getLineToClass().clear();
             StringWriter writer = new StringWriter();
             ProgramPrinter pp = new ProgramPrinter(writer);
             try {

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

+package edu.kit.formal.gui.controls;
+
+import javafx.beans.property.BooleanProperty;
+import javafx.beans.property.MapProperty;
+import javafx.beans.property.SimpleBooleanProperty;
+import javafx.beans.property.SimpleMapProperty;
+import javafx.collections.FXCollections;
+import javafx.collections.ObservableMap;
+import org.antlr.v4.runtime.Token;
+import org.fxmisc.richtext.CodeArea;
+
+import java.util.Collections;
+import java.util.Map;
+
+/**
+ * A code area with support for line highlightning.
+ * Created by weigl on 10.06.2017.
+ *
+ * @author Alexander Weigl
+ */
+public class BaseCodeArea extends CodeArea {
+    protected MapProperty<Integer, String> lineToClass = new SimpleMapProperty<>(FXCollections.observableHashMap());
+    protected BooleanProperty enableLineHighlighting = new SimpleBooleanProperty();
+    protected BooleanProperty enableCurrentLineHighlighting = new SimpleBooleanProperty();
+
+    public BaseCodeArea() {
+        init();
+    }
+
+    public BaseCodeArea(String text) {
+        super(text);
+        init();
+    }
+
+    private void init() {
+
+    }
+
+    public void setText(String text) {
+        replaceText(text);
+    }
+
+    protected void highlightLines() {
+        if (enableLineHighlighting.get() || enableCurrentLineHighlighting.get()) {
+            LineMapping lm = new LineMapping(getText());
+
+            if (enableLineHighlighting.get()) {
+                for (Map.Entry<Integer, String> entry : lineToClass.entrySet()) {
+                    hightlightLine(lm, entry.getKey(), entry.getValue());
+                }
+            }
+
+            if (enableCurrentLineHighlighting.get()) {
+                int caret = getCaretPosition();
+                hightlightLine(lm, lm.getLine(caret), "current-line");
+            }
+        }
+    }
+
+    public void jumpTo(Token token) {
+        //token.getStartIndex();
+    }
+
+    protected void hightlightLine(LineMapping lm, int line, String clazz) {
+        final int start = lm.getLineStart(line);
+        final int end = lm.getLineEnd(line);
+        setStyle(start, end, Collections.singleton(clazz));
+    }
+
+    public ObservableMap<Integer, String> getLineToClass() {
+        return lineToClass.get();
+    }
+
+    public MapProperty<Integer, String> lineToClassProperty() {
+        return lineToClass;
+    }
+
+    public void setLineToClass(ObservableMap<Integer, String> lineToClass) {
+        this.lineToClass.set(lineToClass);
+    }
+
+    public boolean isEnableLineHighlighting() {
+        return enableLineHighlighting.get();
+    }
+
+    public BooleanProperty enableLineHighlightingProperty() {
+        return enableLineHighlighting;
+    }
+
+    public void setEnableLineHighlighting(boolean enableLineHighlighting) {
+        this.enableLineHighlighting.set(enableLineHighlighting);
+    }
+
+    public boolean isEnableCurrentLineHighlighting() {
+        return enableCurrentLineHighlighting.get();
+    }
+
+    public BooleanProperty enableCurrentLineHighlightingProperty() {
+        return enableCurrentLineHighlighting;
+    }
+
+    public void setEnableCurrentLineHighlighting(boolean enableCurrentLineHighlighting) {
+        this.enableCurrentLineHighlighting.set(enableCurrentLineHighlighting);
+    }
+}

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

@@ -2,6 +2,7 @@ package edu.kit.formal.gui.controls;
 
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
+import edu.kit.formal.gui.controller.DebuggerMainWindowController;
 import javafx.beans.binding.StringBinding;
 import javafx.beans.property.ListProperty;
 import javafx.beans.property.SimpleListProperty;
@@ -21,18 +22,31 @@ import javafx.scene.input.MouseEvent;
 import javafx.scene.layout.BorderPane;
 import javafx.stage.Modality;
 import javafx.util.Callback;
+import org.apache.logging.log4j.Level;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
+import org.apache.logging.log4j.core.Appender;
+import org.apache.logging.log4j.core.Filter;
+import org.apache.logging.log4j.core.Layout;
+import org.apache.logging.log4j.core.LogEvent;
+import org.apache.logging.log4j.core.appender.AbstractAppender;
+import org.apache.logging.log4j.core.appender.ConsoleAppender;
+import org.apache.logging.log4j.core.layout.PatternLayout;
 import org.controlsfx.control.StatusBar;
 
 import java.io.PrintWriter;
+import java.io.Serializable;
 import java.io.StringWriter;
 import java.util.Date;
 import java.util.LinkedList;
-import java.util.logging.*;
+import java.util.logging.LogRecord;
 
 /**
  * Created by weigl on 09.06.2017.
  */
 public class DebuggerStatusBar extends StatusBar {
+    private static final Logger LOGGER = LogManager.getLogger(DebuggerStatusBar.class);
+
     private Label lblCurrentNodes = new Label("#nodes: %s");
     private ProgressIndicator progressIndicator = new ProgressIndicator();
     private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
@@ -40,6 +54,7 @@ public class DebuggerStatusBar extends StatusBar {
         publishMessage(((Control) event.getTarget()).getTooltip().getText());
     };
 
+
     private final ContextMenu contextMenu = createContextMenu();
     private final Dialog<Void> loggerDialog = createDialog();
 
@@ -56,24 +71,21 @@ public class DebuggerStatusBar extends StatusBar {
                 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 {
+    private final Appender loggerHandler = createAppender();
 
-        }
-    };
+    private Appender createAppender() {
+        PatternLayout layout = PatternLayout.createDefaultLayout();
+        return new AbstractAppender("", null, layout) {
+            @Override
+            public void append(LogEvent event) {
+                publishMessage(event.getMessage().getFormattedMessage());
+            }
+        };
+    }
 
     public void publishMessage(String format, Object... args) {
         String msg = String.format(format, args);
@@ -91,14 +103,14 @@ public class DebuggerStatusBar extends StatusBar {
     }
 
     public void listenOnField(Logger logger) {
-        logger.addHandler(loggerHandler);
-        logger.addHandler(logCatchHandler);
-
+        org.apache.logging.log4j.core.Logger plogger = ((org.apache.logging.log4j.core.Logger) logger); // Bypassing the public API
+        plogger.addAppender(loggerHandler);
+        plogger.addAppender(logCatchHandler);
         logger.info("Listener added");
     }
 
     public void listenOnField(String loggerCategory) {
-        listenOnField(Logger.getLogger(loggerCategory));
+        listenOnField(LogManager.getLogger(loggerCategory));
     }
 
     public void indicateProgress() {
@@ -123,20 +135,20 @@ public class DebuggerStatusBar extends StatusBar {
     }
 
     public Dialog<Void> createDialog() {
-        final TableView<LogRecord> recordView = new TableView<>(logCatchHandler.recordsProperty());
+        final TableView<LogEvent> 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<LogEvent, Date> dateColumn = new TableColumn<>("Date");
+        TableColumn<LogEvent, Level> levelColumn = new TableColumn<>("Level");
         //TableColumn<LogRecord, String> classColumn = new TableColumn<>("Class");
-        TableColumn<LogRecord, String> messageColumn = new TableColumn<>("Message");
+        TableColumn<LogEvent, String> messageColumn = new TableColumn<>("Message");
 
         recordView.getColumns().setAll(dateColumn, levelColumn, messageColumn);
 
 
         dateColumn.setCellValueFactory(
-                param -> new SimpleObjectProperty<>(new Date(param.getValue().getMillis())
+                param -> new SimpleObjectProperty<>(new Date(param.getValue().getTimeMillis())
                 ));
 
         levelColumn.setCellValueFactory(
@@ -145,7 +157,8 @@ public class DebuggerStatusBar extends StatusBar {
 
         messageColumn.setCellValueFactory(
                 param -> {
-                    String s = formatter.formatMessage(param.getValue());
+                    return new SimpleStringProperty(param.getValue().getMessage().getFormattedMessage());
+                    /*String s = formatter.formatMessage(param.getValue());
                     if (param.getValue().getThrown() != null) {
                         StringWriter sw = new StringWriter();
                         PrintWriter pw = new PrintWriter(sw);
@@ -154,7 +167,7 @@ public class DebuggerStatusBar extends StatusBar {
                         pw.close();
                         s += "\n" + sw.toString();
                     }
-                    return new SimpleStringProperty(s);
+                    return new SimpleStringProperty(s);*/
                 }
         );
 
@@ -169,39 +182,34 @@ public class DebuggerStatusBar extends StatusBar {
         return dialog;
     }
 
-    public static class LogCatchHandlerFX extends Handler {
-        private ListProperty<LogRecord> records = new SimpleListProperty<>(FXCollections.observableList(
+    public static class LogCatchHandlerFX extends AbstractAppender {
+        private ListProperty<LogEvent> 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);
+        protected LogCatchHandlerFX() {
+            super("LogCatchHandlerFX", null, PatternLayout.createDefaultLayout());
         }
 
         @Override
-        public void flush() {
-
+        public void append(LogEvent event) {
+            records.add(event);
+            while (records.size() > maxRecords)
+                records.remove(0);
         }
 
-        @Override
-        public void close() throws SecurityException {
-
-        }
 
-        public ObservableList<LogRecord> getRecords() {
+        public ObservableList<LogEvent> getRecords() {
             return records.get();
         }
 
-        public ListProperty<LogRecord> recordsProperty() {
+        public ListProperty<LogEvent> recordsProperty() {
             return records;
         }
 
-        public void setRecords(ObservableList<LogRecord> records) {
+        public void setRecords(ObservableList<LogEvent> records) {
             this.records.set(records);
         }
 
@@ -213,25 +221,6 @@ public class DebuggerStatusBar extends StatusBar {
             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/java/edu/kit/formal/gui/controls/JavaArea.java

@@ -16,11 +16,8 @@ import java.util.Set;
  * @author Alexander Weigl
  * @version 1 (03.06.17)
  */
-public class JavaArea extends CodeArea {
-    private static final Set<String> HIGHLIGHT_LINE_CLAZZ = Collections.singleton("hl-line");
+public class JavaArea extends BaseCodeArea {
     private ANTLR4LexerHighlighter highlighter = new ANTLR4LexerHighlighter((s) -> new Java8Lexer(CharStreams.fromString(s)));
-    private SimpleSetProperty<Integer> markedLines = new SimpleSetProperty<>(this, "markedLines",
-            FXCollections.observableSet());
 
     public JavaArea() {
         init();
@@ -36,36 +33,13 @@ public class JavaArea extends CodeArea {
         setParagraphGraphicFactory(LineNumberFactory.get(this));
         setWrapText(true);
         getStyleClass().add("java-area");
-
-        //getStylesheets().add(getClass().getResource("java-keywords.css").toExternalForm());
-        getStyleClass().add("java-area");
         textProperty().addListener(
                 (a, b, c) -> updateView());
-        markedLines.addListener((SetChangeListener<Integer>) change -> updateView());
     }
 
     private void updateView() {
         clearStyle(0, getText().length());
         setStyleSpans(0, highlighter.highlight(textProperty().getValue()));
-        LineMapping lmap = new LineMapping(textProperty().getValue());
-        for (Integer line : markedLines) {
-            int start = lmap.getLineStart(line);
-            int end = lmap.getLineEnd(line);
-            setStyle(start, end, HIGHLIGHT_LINE_CLAZZ);
-        }
-
-
-    }
-
-    public ObservableSet<Integer> getMarkedLines() {
-        return markedLines.get();
-    }
-
-    public SimpleSetProperty<Integer> markedLinesProperty() {
-        return markedLines;
-    }
-
-    public void setMarkedLines(ObservableSet<Integer> markedLines) {
-        this.markedLines.set(markedLines);
+        highlightLines();
     }
 }

src/main/java/edu/kit/formal/interpreter/HistoryListener.java

@@ -6,6 +6,7 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 
+import java.util.ArrayList;
 import java.util.LinkedList;
 import java.util.List;
 
@@ -29,5 +30,40 @@ public class HistoryListener extends DefaultASTVisitor<Void> {
         return null;
     }
 
+    public State getLastStateFor(ASTNode node) {
+        int index = queueNode.lastIndexOf(node);
+        if (index == -1)
+            return null;
+        return queueState.get(index);
+    }
+
+    public List<State> getStates(ASTNode node) {
+        ArrayList<State> list = new ArrayList<>(queueState.size());
+        for (int i = 0; i < queueNode.size(); i++) {
+            if (node.equals(queueNode.get(i))) {
+                list.add(queueState.get(i));
+            }
+        }
+        return list;
+    }
+
+
+    public List<State> getStates(int caret) {
+        ArrayList<State> list = new ArrayList<>(queueState.size());
+        int nearestFoundCaret = -1;
+
+        for (int i = 0; i < queueNode.size(); i++) {
+            int currentPos = queueNode.get(i).getRuleCtx().start.getStartIndex();
+            if (currentPos > nearestFoundCaret && currentPos <= caret) {
+                list.clear();
+                nearestFoundCaret = currentPos;
+            }
+
+            if (currentPos == nearestFoundCaret) {
+                list.add(queueState.get(i));
+            }
+        }
+        return list;
+    }
 
 }

src/main/resources/DebuggerMain.fxml

@@ -168,7 +168,7 @@
                         <SeparatorMenuItem/>
                         <MenuItem onAction="#saveScript" text="Save Script"/>
                         <MenuItem onAction="#saveAsScript" text="Save Script As ..."/>
-                        <MenuItem onAction="#saveProof"/>
+                        <MenuItem onAction="#saveProof" text="Save Proof"/>
                         <MenuItem fx:id="closeMenuItem" onAction="#closeProgram" text="Close"/>
                     </items>
                 </Menu>

src/main/resources/log4j2.properties

+# Root logger option
+log4j.rootLogger=INFO, stdout
+
+# Direct log messages to stdout
+log4j.appender.stdout=org.apache.log4j.ConsoleAppender
+log4j.appender.stdout.Target=System.err
+log4j.appender.stdout.layout=org.apache.log4j.PatternLayout
+log4j.appender.stdout.layout.ConversionPattern=%d{yyyy-MM-dd HH:mm:ss} %-5p %c{1}:%L - %m%n