Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proposing a more flexible lexing framework #3537

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
+1,040 −65
Open

Proposing a more flexible lexing framework #3537

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f1561c9
proposing a more flexible lexing framework
mattulbrich Jan 17, 2025
393374a
secondary keyword colour for key files
mattulbrich Jan 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 12 additions & 4 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
}
Expand All @@ -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) {
Expand Down Expand Up @@ -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);
Expand Down
84 changes: 26 additions & 58 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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) {
Expand Down
160 changes: 160 additions & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JMLEditorLexer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,160 @@
/* 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.gui.sourceview;
//
// import de.uka.ilkd.key.gui.colors.ColorSettings;
// import de.uka.ilkd.key.nparser.KeYLexer;
// import de.uka.ilkd.key.parser.proofjava.JavaCharStream;
// import de.uka.ilkd.key.parser.proofjava.ProofJavaParser;
// import de.uka.ilkd.key.parser.proofjava.ProofJavaParserTokenManager;
// import static de.uka.ilkd.key.parser.proofjava.ProofJavaParserConstants.*;
//
// import de.uka.ilkd.key.parser.proofjava.Token;
// import de.uka.ilkd.key.speclang.njml.JmlLexer;
// import org.antlr.v4.runtime.CharStreams;
//
// import javax.swing.text.SimpleAttributeSet;
// import javax.swing.text.StyleConstants;
// import java.awt.*;
// import java.io.StringReader;
// import java.util.ArrayList;
// import java.util.BitSet;
// import java.util.List;
//
// public class JMLEditorLexer implements SourceHighlightDocument.EditorLexer {
//
// /** highight color for Java keywords (dark red/violet) */
// private static final ColorSettings.ColorProperty JAVA_KEYWORD_COLOR =
// ColorSettings.define("[java]keyword", "", new Color(0x7f0055));
//
// // private static final Color JAVA_STRING_COLOR = new Color(0x000000);
//
// /** highight color for comments (dull green) */
// private static final ColorSettings.ColorProperty COMMENT_COLOR =
// ColorSettings.define("[java]comment", "", new Color(0x3f7f5f));
//
// /** highight color for JavaDoc (dull green) */
// private static final ColorSettings.ColorProperty JAVADOC_COLOR =
// ColorSettings.define("[java]javadoc", "", new Color(0x3f7f5f));
//
// /** highight color for JML (dark blue) */
// private static final ColorSettings.ColorProperty JML_COLOR =
// ColorSettings.define("[java]jml", "", new Color(0x0000c0));
//
// /** highight color for JML keywords (blue) */
// private static final ColorSettings.ColorProperty JML_KEYWORD_COLOR =
// ColorSettings.define("[java]jmlKeyword", "", new Color(0x0000f0));
//
//
// /** default style */
// private static final SimpleAttributeSet normal = new SimpleAttributeSet();
//
// /** the style of keywords */
// private static final SimpleAttributeSet keyword = new SimpleAttributeSet();
//
// /** the style of comments and line comments */
// private static final SimpleAttributeSet comment = new SimpleAttributeSet();
//
// /** the style of JavaDoc */
// private static final SimpleAttributeSet javadoc = new SimpleAttributeSet();
//
// /** the style of JML annotations */
// private static final SimpleAttributeSet jml = new SimpleAttributeSet();
//
// /** the style of JML keywords */
// private static final SimpleAttributeSet jmlkeyword = new SimpleAttributeSet();
//
// private static final BitSet KEYWORDS = new BitSet();
// private static final BitSet JAVDOCS = new BitSet();
// private static final BitSet COMMENTS = new BitSet();
// private static final BitSet JMLS = new BitSet();
// private static final BitSet JMLKEYWORDS = new BitSet();
//
// static {
// StyleConstants.setBold(keyword, true);
// StyleConstants.setForeground(keyword, JAVA_KEYWORD_COLOR.get());
// StyleConstants.setForeground(comment, COMMENT_COLOR.get());
// StyleConstants.setForeground(javadoc, JAVADOC_COLOR.get());
// // StyleConstants.setForeground(string, JAVA_STRING_COLOR);
// StyleConstants.setForeground(jml, JML_COLOR.get());
// StyleConstants.setForeground(jmlkeyword, JML_KEYWORD_COLOR.get());
// StyleConstants.setBold(jmlkeyword, true);
// addAll(KEYWORDS, ABSTRACT, ASSERT, BOOLEAN, BREAK, BYTE, CASE, CATCH, CHAR, CLASS, CONST,
// CONTINUE, DEFAULT,
// DO, DOUBLE, ELSE, ENUM, EXTENDS, FINAL, FINALLY, FLOAT, FOR, GOTO, IF, IMPLEMENTS, IMPORT,
// INSTANCEOF,
// INT, INTERFACE, LONG, NATIVE, NEW, PACKAGE, PRIVATE, PROTECTED, PUBLIC, RETURN, SHORT, STATIC,
// STRICTFP,
// SUPER, SWITCH, SYNCHRONIZED, THIS, THROW, THROWS, TRANSIENT, TRY, VOID, VOLATILE, WHILE);
//// addAll(LITERALS, STRING_LITERAL, HEX_LITERAL, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL,
// REAL_LITERAL, TRUE,
//// FALSE);
// addAll(COMMENTS, SINGLE_LINE_COMMENT, MULTI_LINE_COMMENT);
// addAll(JAVDOCS, FORMAL_COMMENT);
// }
//
// private static void addAll(BitSet bitSet, int... values) {
// for (int value : values) {
// bitSet.set(value);
// }
// }
//
// private SimpleAttributeSet getAttributes(int kind) {
// if(KEYWORDS.get(kind)) {
// return keyword;
// } else if(COMMENTS.get(kind)) {
// return comment;
// } else if(JAVDOCS.get(kind)) {
// return javadoc;
// } else {
// return normal;
// }
// }
//
// private SimpleAttributeSet getJMLAttributes(int kind) {
// if(kind == JmlLexer.ENSURES) {
// return jmlkeyword;
// } else {
// return jml;
// }
// }
//
// @Override
// public List<SourceHighlightDocument.Token> applyTo(String text) {
// ProofJavaParser.initialize(new StringReader(text));
// ProofJavaParserTokenManager tm = ProofJavaParser.token_source;
// List<SourceHighlightDocument.Token> result = new ArrayList<>();
// Token t = tm.getNextToken();
// while(t.kind != 0) {
// System.out.println(t.kind + " " + t.image);
// if(t.kind == SINGLE_LINE_COMMENT && t.image.startsWith("//@") ||
// t.kind == MULTI_LINE_COMMENT && t.image.startsWith("/*@")) {
// result.addAll(parseJML(t.image));
// } else {
// result.add(new SourceHighlightDocument.Token(t.image.length(), getAttributes(t.kind)));
// }
//
// if (t.specialToken != null) {
// t = t.specialToken;
// } if (t.next != null) {
// t = t.next;
// } else {
// t = tm.getNextToken();
// }
// }
// return result;
// }
//
// private List<SourceHighlightDocument.Token> parseJML(String text) {
// JmlLexer jmlLexer = new JmlLexer(CharStreams.fromString(text));
// List<SourceHighlightDocument.Token> result = new ArrayList<>();
// var t = jmlLexer.nextToken();
// while(t.getType() != -1) {
// result.add(new SourceHighlightDocument.Token(t.getText().length(),
// getJMLAttributes(t.getType())));
// t = jmlLexer.nextToken();
// }
// return result;
// }
// }
Loading
Loading