Proposing a more flexible lexing framework (#3537)

Author: mattulbrich

key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java

@@ -1252,7 +1252,7 @@ public StrategyFactory getActiveStrategyFactory() {
      * @return null or the previous data
      * @see #register(Object, Class)
      */
-    public <T> T lookup(Class<T> service) {
+    public <T> @Nullable T lookup(Class<T> service) {
         try {
             if (userData == null) {
                 return null;

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLUtils.java

@@ -129,6 +129,15 @@ private boolean consume(String str) {
         return false;
     }
 
+    /**
+     * Given a string of conditions of a JML comment, that method decides whether the conditions are
+     * met.
+     *
+     * @param foundKeys a string of conditions, e.g., {@code "+key+esc-float"}. Should not contain
+     *        whitespaces.
+     * @return true whether the given conditions are met and the comment should be considered as
+     *         active.
+     */
     public boolean isActiveJmlSpec(String foundKeys) {
         if (foundKeys.isEmpty()) {
             // a JML annotation with no keys is always included,

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlMarkerDecision.java

@@ -0,0 +1,35 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.speclang.jml;
+
+import de.uka.ilkd.key.speclang.njml.JmlMarkerDecision;
+
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+
+public class JmlMarkerDecisionTest {
+
+    @Test
+    public void testIsActiveJmlSpec() {
+        JmlMarkerDecision dec = new JmlMarkerDecision(null);
+        assertFalse(dec.isActiveJmlSpec("+ESC"));
+        assertFalse(dec.isActiveJmlSpec("+a+b+c"));
+        assertFalse(dec.isActiveJmlSpec("+a"));
+        assertFalse(dec.isActiveJmlSpec("-key+key"));
+        assertFalse(dec.isActiveJmlSpec("-"));
+        assertFalse(dec.isActiveJmlSpec("+"));
+        assertFalse(dec.isActiveJmlSpec("+ke y"));
+
+        assertTrue(dec.isActiveJmlSpec("+key-a b"));
+        assertTrue(dec.isActiveJmlSpec("+a+key"));
+        assertTrue(dec.isActiveJmlSpec("+key"));
+        assertTrue(dec.isActiveJmlSpec("+key"));
+        assertTrue(dec.isActiveJmlSpec("+KEY"));
+        assertTrue(dec.isActiveJmlSpec("+KEY"));
+        assertTrue(dec.isActiveJmlSpec(""));
+    }
+}

key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JMLUtilsTest.java

@@ -25,7 +25,9 @@
 import de.uka.ilkd.key.gui.actions.EditSourceFileAction;
 import de.uka.ilkd.key.gui.actions.SendFeedbackAction;
 import de.uka.ilkd.key.gui.configuration.Config;
-import de.uka.ilkd.key.gui.sourceview.JavaDocument;
+import de.uka.ilkd.key.gui.sourceview.JavaJMLEditorLexer;
+import de.uka.ilkd.key.gui.sourceview.KeYEditorLexer;
+import de.uka.ilkd.key.gui.sourceview.SourceHighlightDocument;
 import de.uka.ilkd.key.gui.sourceview.TextLineNumber;
 import de.uka.ilkd.key.gui.utilities.GuiUtilities;
 import de.uka.ilkd.key.gui.utilities.SquigglyUnderlinePainter;
@@ -687,7 +689,9 @@ private void updatePreview(PositionedIssueString issue) {
                     }), "\n");
 
                 if (isJava(uri.getPath())) {
-                    showJavaSourceCode(source);
+                    showSourceCode(source, new JavaJMLEditorLexer());
+                } else if (isKeY(uri.getPath())) {
+                    showSourceCode(source, new KeYEditorLexer());
                 } else {
                     txtSource.setText(source);
                 }
@@ -709,9 +713,9 @@ private void updateStackTrace(PositionedIssueString issue) {
         txtStacktrace.setText(issue.getAdditionalInfo());
     }
 
-    private void showJavaSourceCode(String source) {
+    private void showSourceCode(String source, SourceHighlightDocument.EditorLexer lexer) {
         try {
-            JavaDocument doc = new JavaDocument();
+            SourceHighlightDocument doc = new SourceHighlightDocument(lexer);
             txtSource.setDocument(doc);
             doc.insertString(0, source, new SimpleAttributeSet());
         } catch (BadLocationException e) {
@@ -752,6 +756,10 @@ private boolean isJava(String fileName) {
         return fileName != null && fileName.endsWith(".java");
     }
 
+    private boolean isKeY(String fileName) {
+        return fileName != null && (fileName.endsWith(".key") || fileName.endsWith(".proof"));
+    }
+
     public static int getOffsetFromLineColumn(String source, Position pos) {
         // Position has 1-based line and column, we need them 0-based
         return getOffsetFromLineColumn(source, pos.line() - 1, pos.column() - 1);

key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecisionTest.java

@@ -6,16 +6,12 @@
 import java.awt.*;
 import java.awt.event.ActionEvent;
 import java.awt.event.ActionListener;
-import java.awt.event.KeyAdapter;
-import java.awt.event.KeyEvent;
 import java.io.File;
 import java.io.IOException;
 import java.net.URI;
 import java.nio.file.Files;
 import java.nio.file.Paths;
 import java.util.Optional;
-import java.util.Timer;
-import java.util.TimerTask;
 import javax.swing.*;
 import javax.swing.border.TitledBorder;
 import javax.swing.text.BadLocationException;
@@ -25,7 +21,9 @@
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.gui.configuration.Config;
 import de.uka.ilkd.key.gui.fonticons.IconFactory;
-import de.uka.ilkd.key.gui.sourceview.JavaDocument;
+import de.uka.ilkd.key.gui.sourceview.JavaJMLEditorLexer;
+import de.uka.ilkd.key.gui.sourceview.KeYEditorLexer;
+import de.uka.ilkd.key.gui.sourceview.SourceHighlightDocument;
 import de.uka.ilkd.key.gui.sourceview.TextLineNumber;
 import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.parser.Location;
@@ -137,65 +135,35 @@ public void addNotify() {
                 textAreaGoto(this, location.getPosition());
             }
         };
-        Optional<URI> file = location.getFileURI();
-        String source = IOUtil.readFrom(file.orElse(null));
+        Optional<URI> fileOpt = location.getFileURI();
+        if (fileOpt.isEmpty()) {
+            JTextPane jTextPane = new JTextPane();
+            jTextPane.setText("No file location available");
+            return jTextPane;
+        }
+
+        URI file = fileOpt.get();
+        String source = IOUtil.readFrom(file);
         // workaround for #1641: replace all carriage returns, since JavaDocument can currently
         // not handle them
         source = source != null ? source.replace("\r", "") : "";
 
-        if (file.isPresent() && file.get().toString().endsWith(".java")) {
-            JavaDocument doc = new JavaDocument();
-            try {
-                doc.insertString(0, source, new SimpleAttributeSet());
-            } catch (BadLocationException e) {
-                LOGGER.warn("Failed insert string", e);
-            }
-            textPane.setDocument(doc);
-
-            // when no char is inserted for the specified interval, refresh the syntax highlighting
-            // note: When other keys are pressed or held down (e.g. arrow keys) nothing is done.
-            textPane.addKeyListener(new KeyAdapter() {
-                private Timer timer = new Timer();
-
-                @Override
-                public void keyTyped(KeyEvent e) {
-                    restartTimer();
-                }
-
-                private void restartTimer() {
-                    timer.cancel();
-                    timer = new Timer();
-                    final TimerTask task = new TimerTask() {
-                        @Override
-                        public void run() {
-                            // synchronized to avoid inserting chars during document updating
-                            synchronized (textPane) {
-                                int pos = textPane.getCaretPosition();
-                                int start = textPane.getSelectionStart();
-                                int end = textPane.getSelectionEnd();
-                                String content = textPane.getText();
-                                try {
-                                    // creating a completely new document seems to be more than
-                                    // necessary, but works well enough for the moment
-                                    JavaDocument newDoc = new JavaDocument();
-                                    newDoc.insertString(0, content, new SimpleAttributeSet());
-                                    textPane.setDocument(newDoc);
-                                    textPane.setCaretPosition(pos);
-                                    textPane.setSelectionStart(start);
-                                    textPane.setSelectionEnd(end);
-                                } catch (BadLocationException ex) {
-                                    LOGGER.warn("Failed update document", ex);
-                                }
-                                textPane.repaint();
-                            }
-                        }
-                    };
-                    timer.schedule(task, SYNTAX_HIGHLIGHTING_REFRESH_INTERVAL);
-                }
-            });
+        SourceHighlightDocument.EditorLexer lexer;
+        if (file.toString().endsWith(".java")) {
+            lexer = new JavaJMLEditorLexer();
+        } else if (file.toString().endsWith(".key") || file.toString().endsWith(".proof")) {
+            lexer = new KeYEditorLexer();
         } else {
-            textPane.setText(source);
+            lexer = SourceHighlightDocument.TRIVIAL_LEXER;
+        }
+
+        SourceHighlightDocument doc = new SourceHighlightDocument(lexer);
+        try {
+            doc.insertString(0, source, new SimpleAttributeSet());
+        } catch (BadLocationException e) {
+            LOGGER.warn("Failed insert string", e);
         }
+        textPane.setDocument(doc);
 
         Font font = UIManager.getFont(Config.KEY_FONT_SEQUENT_VIEW);
         if (font == null) {

key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java

@@ -11,8 +11,7 @@
 import javax.swing.text.*;
 
 import de.uka.ilkd.key.gui.colors.ColorSettings;
-
-import static de.uka.ilkd.key.speclang.jml.JMLUtils.isJmlCommentStarter;
+import de.uka.ilkd.key.speclang.njml.JmlMarkerDecision;
 
 /**
  * This document performs syntax highlighting when strings are inserted. However, only inserting the
@@ -321,8 +320,10 @@ private void checkAt() {
                 || state == CommentState.JML_ANNOTATION_LINE) {
             boolean lineComment = state == CommentState.JML_ANNOTATION_LINE;
             state = CommentState.NO;
-            String features = token.substring(2); // cut-off '//' or '/*'
-            if (isJmlCommentStarter(features)) {
+            String features = token.substring(2, token.length() - 1); // cut-off '//' or '/*' and
+                                                                      // '@'
+            var jmlMarkerDecision = new JmlMarkerDecision(null);
+            if (jmlMarkerDecision.isActiveJmlSpec(features)) {
                 mode = lineComment ? Mode.LINE_JML : Mode.JML;
             } else {
                 mode = lineComment ? Mode.LINE_COMMENT : Mode.COMMENT;