From f1561c970f816e45ccbf7e942af84b40ee129dbb Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sat, 18 Jan 2025 00:01:17 +0100 Subject: [PATCH 1/2] proposing a more flexible lexing framework --- .../java/de/uka/ilkd/key/gui/IssueDialog.java | 16 +- .../key/gui/actions/EditSourceFileAction.java | 84 +-- .../key/gui/sourceview/JMLEditorLexer.java | 160 ++++++ .../gui/sourceview/JavaJMLEditorLexer.java | 544 ++++++++++++++++++ .../key/gui/sourceview/KeYEditorLexer.java | 152 +++++ .../sourceview/SourceHighlightDocument.java | 139 +++++ .../ilkd/key/gui/sourceview/SourceView.java | 6 +- 7 files changed, 1036 insertions(+), 65 deletions(-) create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JMLEditorLexer.java create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaJMLEditorLexer.java create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceHighlightDocument.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java index 58587967ba5..a49fcdb69e3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.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); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java index 8d495db8c9c..dad5592850e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.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 file = location.getFileURI(); - String source = IOUtil.readFrom(file.orElse(null)); + Optional 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) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JMLEditorLexer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JMLEditorLexer.java new file mode 100644 index 00000000000..5e1ceb18b70 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JMLEditorLexer.java @@ -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 applyTo(String text) { +// ProofJavaParser.initialize(new StringReader(text)); +// ProofJavaParserTokenManager tm = ProofJavaParser.token_source; +// List 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 parseJML(String text) { +// JmlLexer jmlLexer = new JmlLexer(CharStreams.fromString(text)); +// List 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; +// } +// } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaJMLEditorLexer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaJMLEditorLexer.java new file mode 100644 index 00000000000..987a105864b --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaJMLEditorLexer.java @@ -0,0 +1,544 @@ +/* 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 java.awt.*; +import java.beans.PropertyChangeListener; +import java.io.Serial; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.regex.Pattern; +import javax.swing.text.*; + +import de.uka.ilkd.key.gui.colors.ColorSettings; + +import static de.uka.ilkd.key.speclang.jml.JMLUtils.isJmlCommentStarter; + +/** + * This lexer splits a text into tokens with coloured attributes. + *

+ * It is based on the mechanisms in class {@link JavaDocument}. + * + * @see JavaDocument + * @author Wolfram Pfeifer, Mattias Ulbrich + */ +public class JavaJMLEditorLexer implements SourceHighlightDocument.EditorLexer { + + @Serial + private static final long serialVersionUID = -1856296532743892931L; + + // highlighting colors (same as in HTMLSyntaxHighlighter of SequentView for consistency) + + /** 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)); + + /** + * Enum to indicate the current mode (environment) of the parser. Examples are STRING ("..."), + * COMMENT (/* ... */), JML (/*@ ... */ ), ... + */ + private enum Mode { + /* parser is currently inside a String */ + // STRING, // currently not in use + /** parser is currently inside normal java code */ + NORMAL, + /** parser is currently inside a keyword */ + KEYWORD, + /** parser is currently inside a comment (starting with "/*") */ + COMMENT, + /** parser is currently inside a line comment (starting with "//") */ + LINE_COMMENT, + /** parser is currently inside a line JML annotation (starting with "//@") */ + LINE_JML, + /** parser is currently inside JavaDoc (starting with "/**") */ + JAVADOC, + /** parser is currently inside an annotation (starting with "@") */ + ANNOTATION, + /** parser is currently inside a JML annotation (starting with "/*@") */ + JML, + /** parser is currently inside a JML keyword */ + JML_KEYWORD + } + + /** + * Enum to indicate the current comment state of the parser. It is used to store which comment + * relevant chars were just recently encountered. + */ + private enum CommentState { + /** no comment char encountered */ + NO, + /** last processed char was "/" */ + MAYBE, + /** last processed chars were "/*" */ + COMMENT, + /** last processed chars were "//" */ + LINECOMMENT, + /** + * current token could be a JML annotation marker (see JML reference manual 4.4, + * + * http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_4.html#SEC29) + */ + JML_ANNOTATION, + /** + * current token could be a JML annotation marker inside single line JML (see JML reference + * manual 4.4, + * + * http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_4.html#SEC29) + */ + JML_ANNOTATION_LINE, + /** last processed char was "*" */ + MAYBEEND + } + + /** + * Regular expression character class for all chars which are delimiters of keywords. \\Q ... + * \\E is used to escape all chars inside the class. + */ + private static final String DELIM = "[\\Q .;{}[]\n\r()+-*/%!=<>?:~&|^@'\"\\E]"; + + /** Pattern to match JML start with annotation marker(s). */ + private static final Pattern JML_ANNOT_MARKER = Pattern.compile("/\\*([+|-][$_a-zA-Z0-9]+)+@"); + + /** Pattern to match single line JML start with annotation marker(s). */ + private static final Pattern JML_ANNOT_MARKER_LINE = + Pattern.compile("//([+|-][$_a-zA-Z0-9]+)+@"); + + /** + * Stores the Java keywords which have to be highlighted. The list is taken from + * + * https://docs.oracle.com/javase/tutorial/java/nutsandbolts/_keywords.html . + *

+ * To add additional keywords, simply add them to the array. Note that the keywords must not + * contain any of the characters defined by the DELIM regex. + */ + private static final String[] KEYWORDS = { "abstract", "assert", "boolean", "break", "byte", + "case", "catch", "char", "class", "continue", "default", "do", "double", "else", "enum", + "extends", "final", "finally", "float", "for", "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", "true", "false", "null" + // "const", "goto" // reserved, but currently not used in Java + }; + + /** + * Stores the JML keywords which have to be highlighted. + *

+ * To add additional keywords, simply add them to the array. Note that the keywords must not + * contain any of the characters defined by the DELIM regex. + */ + private static final String[] JMLKEYWORDS = { + // other Java keywords + "break", "case", "catch", "class", "const", "continue", "default", "do", "else", "extends", + "false", "finally", "for", "goto", "if", "implements", "import", "instanceof", "interface", + "label", "new", "null", "package", "return", "super", "switch", "this", "throw", "throws", + "true", "try", "void", "while", + // types: + "boolean", "byte", "char", "double", "float", "int", "long", "short", "\\bigint", + "\\locset", "\\real", "\\seq", "\\TYPE", + // modifiers: + "abstract", "code", "code_bigint_math", "code_java_math", "code_safe_math", "extract", + "final", "ghost", "helper", "instance", "model", "native", "non_null", "nullable", + "nullable_by_default", "private", "protected", "peer", "\\peer", "public", "pure", "rep", + "\\rep", "spec_bigint_math", "spec_java_math", "spec_protected", "spec_public", + "spec_safe_math", "static", "strictfp", "strictly_pure", "synchronized", "transient", + "two_state", "uninitialized", "volatile", + + "no_state", "erases", "returns", "break_behavior", "continue_behavior", "return_behavior", + // special JML expressions: + "\\constraint_for", "\\created", "\\disjoint", "\\duration", "\\everything", "\\exception", + "\\exists", "\\forall", "\\fresh", "\\index", "\\invariant_for", "\\is_initialized", + "\\itself", "\\lblneg", "\\lblpos", "\\lockset", "\\max", "\\measured_by", "\\min", + "\\new_elems_fresh", "\\nonnullelements", "\\not_accessed", "\\not_assigned", + "\\not_modified", "\\not_specified", "\\nothing", "\\num_of", "\\old", "\\only_assigned", + "\\only_called", "\\only_captured", "\\pre", "\\product", "\\reach", "\\reachLocs", + "\\result", "\\same", "\\seq_contains", "\\space", "\\static_constraint_for", + "\\static_invariant_for", "\\strictly_nothing", "\\subset", "\\sum", "\\type", "\\typeof", + "\\working_space", "\\values", "\\inv", + // clause keywords: + "accessible", "accessible_redundantly", "assert", "assert_redundantly", + "assignable", "assignable_free", "assignable_redundantly", "assigns", "assigns_free", + "assigns_redundantly", "assigning", "assigning_free", "assigning_redundantly", + "modifiable", "modifiable_free", "modifiable_redundantly", "modifies", "modifies_free", + "modifies_redundantly", "modifying", "modifying_free", "modifying_redundantly", + "loop_assignable", "loop_assignable_free", "loop_assignable_redundantly", "loop_assigns", + "loop_assigns_free", "loop_assigns_redundantly", "loop_assigning", "loop_assigning_free", + "loop_assigning_redundantly", "loop_modifiable", "loop_modifiable_free", + "loop_modifiable_redundantly", "loop_modifies", "loop_modifies_free", + "loop_modifies_redundantly", "loop_modifying", "loop_modifying_free", + "loop_modifying_redundantly", "loop_writable", "loop_writable_free", + "loop_writable_redundantly", "loop_writes", "loop_writes_free", "loop_writes_redundantly", + "loop_writing", "loop_writing_free", "loop_writing_redundantly", + "assume", "assume_redudantly", "breaks", "breaks_redundantly", "\\by", + "callable", "callable_redundantly", "captures", + "captures_redundantly", "continues", "continues_redundantly", "debug", "\\declassifies", + "decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly", + "loop_variant", "loop_variant_redundantly", "diverges", + "determines", "diverges_redundantly", "duration", "duration_redundantly", "ensures", + "ensures_free", "ensures_redundantly", "\\erases", "forall", "for_example", "hence_by", + "implies_that", "in", "in_redundantly", "\\into", "loop_invariant", "loop_invariant_free", + "loop_invariant_redundantly", "measured_by", "measured_by_redundantly", "maintaining", + "maintaining_redundantly", "maps", "maps_redundantly", "\\new_objects", "old", "refining", + "represents", "requires", "requires_free", "set", "signals", "signals_only", "\\such_that", + "unreachable", "when", "working_space", + // "invariant-like" keywords + "abrupt_behavior", "abrupt_behaviour", "also", "axiom", "behavior", "behaviour", + "constraint", "exceptional_behavior", "exceptional_behaviour", "initially", "invariant", + "invariant_free", "model_behavior", "model_behaviour", "monitors_for", "normal_behavior", + "normal_behaviour", "readable", "writable", "writes", "writing", + // ADT functions: + "\\seq_empty", "\\seq_def", "\\seq_singleton", "\\seq_get", "\\seq_upd", "\\seq_upd", + "\\seq_reverse", "\\seq_sub", + "\\seq_length", "\\index_of", "\\seq_concat", "\\empty", "\\singleton", "\\set_union", + "\\intersect", "\\set_minus", "\\all_fields", "\\infinite_union", + "\\strictly_than_nothing" }; + + /** the style of annotations */ + private final SimpleAttributeSet annotation = new SimpleAttributeSet(); + + /* the style of strings */ + // private SimpleAttributeSet string = new SimpleAttributeSet(); + + /** default style */ + private final SimpleAttributeSet normal = new SimpleAttributeSet(); + + /** the style of keywords */ + private final SimpleAttributeSet keyword = new SimpleAttributeSet(); + + /** the style of comments and line comments */ + private final SimpleAttributeSet comment = new SimpleAttributeSet(); + + /** the style of JavaDoc */ + private final SimpleAttributeSet javadoc = new SimpleAttributeSet(); + + /** the style of JML annotations */ + private final SimpleAttributeSet jml = new SimpleAttributeSet(); + + /** the style of JML keywords */ + private final SimpleAttributeSet jmlkeyword = new SimpleAttributeSet(); + + /** stores the keywords */ + private final Set keywords = new HashSet<>(KEYWORDS.length); + + /** stores the JML keywords */ + private final Set jmlkeywords = new HashSet<>(JMLKEYWORDS.length); + + /** + * The current position of the parser in the inserted String. + */ + private int currentPos = 0; + + /** + * The start index of the current token in the inserted String. + */ + private int tokenStart = 0; + + /** + * The current token of the parser. + */ + private String token = ""; + + /** + * Stores the mode in which the parser currently is. + */ + private JavaJMLEditorLexer.Mode mode = Mode.NORMAL; + + /** + * Stores the current comment state of the parser to recognize comments/comment ends. + */ + private JavaJMLEditorLexer.CommentState state = CommentState.NO; + + /** + * The settings listener of this document (registered in the static listener list). + */ + private final transient PropertyChangeListener listener = e -> updateStyles(); + + private final List result = new ArrayList<>(); + + /** + * Creates a new JavaDocument and sets the syntax highlighting styles (as in eclipse default + * settings). + */ + public JavaJMLEditorLexer() { + updateStyles(); + ColorSettings.getInstance().addPropertyChangeListener(listener); + + // fill the keyword hash sets + keywords.addAll(Arrays.asList(KEYWORDS)); + jmlkeywords.addAll(Arrays.asList(JMLKEYWORDS)); + } + + /** + * Use the own parsing infrastructure to apply syntax highlighting to the given text. + * + * @param text non-null text to parse + * @return list of tokens with their respective styles + */ + @Override + public List applyTo(String text) { + result.clear(); + currentPos = 0; + tokenStart = 0; + token = ""; + state = CommentState.NO; + mode = Mode.NORMAL; + var chars = text.toCharArray(); + for (char aChar : chars) { + try { + processChar(aChar); + } catch (BadLocationException e) { + e.printStackTrace(); + throw new RuntimeException(e); + } + } + return result; + } + + /** + * Dispose this object. + */ + public void dispose() { + ColorSettings.getInstance().removePropertyChangeListener(listener); + } + + private void updateStyles() { + // set the styles + 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); + } + + private void checkAt() { + token += '@'; + if (state == CommentState.COMMENT) { // "/*@" + state = CommentState.NO; + mode = Mode.JML; + } else if (state == CommentState.LINECOMMENT) { // "//@" + state = CommentState.NO; + mode = Mode.LINE_JML; + } else if (mode == Mode.NORMAL && state == CommentState.NO) { // "@" + mode = Mode.ANNOTATION; + tokenStart = currentPos; + } else if (state == CommentState.JML_ANNOTATION + || 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)) { + mode = lineComment ? Mode.LINE_JML : Mode.JML; + } else { + mode = lineComment ? Mode.LINE_COMMENT : Mode.COMMENT; + } + } + } + + private void checkSpaceTab(char c) { + token += c; + state = CommentState.NO; + } + + private void checkPlusMinus(char c) { + if (state == CommentState.LINECOMMENT || state == CommentState.JML_ANNOTATION_LINE) { + // "//+" or "//-" + token += c; + state = CommentState.JML_ANNOTATION_LINE; + } else if (state == CommentState.COMMENT || state == CommentState.JML_ANNOTATION) { + // "/*+" or "/*-" + token += c; + state = CommentState.JML_ANNOTATION; + } else { + token += c; + state = CommentState.NO; + } + } + + private void checkLinefeed() throws BadLocationException { + state = CommentState.NO; + if (mode == Mode.LINE_COMMENT) { // "// ... \n" + insertCommentString(token, tokenStart); + mode = Mode.NORMAL; // reset + token = "\n"; // reset token + tokenStart = currentPos; + } else if (mode == Mode.LINE_JML) { // "//@ ... \n" + insertJMLString(token, tokenStart); + mode = Mode.NORMAL; // reset + token = "\n"; // reset token + tokenStart = currentPos; + } else if (mode == Mode.ANNOTATION) { // "@ ... \n" + insertAnnotation(token, tokenStart); + mode = Mode.NORMAL; // reset + token = "\n"; // reset token + tokenStart = currentPos; + } else if (mode == Mode.NORMAL) { // normal mode + insertNormalString(token, tokenStart); + token = "\n"; // reset token + tokenStart = currentPos; + } else { // modes: JML, Comment, JavaDoc + token += '\n'; + } + } + + private void checkStar() throws BadLocationException { + if (state == CommentState.MAYBE) { // "/*" + // insert what we have in this line so far + insertNormalString(token.substring(0, token.length() - 1), tokenStart); + token = "/*"; + tokenStart = currentPos - 1; + state = CommentState.COMMENT; + mode = Mode.COMMENT; + } else if (state == CommentState.COMMENT) { // "/**" + // tokenStart should be already set here + token += '*'; + state = CommentState.MAYBEEND; + mode = Mode.JAVADOC; + } else if (mode == Mode.COMMENT // "/* ... *" + || mode == Mode.JAVADOC // "/*@ ... *" + || mode == Mode.JML) { // "/** ... *" + // tokenStart should be already set here + token += '*'; + state = CommentState.MAYBEEND; + } else { // multiplication + token += '*'; + state = CommentState.NO; + } + } + + private void checkSlash() throws BadLocationException { + if (mode == Mode.NORMAL && state == CommentState.NO) { // "/" + token += '/'; + state = CommentState.MAYBE; + } else if (state == CommentState.MAYBE) { // "//" + // insert what we have in this line so far + insertNormalString(token.substring(0, token.length() - 1), tokenStart); + token = "//"; + tokenStart = currentPos - 1; + state = CommentState.LINECOMMENT; + mode = Mode.LINE_COMMENT; + } else if (state == CommentState.MAYBEEND) { // "/* ... */" + token += '/'; + if (mode == Mode.COMMENT) { + insertCommentString(token, tokenStart); + } else if (mode == Mode.JAVADOC) { + if (token.equals("/**/")) { // "/**/" is no JavaDoc + insertCommentString(token, tokenStart); + } else { + insertJavadocString(token, tokenStart); + } + } else if (mode == Mode.JML) { + insertJMLString(token, tokenStart); + } + state = CommentState.NO; + mode = Mode.NORMAL; + token = ""; // reset token + tokenStart = currentPos + 1; + } else { + // not NORMAL_MODE + token += '/'; + } + } + + private void checkQuote() { // TODO: separate style for Strings + state = CommentState.NO; + token += '"'; + } + + private void checkOther(char c) { + token += c; + + if (state != CommentState.JML_ANNOTATION && state != CommentState.JML_ANNOTATION_LINE) { + state = CommentState.NO; + } + } + + private void checkDelimiter(char c) { + token += c; + state = CommentState.NO; + } + + private void processChar(char strChar) throws BadLocationException { + switch (strChar) { + case ('@') -> checkAt(); + case '\n' -> checkLinefeed(); + // all tabs should have been replaced earlier! + case '\t', ' ' -> checkSpaceTab(strChar); + case '*' -> checkStar(); + case '/' -> checkSlash(); + case '"' -> checkQuote(); + + // keyword delimiters: +-*/(){}[]%!^~.;?:&|<>="'\n(space) + case '+', '-' -> checkPlusMinus(strChar); + + // case '*': + // case '/': + case '(', ')', '[', ']', '{', '}', '%', '!', '^', '~', '&', '|', '.', ':', ';', '?', '<', + '>', '=', '\'' -> + // case ' ': + // case '"': + // case '\'': + // case '\n': + checkDelimiter(strChar); + default -> checkOther(strChar); + } + } + + private void insertCommentString(String str, int pos) throws BadLocationException { + result.add(new SourceHighlightDocument.Token(str.length(), comment)); + } + + private void insertAnnotation(String str, int pos) throws BadLocationException { + result.add(new SourceHighlightDocument.Token(str.length(), annotation)); + } + + private void insertJavadocString(String str, int pos) throws BadLocationException { + result.add(new SourceHighlightDocument.Token(str.length(), javadoc)); + } + + private void insertJMLString(String str, int pos) throws BadLocationException { + String[] tokens = str.split("((?<=" + DELIM + ")|(?=" + DELIM + "))"); + for (String t : tokens) { + if (jmlkeywords.contains(t)) { + result.add(new SourceHighlightDocument.Token(t.length(), jmlkeyword)); + } else { + result.add(new SourceHighlightDocument.Token(t.length(), jml)); + } + } + } + + private void insertNormalString(String str, int pos) throws BadLocationException { + String[] tokens = str.split("((?<=" + DELIM + ")|(?=" + DELIM + "))"); + for (String t : tokens) { + if (keywords.contains(t)) { + result.add(new SourceHighlightDocument.Token(t.length(), keyword)); + } else { + result.add(new SourceHighlightDocument.Token(t.length(), normal)); + } + } + } + +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java new file mode 100644 index 00000000000..7beab20815e --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java @@ -0,0 +1,152 @@ +/* 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 java.awt.*; +import java.util.ArrayList; +import java.util.BitSet; +import java.util.List; +import javax.swing.text.SimpleAttributeSet; +import javax.swing.text.StyleConstants; + +import de.uka.ilkd.key.gui.colors.ColorSettings; +import de.uka.ilkd.key.nparser.KeYLexer; + +import org.antlr.v4.runtime.CharStreams; + +import static de.uka.ilkd.key.nparser.KeYLexer.*; + +/** + * This is a lexer class used by a {@link SourceHighlightDocument} to highlight KeY code. + * It uses the ANTLR lexer {@link KeYLexer} to tokenize the text. + * + * @author Mattias Ulbrich + */ +public class KeYEditorLexer implements SourceHighlightDocument.EditorLexer { + + /** highight color for Java keywords (dark red/violet) */ + private static final ColorSettings.ColorProperty KEYWORD_COLOR = + ColorSettings.define("[key]keyword", "", new Color(0x7f0055)); + + /** highight color for comments (dull green) */ + private static final ColorSettings.ColorProperty COMMENT_COLOR = + ColorSettings.define("[key]comment", "", new Color(0x3f7f5f)); + + /** highight color for literals (dark blue) */ + private static final ColorSettings.ColorProperty LITERAL_COLOR = + ColorSettings.define("[key]literal", "", new Color(0x2A75B1)); + + /** highight color for Modalities (dark yellow) */ + private static final ColorSettings.ColorProperty MODALITY_COLOR = + ColorSettings.define("[key]modality", "", new Color(0xC4985B)); + + /** default style */ + private static final SimpleAttributeSet normalStyle = new SimpleAttributeSet(); + + /** the style of keywords */ + private static final SimpleAttributeSet commentStyle = new SimpleAttributeSet(); + + /** the style of keywords */ + private static final SimpleAttributeSet keywordStyle = new SimpleAttributeSet(); + + /** the style of literals */ + private static final SimpleAttributeSet literalStyle = new SimpleAttributeSet(); + + /** the style of comments and line comments */ + private static final SimpleAttributeSet modalityStyle = new SimpleAttributeSet(); + + /** the token identifiers for keywords */ + private static final BitSet KEYWORDS = new BitSet(); + + /** the token identifiers for literals */ + private static final BitSet LITERALS = new BitSet(); + + /** the token identifiers for comments */ + private static final BitSet COMMENTS = new BitSet(); + + /** the token identifiers for modalities */ + private static final BitSet MODALITIES = new BitSet(); + + static { + // set the styles + // StyleConstants.setBold(keywordStyle, true); + StyleConstants.setForeground(keywordStyle, KEYWORD_COLOR.get()); + StyleConstants.setForeground(commentStyle, COMMENT_COLOR.get()); + StyleConstants.setForeground(literalStyle, LITERAL_COLOR.get()); + StyleConstants.setForeground(modalityStyle, MODALITY_COLOR.get()); + + // the following can probably be refined + addAll(KEYWORDS, SORTS, GENERIC, PROXY, EXTENDS, ONEOF, ABSTRACT, SCHEMAVARIABLES, + SCHEMAVAR, MODALOPERATOR, + PROGRAM, FORMULA, TERM, UPDATE, VARIABLES, VARIABLE, SKOLEMTERM, SKOLEMFORMULA, + TERMLABEL, MODIFIABLE, + PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, + GET_FREE_INVARIANT, + GET_VARIANT, IS_LABELED, SAME_OBSERVER, VARCOND, APPLY_UPDATE_ON_RIGID, DEPENDINGON, + DISJOINTMODULONULL, + DROP_EFFECTLESS_ELEMENTARIES, DROP_EFFECTLESS_STORES, SIMPLIFY_IF_THEN_ELSE_UPDATE, + ENUM_CONST, + FREELABELIN, HASSORT, FIELDTYPE, FINAL, ELEMSORT, HASLABEL, HASSUBFORMULAS, ISARRAY, + ISARRAYLENGTH, + ISCONSTANT, ISENUMTYPE, ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, + METADISJOINT, + ISTHISREFERENCE, DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, ISSTATICFIELD, + ISMODELFIELD, + ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, + NEW_LOCAL_VARS, + HAS_ELEMENTARY_SORT, NEWLABEL, CONTAINS_ASSIGNMENT, NOT_, NOTFREEIN, SAME, STATIC, + STATICMETHODREFERENCE, MAXEXPANDMETHOD, STRICT, TYPEOF, INSTANTIATE_GENERIC, FORALL, + EXISTS, SUBST, IF, + IFEX, THEN, ELSE, INCLUDE, INCLUDELDTS, CLASSPATH, BOOTCLASSPATH, NODEFAULTCLASSES, + JAVASOURCE, + WITHOPTIONS, OPTIONSDECL, KEYSETTINGS, PROFILE, SAMEUPDATELEVEL, INSEQUENTSTATE, + ANTECEDENTPOLARITY, + SUCCEDENTPOLARITY, CLOSEGOAL, HEURISTICSDECL, NONINTERACTIVE, DISPLAYNAME, HELPTEXT, + REPLACEWITH, + ADDRULES, ADDPROGVARS, HEURISTICS, FIND, ADD, ASSUMES, TRIGGER, AVOID, PREDICATES, + FUNCTIONS, + DATATYPES, TRANSFORMERS, UNIQUE, FREE, RULES, AXIOMS, PROBLEM, CHOOSECONTRACT, + PROOFOBLIGATION, PROOF, + PROOFSCRIPT, CONTRACTS, INVARIANTS, LEMMA, IN_TYPE, IS_ABSTRACT_OR_INTERFACE, + CONTAINERTYPE); + addAll(LITERALS, STRING_LITERAL, HEX_LITERAL, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, + REAL_LITERAL, TRUE, + FALSE); + addAll(COMMENTS, DOC_COMMENT, ML_COMMENT, SL_COMMENT); + addAll(MODALITIES, MODALITY); + } + + private static void addAll(BitSet bitSet, int... values) { + for (int value : values) { + bitSet.set(value); + } + } + + private SimpleAttributeSet getAttributes(int type) { + if (KEYWORDS.get(type)) { + return keywordStyle; + } else if (LITERALS.get(type)) { + return literalStyle; + } else if (COMMENTS.get(type)) { + return commentStyle; + } else if (MODALITIES.get(type)) { + return modalityStyle; + } else { + return normalStyle; + } + } + + @Override + public List applyTo(String text) { + KeYLexer keYLexer = new KeYLexer(CharStreams.fromString(text)); + List result = new ArrayList<>(); + var t = keYLexer.nextToken(); + while (t.getType() != -1) { + result.add(new SourceHighlightDocument.Token(t.getText().length(), + getAttributes(t.getType()))); + t = keYLexer.nextToken(); + } + return result; + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceHighlightDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceHighlightDocument.java new file mode 100644 index 00000000000..37d3f99c29c --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceHighlightDocument.java @@ -0,0 +1,139 @@ +/* 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 java.awt.*; +import java.util.List; +import java.util.Timer; +import java.util.TimerTask; +import javax.swing.event.DocumentEvent; +import javax.swing.event.DocumentListener; +import javax.swing.text.*; + + +/** + * This document knows about syntax highlighting. + * + * It uses a lexer to determine the syntax highlighting for the text that it contains. + * + * There is a timer that triggers the re-parsing of the text after a certain time of inactivity. + * Currently the entire text is reparsed when needed. This is less efficient than in other + * frameworks + * that work line-based, but probably good enough for our purposes. + * + * @author Mattias Ulbrich + */ +public class SourceHighlightDocument extends DefaultStyledDocument { + + /** + * How long to wait after the last change before re-parsing the text. + */ + private static final long SYNTAX_HIGHLIGHTING_REFRESH_INTERVAL = 800; + + /** + * The timer that triggers the re-parsing of the text. + */ + private Timer refreshTimer = new Timer(); + + /** + * The listener that triggers the re-parsing of the text. + */ + private final DocumentListener docListener = new DocumentListener() { + @Override + public void insertUpdate(DocumentEvent documentEvent) { + restartTimer(); + } + + @Override + public void removeUpdate(DocumentEvent documentEvent) { + restartTimer(); + } + + @Override + public void changedUpdate(DocumentEvent documentEvent) { + // this seems to enter an infinite loop + // restartTimer(); + } + }; + + /** + * Tokens are the entities returned by the lexer. They contain the length of the token and the + * attributes that should be applied to it. + * + * @param len positive length of the token + * @param attributes to be applied to the span of text + */ + public record Token(int len, AttributeSet attributes) { + } + + /** + * An editor lexer is a function that takes a string and returns a list of tokens that describe + * the syntax highlighting of the string. + */ + public interface EditorLexer { + /** + * Parse the given non-null text into a list of tokens + * + * @param text non-null text to parse + * @return non-null list of tokens + */ + List applyTo(String text); + } + + /** + * A trivial lexer that does no syntax highlighting at all. + */ + public static final EditorLexer TRIVIAL_LEXER = new EditorLexer() { + @Override + public List applyTo(String text) { + return List.of(new Token(text.length(), new SimpleAttributeSet())); + } + }; + + /** + * The lexer that this document uses to determine the syntax highlighting. + */ + private final EditorLexer lexer; + + /** + * Create a new document that uses the given lexer for syntax highlighting. + * + * @param lexer the lexer to use + */ + public SourceHighlightDocument(EditorLexer lexer) { + this.lexer = lexer; + // workaround for #1641: typing "enter" key shall insert only "\n", even on Windows + putProperty(DefaultEditorKit.EndOfLineStringProperty, "\n"); + addDocumentListener(docListener); + } + + private void restartTimer() { + refreshTimer.cancel(); + refreshTimer = new Timer(); + final TimerTask task = new TimerTask() { + @Override + public void run() { + reparse(); + } + }; + refreshTimer.schedule(task, SYNTAX_HIGHLIGHTING_REFRESH_INTERVAL); + } + + private void reparse() { + try { + String text = getText(0, getLength()); + List tokens = lexer.applyTo(text); + int pos = 0; + for (Token token : tokens) { + setCharacterAttributes(pos, token.len(), token.attributes(), true); + pos += token.len(); + } + } catch (BadLocationException e) { + e.printStackTrace(); + throw new RuntimeException(e); + } + } + +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java index ea95cfdc20b..aae13e504a0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java @@ -936,7 +936,7 @@ public String getToolTipText(MouseEvent mouseEvent) { /** * The JavaDocument shown in this tab. */ - private JavaDocument doc = null; + private SourceHighlightDocument doc = null; private Tab(URI fileURI, InputStream stream) { this.absoluteFileName = fileURI; @@ -1012,7 +1012,7 @@ public void mouseMoved(MouseEvent mouseEvent) { // insert source code into text pane try { - doc = new JavaDocument(); + doc = new SourceHighlightDocument(new JavaJMLEditorLexer()); textPane.setDocument(doc); doc.insertString(0, source, new SimpleAttributeSet()); } catch (BadLocationException e) { @@ -1192,7 +1192,7 @@ private void scrollToLine(int line) { private void dispose() { if (doc != null) { - doc.dispose(); + // doc.dispose(); } } } From 393374a619fdaf4ea0b38750ef1124155f5f3613 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sat, 18 Jan 2025 10:55:18 +0100 Subject: [PATCH 2/2] secondary keyword colour for key files --- .../key/gui/sourceview/KeYEditorLexer.java | 74 ++++++++++--------- 1 file changed, 39 insertions(+), 35 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java index 7beab20815e..3240e1d3bdd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java @@ -21,14 +21,21 @@ * This is a lexer class used by a {@link SourceHighlightDocument} to highlight KeY code. * It uses the ANTLR lexer {@link KeYLexer} to tokenize the text. * + * Secondary keywords are highlighted in a different color. These are schema variables kinds, + * variable conditions etc. + * * @author Mattias Ulbrich */ public class KeYEditorLexer implements SourceHighlightDocument.EditorLexer { - /** highight color for Java keywords (dark red/violet) */ + /** highight color for KeY keywords (dark red/violet) */ private static final ColorSettings.ColorProperty KEYWORD_COLOR = ColorSettings.define("[key]keyword", "", new Color(0x7f0055)); + /** highight color for secondary KeY keywords (light red/violet) */ + private static final ColorSettings.ColorProperty KEYWORD2_COLOR = + ColorSettings.define("[key]keyword2", "", new Color(0x78526C)); + /** highight color for comments (dull green) */ private static final ColorSettings.ColorProperty COMMENT_COLOR = ColorSettings.define("[key]comment", "", new Color(0x3f7f5f)); @@ -39,7 +46,7 @@ public class KeYEditorLexer implements SourceHighlightDocument.EditorLexer { /** highight color for Modalities (dark yellow) */ private static final ColorSettings.ColorProperty MODALITY_COLOR = - ColorSettings.define("[key]modality", "", new Color(0xC4985B)); + ColorSettings.define("[key]modality", "", new Color(0xC67C13)); /** default style */ private static final SimpleAttributeSet normalStyle = new SimpleAttributeSet(); @@ -50,6 +57,9 @@ public class KeYEditorLexer implements SourceHighlightDocument.EditorLexer { /** the style of keywords */ private static final SimpleAttributeSet keywordStyle = new SimpleAttributeSet(); + /** the style of secondary keywords */ + private static final SimpleAttributeSet keyword2Style = new SimpleAttributeSet(); + /** the style of literals */ private static final SimpleAttributeSet literalStyle = new SimpleAttributeSet(); @@ -59,6 +69,9 @@ public class KeYEditorLexer implements SourceHighlightDocument.EditorLexer { /** the token identifiers for keywords */ private static final BitSet KEYWORDS = new BitSet(); + /** the token identifiers for secondary keywords */ + private static final BitSet KEYWORDS2 = new BitSet(); + /** the token identifiers for literals */ private static final BitSet LITERALS = new BitSet(); @@ -72,47 +85,36 @@ public class KeYEditorLexer implements SourceHighlightDocument.EditorLexer { // set the styles // StyleConstants.setBold(keywordStyle, true); StyleConstants.setForeground(keywordStyle, KEYWORD_COLOR.get()); + StyleConstants.setForeground(keyword2Style, KEYWORD2_COLOR.get()); StyleConstants.setForeground(commentStyle, COMMENT_COLOR.get()); StyleConstants.setForeground(literalStyle, LITERAL_COLOR.get()); StyleConstants.setForeground(modalityStyle, MODALITY_COLOR.get()); // the following can probably be refined addAll(KEYWORDS, SORTS, GENERIC, PROXY, EXTENDS, ONEOF, ABSTRACT, SCHEMAVARIABLES, - SCHEMAVAR, MODALOPERATOR, - PROGRAM, FORMULA, TERM, UPDATE, VARIABLES, VARIABLE, SKOLEMTERM, SKOLEMFORMULA, - TERMLABEL, MODIFIABLE, - PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, - GET_FREE_INVARIANT, - GET_VARIANT, IS_LABELED, SAME_OBSERVER, VARCOND, APPLY_UPDATE_ON_RIGID, DEPENDINGON, - DISJOINTMODULONULL, - DROP_EFFECTLESS_ELEMENTARIES, DROP_EFFECTLESS_STORES, SIMPLIFY_IF_THEN_ELSE_UPDATE, - ENUM_CONST, - FREELABELIN, HASSORT, FIELDTYPE, FINAL, ELEMSORT, HASLABEL, HASSUBFORMULAS, ISARRAY, - ISARRAYLENGTH, - ISCONSTANT, ISENUMTYPE, ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, - METADISJOINT, - ISTHISREFERENCE, DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, ISSTATICFIELD, - ISMODELFIELD, - ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, - NEW_LOCAL_VARS, - HAS_ELEMENTARY_SORT, NEWLABEL, CONTAINS_ASSIGNMENT, NOT_, NOTFREEIN, SAME, STATIC, - STATICMETHODREFERENCE, MAXEXPANDMETHOD, STRICT, TYPEOF, INSTANTIATE_GENERIC, FORALL, - EXISTS, SUBST, IF, - IFEX, THEN, ELSE, INCLUDE, INCLUDELDTS, CLASSPATH, BOOTCLASSPATH, NODEFAULTCLASSES, - JAVASOURCE, - WITHOPTIONS, OPTIONSDECL, KEYSETTINGS, PROFILE, SAMEUPDATELEVEL, INSEQUENTSTATE, - ANTECEDENTPOLARITY, - SUCCEDENTPOLARITY, CLOSEGOAL, HEURISTICSDECL, NONINTERACTIVE, DISPLAYNAME, HELPTEXT, - REPLACEWITH, - ADDRULES, ADDPROGVARS, HEURISTICS, FIND, ADD, ASSUMES, TRIGGER, AVOID, PREDICATES, - FUNCTIONS, + SCHEMAVAR, MODIFIABLE, PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, + GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, IS_LABELED, SAME_OBSERVER, VARCOND, + FORALL, EXISTS, SUBST, IF, IFEX, THEN, ELSE, INCLUDE, INCLUDELDTS, CLASSPATH, + BOOTCLASSPATH, NODEFAULTCLASSES, JAVASOURCE, WITHOPTIONS, OPTIONSDECL, KEYSETTINGS, + PROFILE, SAMEUPDATELEVEL, INSEQUENTSTATE, ANTECEDENTPOLARITY, SUCCEDENTPOLARITY, + CLOSEGOAL, HEURISTICSDECL, NONINTERACTIVE, DISPLAYNAME, HELPTEXT, REPLACEWITH, ADDRULES, + ADDPROGVARS, HEURISTICS, FIND, ADD, ASSUMES, TRIGGER, AVOID, PREDICATES, FUNCTIONS, DATATYPES, TRANSFORMERS, UNIQUE, FREE, RULES, AXIOMS, PROBLEM, CHOOSECONTRACT, - PROOFOBLIGATION, PROOF, - PROOFSCRIPT, CONTRACTS, INVARIANTS, LEMMA, IN_TYPE, IS_ABSTRACT_OR_INTERFACE, - CONTAINERTYPE); + PROOFOBLIGATION, PROOF, PROOFSCRIPT, CONTRACTS, INVARIANTS, LEMMA, IN_TYPE, + IS_ABSTRACT_OR_INTERFACE, CONTAINERTYPE); + addAll(KEYWORDS2, MODALOPERATOR, PROGRAM, FORMULA, TERM, UPDATE, VARIABLES, VARIABLE, + SKOLEMTERM, SKOLEMFORMULA, TERMLABEL, VARIABLES, VARIABLE, APPLY_UPDATE_ON_RIGID, + DEPENDINGON, DISJOINTMODULONULL, DROP_EFFECTLESS_ELEMENTARIES, DROP_EFFECTLESS_STORES, + SIMPLIFY_IF_THEN_ELSE_UPDATE, ENUM_CONST, FREELABELIN, HASSORT, FIELDTYPE, FINAL, + ELEMSORT, HASLABEL, HASSUBFORMULAS, ISARRAY, ISARRAYLENGTH, ISCONSTANT, ISENUMTYPE, + ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, METADISJOINT, ISTHISREFERENCE, + DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, ISSTATICFIELD, ISMODELFIELD, + ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, + NEW_LOCAL_VARS, HAS_ELEMENTARY_SORT, NEWLABEL, CONTAINS_ASSIGNMENT, NOT_, NOTFREEIN, + SAME, STATIC, STATICMETHODREFERENCE, MAXEXPANDMETHOD, STRICT, TYPEOF, + INSTANTIATE_GENERIC); addAll(LITERALS, STRING_LITERAL, HEX_LITERAL, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, - REAL_LITERAL, TRUE, - FALSE); + REAL_LITERAL, TRUE, FALSE); addAll(COMMENTS, DOC_COMMENT, ML_COMMENT, SL_COMMENT); addAll(MODALITIES, MODALITY); } @@ -126,6 +128,8 @@ private static void addAll(BitSet bitSet, int... values) { private SimpleAttributeSet getAttributes(int type) { if (KEYWORDS.get(type)) { return keywordStyle; + } else if (KEYWORDS2.get(type)) { + return keyword2Style; } else if (LITERALS.get(type)) { return literalStyle; } else if (COMMENTS.get(type)) {