clean up and syntaxhighlightning

src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4

@@ -125,11 +125,11 @@ callStmt
 */
 
 //LEXER Rules
-WS : [ \t\n\r]+ -> skip ;
+WS : [ \t\n\r]+ -> channel(HIDDEN) ;
 
 //comments, allowing nesting.
-SINGLE_LINE_COMMENT : '//' ~[\r\n]* -> skip;
-MULTI_LINE_COMMENT  : '/*' (MULTI_LINE_COMMENT|.)*? '*/' -> skip;
+SINGLE_LINE_COMMENT : '//' ~[\r\n]* -> channel(HIDDEN);
+MULTI_LINE_COMMENT  : '/*' (MULTI_LINE_COMMENT|.)*? '*/' -> channel(HIDDEN);
 
 CASES: 'cases';
 CASE: 'case';

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

 package edu.kit.formal.gui.controller;
 
 import de.uka.ilkd.key.speclang.Contract;
+import edu.kit.formal.gui.controls.ScriptArea;
 import edu.kit.formal.gui.model.RootModel;
 import edu.kit.formal.interpreter.KeYProofFacade;
 import edu.kit.formal.interpreter.data.GoalNode;
@@ -79,7 +80,7 @@ public class DebuggerMainWindowController implements Initializable {
      *      GoalView
      * **********************************************************************************************************/
     @FXML
-    ListGoalView goalView;
+    ListView goalView;
     private ExecutorService executorService = null;
 
 
@@ -236,13 +237,7 @@ public class DebuggerMainWindowController implements Initializable {
      */
     public void init() {
         facade = new KeYProofFacade(this.model);
-        scriptArea.setRootModel(this.model);
-        scriptArea.init();
-        goalView.setRootModel(this.model);
-        goalView.init();
-        // create and assign the flow
         cls = new ContractLoaderService();
-
     }
 
 

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

-package edu.kit.formal.gui.controller;
-
-import edu.kit.formal.gui.model.RootModel;
-import javafx.beans.property.SimpleObjectProperty;
-import javafx.beans.value.ObservableValue;
-import lombok.Getter;
-import org.fxmisc.richtext.CodeArea;
-import org.fxmisc.richtext.LineNumberFactory;
-
-/**
- * Created by sarah on 5/27/17.
- */
-public class ScriptArea extends CodeArea {
-    @Getter
-    private RootModel rootModel;
-
-    public void setRootModel(RootModel rootModel) {
-        this.rootModel = rootModel;
-
-        ObservableValue<String> stringObservableValue = this.textProperty();
-        SimpleObjectProperty<String> stringSimpleObjectProperty = this.rootModel.currentScriptProperty();
-        stringSimpleObjectProperty.bind(stringObservableValue);
-        //  rootModel.currentScriptProperty().addListener((prop, old, cur) -> {clear(); insertText(0, cur););});
-    }
-
-    public void init() {
-        this.setWrapText(true);
-        this.setParagraphGraphicFactory(LineNumberFactory.get(this));
-
-        this.setDefaultText();
-    }
-
-    private void setDefaultText() {
-        this.appendText("script test(){\n\n}");
-    }
-
-
-}

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

+package edu.kit.formal.gui.controls;
+
+import org.antlr.v4.runtime.Lexer;
+import org.antlr.v4.runtime.Token;
+import org.fxmisc.richtext.StyleSpans;
+import org.fxmisc.richtext.StyleSpansBuilder;
+
+import java.util.Collection;
+import java.util.Collections;
+import java.util.List;
+import java.util.Set;
+import java.util.function.Function;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (03.06.17)
+ */
+public class ANTLR4LexerHighlighter {
+    private final Function<String, Lexer> factory;
+
+    public ANTLR4LexerHighlighter(Function<String, Lexer> factory) {
+        this.factory = factory;
+    }
+
+
+    public StyleSpans<Collection<String>> highlight(String sourcecode) {
+        Lexer lexer = factory.apply(sourcecode);
+        StyleSpansBuilder<Collection<String>> spansBuilder = new StyleSpansBuilder<>();
+        try {
+            List<? extends Token> tokens = lexer.getAllTokens();
+            if (tokens.size() == 0)
+                spansBuilder.add(Collections.emptyList(), 0);
+
+            tokens.forEach(token -> {
+                String clazz = lexer.getVocabulary().getSymbolicName(token.getType());
+                Set<String> clazzes = Collections.singleton(clazz);
+                //System.out.format("%25s %s%n", clazz, token.getText());
+                spansBuilder.add(
+                        clazzes,
+                        token.getText().length());
+            });
+
+            return spansBuilder.create();
+        } catch (StringIndexOutOfBoundsException e) {
+            e.printStackTrace();
+        }
+        return null;
+    }
+}

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

+package edu.kit.formal.gui.controls;
+
+import org.fxmisc.richtext.CodeArea;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (03.06.17)
+ */
+public class JavaArea extends CodeArea {
+
+
+    public JavaArea() {
+        init();
+    }
+
+    public JavaArea(String text) {
+        super(text);
+        init();
+    }
+
+    private void init() {
+
+
+
+    }
+}

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

+package edu.kit.formal.gui.controls;
+
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
+import edu.kit.formal.proofscriptparser.Facade;
+import edu.kit.formal.proofscriptparser.ScriptLanguageLexer;
+import edu.kit.formal.proofscriptparser.lint.LintProblem;
+import edu.kit.formal.proofscriptparser.lint.LinterStrategy;
+import javafx.beans.property.SimpleListProperty;
+import javafx.beans.property.SimpleObjectProperty;
+import javafx.collections.FXCollections;
+import javafx.collections.ObservableList;
+import javafx.collections.ObservableSet;
+import javafx.geometry.Insets;
+import javafx.scene.Node;
+import javafx.scene.control.Label;
+import javafx.scene.layout.Background;
+import javafx.scene.layout.BackgroundFill;
+import javafx.scene.layout.HBox;
+import javafx.scene.paint.Color;
+import javafx.scene.paint.Paint;
+import javafx.scene.text.Font;
+import javafx.scene.text.FontPosture;
+import org.antlr.v4.runtime.CharStreams;
+import org.antlr.v4.runtime.Token;
+import org.fxmisc.richtext.CodeArea;
+import org.reactfx.collection.LiveList;
+import org.reactfx.value.Val;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
+import java.util.function.IntFunction;
+
+/**
+ * Created by sarah on 5/27/17.
+ */
+public class ScriptArea extends CodeArea {
+    private ObservableSet<Integer> markedLines = FXCollections.observableSet();
+    private GutterFactory gutter;
+    private ANTLR4LexerHighlighter highlighter;
+
+    public ScriptArea() {
+        init();
+    }
+
+    private void init() {
+        this.setWrapText(true);
+        gutter = new GutterFactory();
+        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");
+        textProperty().addListener((prop, oldValue, newValue) -> {
+            clearStyle(0, newValue.length());
+            setStyleSpans(0, highlighter.highlight(newValue));
+            highlightProblems();
+        });
+               /* .successionEnds(Duration.ofMillis(100))
+                .hook(collectionRichTextChange -> this.getUndoManager().mark())
+                .supplyTask(this::computeHighlightingAsync).awaitLatest(richChanges())
+                .filterMap(t -> {
+                    if (t.isSuccess()) {
+                        return Optional.of(t.get());
+                    } else {
+                        t.getFailure().printStackTrace();
+                        return Optional.empty();
+                    }
+                }).subscribe(s -> setStyleSpans(0, s));*/
+    }
+
+    private void highlightProblems() {
+        LinterStrategy ls = LinterStrategy.getDefaultLinter();
+        List<LintProblem> pl = ls.check(Facade.getAST(CharStreams.fromString(getText())));
+
+        List<Integer> newlines = new ArrayList<>();
+        newlines.add(0);
+        char[] chars = getText().toCharArray();
+        for (int i = 0; i < chars.length; i++) {
+            if (chars[i] == '\n') {
+                newlines.add(i);
+            }
+        }
+
+        for (LintProblem p : pl) {
+            for (Token tok : p.getMarkTokens()) {
+                setStyle(tok.getStartIndex(),
+                        tok.getStopIndex()+1, Collections.singleton("problem"));
+            }
+        }
+    }
+
+    public void setText(String text) {
+        insertText(0, text);
+    }
+
+    private void onLineClicked(int idx) {
+        if (markedLines.contains(idx)) {
+            markedLines.remove(idx);
+            gutter.lineAnnotations.get(idx).set(null);
+        } else {
+            markedLines.add(idx);
+            gutter.lineAnnotations.get(idx).set(
+                    new MaterialDesignIconView(MaterialDesignIcon.STOP_CIRCLE_OUTLINE)
+            );
+        }
+    }
+
+
+    public class GutterFactory implements IntFunction<Node> {
+        private Insets defaultInsets = new Insets(0.0, 5.0, 0.0, 5.0);
+        private Paint defaultTextFill = Color.web("#666");
+        private Font defaultFont = Font.font("monospace", FontPosture.ITALIC, 13);
+        private final Background defaultBackground =
+                new Background(new BackgroundFill(Color.web("#ddd"), null, null));
+
+        private final Val<Integer> nParagraphs;
+
+        private ObservableList<SimpleObjectProperty<Node>> lineAnnotations = new SimpleListProperty<>(FXCollections.observableArrayList());
+
+
+        public GutterFactory() {
+            nParagraphs = LiveList.sizeOf(getParagraphs());
+
+            for (int i = 0; i < 100; i++) {
+                lineAnnotations.add(new SimpleObjectProperty<>());
+            }
+
+            // Update the gutter.
+            // If a line is deleted, delete also the image entry for this line
+            nParagraphs.addInvalidationObserver((n) -> {
+                int diff = lineAnnotations.size() - n;
+            /*if (diff < 0) {
+                for (int i = 0; i < diff; i++) {
+                    lineAnnotations.add(new SimpleObjectProperty<>());
+                }
+            }*/
+                if (diff > 0) {
+                    lineAnnotations.remove(n, lineAnnotations.size());
+                }
+            });
+
+        }
+
+
+        @Override
+        public Node apply(int idx) {
+            Val<String> formatted = nParagraphs.map(n -> format(idx + 1, n));
+
+            Label lineNo = new Label();
+            // bind label's text to a Val that stops observing area's paragraphs
+            // when lineNo is removed from scene
+            lineNo.textProperty().bind(formatted.conditionOnShowing(lineNo));
+
+
+            if (lineAnnotations.size() <= idx) {
+                for (int i = lineAnnotations.size(); i < idx + 1; i++) {
+                    lineAnnotations.add(new SimpleObjectProperty<>());
+                }
+            }
+
+            Label labelInfo = new Label();
+            labelInfo.setMinHeight(12);
+            labelInfo.setMinWidth(12);
+            SimpleObjectProperty<Node> annotation = lineAnnotations.get(idx);
+            annotation.addListener((a, b, c) -> {
+                labelInfo.setGraphic(c);
+            });
+            labelInfo.setGraphic(annotation.get());
+
+            HBox hbox = new HBox(lineNo, labelInfo);
+            hbox.setOnMouseClicked((mevent) -> onLineClicked(idx));
+
+            lineNo.setFont(defaultFont);
+            labelInfo.setFont(defaultFont);
+            hbox.setBackground(defaultBackground);
+            lineNo.setTextFill(defaultTextFill);
+            hbox.setPadding(defaultInsets);
+            hbox.getStyleClass().add("lineno");
+            return hbox;
+        }
+
+        private String format(int x, int max) {
+            int digits = (int) Math.floor(Math.log10(max)) + 1;
+            return String.format("%" + digits + "d", x);
+        }
+
+    }
+}
\ No newline at end of file

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

+package edu.kit.formal.gui.controls;
+
+import org.fxmisc.richtext.CodeArea;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (03.06.17)
+ */
+public class SequentView extends CodeArea {
+}

src/main/resources/DebuggerMain.fxml

 <?xml version="1.0" encoding="UTF-8"?>
 
-
 <?import de.jensd.fx.glyphs.materialdesignicons.*?>
-<?import edu.kit.formal.gui.controller.ListGoalView?>
-<?import edu.kit.formal.gui.controller.ScriptArea?>
+<?import edu.kit.formal.gui.controls.ScriptArea?>
+<?import edu.kit.formal.gui.controls.JavaArea?>
+<?import edu.kit.formal.gui.controls.SequentView?>
+<?import javafx.geometry.Insets?>
 <?import javafx.scene.control.*?>
 <?import javafx.scene.layout.*?>
-<?import java.lang.Boolean?>
-
-<Pane xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" maxHeight="-Infinity" maxWidth="-Infinity"
-      minHeight="-Infinity"
-      minWidth="-Infinity" prefHeight="400.0" prefWidth="600.0"
-      xmlns="http://javafx.com/javafx/8.0.102-ea"
-      fx:controller="edu.kit.formal.gui.controller.DebuggerMainWindowController">
 
-    <!--
-    <fx:define>
-        <Boolean fx:id="disableDebuggingButtons" fx:value="true" />
-    </fx:define>-->
 
-    <children>
+<BorderPane fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112" xmlns:fx="http://javafx.com/fxml/1"
+            fx:controller="edu.kit.formal.gui.controller.DebuggerMainWindowController">
+    <center>
         <SplitPane fx:id="splitPane" dividerPositions="0.5" layoutY="29.0" prefHeight="371.0" prefWidth="600.0">
             <items>
-                <AnchorPane minHeight="0.0" minWidth="0.0" prefHeight="366.0" prefWidth="175.0">
-                    <VBox prefHeight="369.0" prefWidth="295.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0"
-                          AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0">
-                        <children>
-                            <ToolBar fx:id="toolbar" prefHeight="40.0" prefWidth="200.0">
-                                <items>
-                                    <Button fx:id="buttonStartInterpreter" onAction="#executeScript">
-                                        <graphic>
-                                            <MaterialDesignIconView glyphName="PLAY" size="24.0"/>
-                                        </graphic>
-                                        <tooltip>
-                                            <Tooltip text="Execute Script"/>
-                                        </tooltip>
-                                    </Button>
-                                    <Button fx:id="startDebugMode" onAction="#changeToDebugMode">
-                                        <graphic>
-                                            <MaterialDesignIconView glyphName="PLAY_PAUSE" size="24.0"/>
-                                        </graphic>
-                                        <tooltip>
-                                            <Tooltip text="Change to Debug Mode"/>
-                                        </tooltip>
-                                    </Button>
+                <VBox>
+                    <children>
+                        <ToolBar fx:id="toolbar">
+                            <items>
+                                <Button fx:id="buttonStartInterpreter" onAction="#executeScript">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="PLAY" size="24.0"/>
+                                    </graphic>
+                                    <tooltip>
+                                        <Tooltip text="Execute Script"/>
+                                    </tooltip>
+                                </Button>
+                                <Button fx:id="startDebugMode" onAction="#changeToDebugMode">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="PLAY_PAUSE" size="24.0"/>
+                                    </graphic>
+                                    <tooltip>
+                                        <Tooltip text="Change to Debug Mode"/>
+                                    </tooltip>
+                                </Button>
 
-                                    <Separator/>
+                                <Separator/>
 
-                                    <Button disable="${! controller.debugMode}">
-                                        <graphic>
-                                            <MaterialDesignIconView glyphName="DEBUG_STEP_INTO" size="24.0"/>
-                                        </graphic>
-                                    </Button>
+                                <Button disable="${! controller.debugMode}">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="DEBUG_STEP_INTO" size="24.0"/>
+                                    </graphic>
+                                </Button>
 
-                                    <Button disable="${! controller.debugMode}">
-                                        <graphic>
-                                            <MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0"/>
-                                        </graphic>
-                                    </Button>
+                                <Button disable="${! controller.debugMode}">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="DEBUG_STEP_OVER" size="24.0"/>
+                                    </graphic>
+                                </Button>
 
-                                    <Button disable="${! controller.debugMode}">
-                                        <graphic>
-                                            <MaterialDesignIconView glyphName="DEBUG_STEP_OUT" size="24.0"/>
-                                        </graphic>
-                                    </Button>
+                                <Button disable="${! controller.debugMode}">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="DEBUG_STEP_OUT" size="24.0"/>
+                                    </graphic>
+                                </Button>
 
-                                    <Button disable="${! controller.debugMode}">
-                                        <graphic>
-                                            <MaterialDesignIconView glyphName="STOP" size="24.0"/>
-                                        </graphic>
-                                    </Button>
-                                </items>
-                            </ToolBar>
-                            <ScrollPane fx:id="scrollPaneCode" prefHeight="369.0" prefWidth="295.0"
-                                        AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0"
-                                        AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0">
-                                <content>
-                                    <ScriptArea fx:id="scriptArea" prefHeight="369.0" prefWidth="295.0"
-                                                AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0"
-                                                AnchorPane.rightAnchor="0.0" AnchorPane.topAnchor="0.0"
-                                                SplitPane.resizableWithParent="true"/>
-                                </content>
-                            </ScrollPane>
-                        </children>
-                    </VBox>
-                </AnchorPane>
-                <AnchorPane minHeight="0.0" minWidth="0.0" prefHeight="160.0" prefWidth="100.0">
-                    <StackPane AnchorPane.topAnchor="0.0" AnchorPane.bottomAnchor="0.0" AnchorPane.leftAnchor="0.0"
-                               AnchorPane.rightAnchor="0.0">
-                        <ListGoalView fx:id="goalView" prefHeight="369.0" prefWidth="295.0"
-                                      AnchorPane.bottomAnchor="0.0"
-                                      AnchorPane.leftAnchor="0.0" AnchorPane.rightAnchor="0.0"
-                                      AnchorPane.topAnchor="0.0"
-                                      SplitPane.resizableWithParent="true">
-                            <!--<children>
-                                <ListView fx:id="listOfGoalsView" prefHeight="200.0" prefWidth="200.0"/>
-                                <TextArea fx:id="goalNodeView" prefHeight="200.0" prefWidth="200.0"/>
-                            </children>-->
-                        </ListGoalView>
-                    </StackPane>
-                </AnchorPane>
+                                <Button disable="${! controller.debugMode}">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="STOP" size="24.0"/>
+                                    </graphic>
+                                </Button>
+                            </items>
+                        </ToolBar>
+                        <ScriptArea fx:id="scriptArea" VBox.vgrow="ALWAYS"/>
+                    </children>
+                </VBox>
+                <BorderPane SplitPane.resizableWithParent="true">
+                    <center>
+                        <Accordion>
+                            <padding>
+                                <Insets top="5" left="5" right="5" bottom="5"/>
+                            </padding>
+                            <panes>
+                                <TitledPane text="Current Goals:" VBox.vgrow="ALWAYS">
+                                    <ListView fx:id="goalView" VBox.vgrow="ALWAYS"/>
+                                </TitledPane>
+                                <TitledPane text="Sequent">
+                                    <SequentView fx:id="sequentView" VBox.vgrow="ALWAYS"/>
+                                </TitledPane>
+                                <TitledPane text="Source Code">
+                                    <JavaArea fx:id="javaSourceCode"/>
+                                </TitledPane>
+                            </panes>
+                        </Accordion>
+                    </center>
+                </BorderPane>
             </items>
         </SplitPane>
-        <MenuBar fx:id="menuBar" prefHeight="29.0" prefWidth="600.0">
+    </center>
+    <top>
+        <MenuBar fx:id="menuBar">
             <menus>
                 <Menu fx:id="fileMenu" mnemonicParsing="false" text="File">
                     <items>
-                        <MenuItem fx:id="openScriptFileMenuItem" mnemonicParsing="false" onAction="#openScript"
-                                  text="Open Script"/>
-                        <MenuItem fx:id="loadKeYFileMenuItem" mnemonicParsing="false" onAction="#loadKeYFile"
-                                  text="Load KeY File"/>
-                        <MenuItem fx:id="loadJavaFileMenuItem" mnemonicParsing="false" onAction="#loadJavaFile"
-                                  text="Load Java File"/>
+                        <MenuItem fx:id="openScriptFileMenuItem" onAction="#openScript" text="Open Script"/>
+                        <MenuItem fx:id="loadKeYFileMenuItem" onAction="#loadKeYFile" text="Load KeY File"/>
+                        <MenuItem fx:id="loadJavaFileMenuItem" onAction="#loadJavaFile" text="Load Java File"/>
 
                         <MenuItem fx:id="closeMenuItem" mnemonicParsing="false" onAction="#closeProgram" text="Close"/>
                     </items>
@@ -128,5 +112,5 @@
                 </Menu>
             </menus>
         </MenuBar>
-    </children>
-</Pane>
+    </top>
+</BorderPane>

src/main/resources/edu/kit/formal/gui/controls/script-keywords.css

+.FOREACH, .CASES, .CASE, .THEONLY, .SCRIPT, .USING,
+.REPEAT {
+    -fx-fill: darkgreen;
+    -fx-font-weight: bold;
+}
+
+.MATCH, .PLUS, .MINUS {
+    -fx-font-weight: bold;
+    -fx-fill: darkred;
+}
+
+.INDENT, .DEDENT, .COLON, .ASSIGN {
+    -fx-font-weight: bold;
+    -fx-fill: blueviolet;
+}
+
+.script-area {
+    -fx-font-size: 14pt;
+    -fx-font-family: "Fira Code Medium";
+}
+
+.INTEGER_LITERAL {
+    -fx-fill: blue;
+}
+
+.TERM_LITERAL {
+    -fx-fill: green;
+    -fx-font-smoothing-type: lcd;
+}
+
+.STRING_LITERAL {
+    -fx-fill: olivedrab;
+}
+
+.SINGLE_LINE_COMMENT, .MULTI_LINE_COMMENT {
+    -fx-fill: dimgrey;
+    -fx-font-family: "Fira Code Light";
+}
+
+.IDENTIFIER {
+    -fx-fill: darkslateblue;
+    -fx-font-weight: bold;
+}
+
+.problem {