diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java index c02495ab8cf..810e479745e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java @@ -71,7 +71,7 @@ public ProofScriptEngine(List script, Goal initiallySelectedGo this.script = script; } - private static Map loadCommands() { + public static Map loadCommands() { Map result = new HashMap<>(); var loader = ServiceLoader.load(ProofScriptCommand.class); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTree.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTree.java deleted file mode 100644 index 6918c7339ba..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTree.java +++ /dev/null @@ -1,40 +0,0 @@ -/* 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; - -import javax.swing.JTree; -import javax.swing.tree.DefaultMutableTreeNode; -import javax.swing.tree.DefaultTreeModel; - -/** - * This class is used by {@link InfoView} to display its contents. - * - * @author Kai Wallisch - */ -public class InfoTree extends JTree { - - /** - * - */ - private static final long serialVersionUID = 2018185104131516569L; - - InfoTree() { - DefaultMutableTreeNode root = new DefaultMutableTreeNode(); - root.add(new InfoTreeNode("No proof loaded", - "In this pane, the available logical rules will be displayed and/or explained.")); - setModel(new DefaultTreeModel(root)); - setShowsRootHandles(true); - setRootVisible(false); - } - - /* - * This function is expected to return only {@link InfoTreeNode} instances. The super method - * returns {@link DefaultMutableTreeNode} instances. - */ - @Override - public InfoTreeNode getLastSelectedPathComponent() { - return (InfoTreeNode) super.getLastSelectedPathComponent(); - } - -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java deleted file mode 100644 index bf1a05eddbc..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java +++ /dev/null @@ -1,223 +0,0 @@ -/* 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; - -import java.util.*; -import javax.swing.tree.DefaultTreeModel; - -import de.uka.ilkd.key.logic.MetaSpace; -import de.uka.ilkd.key.logic.NamespaceSet; -import de.uka.ilkd.key.logic.label.TermLabelManager; -import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.mgt.RuleJustification; -import de.uka.ilkd.key.rule.BuiltInRule; -import de.uka.ilkd.key.rule.NoPosTacletApp; -import de.uka.ilkd.key.rule.OneStepSimplifier; -import de.uka.ilkd.key.rule.Taclet; -import de.uka.ilkd.key.util.MiscTools; - -import org.key_project.logic.Name; -import org.key_project.logic.op.Function; - -/** - * Extension of {@link DefaultTreeModel} used by {@link InfoTree}. - * - * @author Kai Wallisch - */ -public class InfoTreeModel extends DefaultTreeModel { - - /** - * - */ - private static final long serialVersionUID = 2093787874117871875L; - private static final String LEMMAS = "Lemmas"; - private static final String TACLET_BASE = "Taclet Base"; - - public InfoTreeModel(Goal goal, MetaSpace meta, MainWindow mainWindow) { - super(new InfoTreeNode()); - insertAsLast(new RulesNode(meta, goal), (InfoTreeNode) root); - insertAsLast(new TermLabelsNode(goal.proof(), meta), - (InfoTreeNode) root); - insertAsLast(new FunctionsNode(meta, goal.getLocalNamespaces()), (InfoTreeNode) root); - } - - private void insertAsLast(InfoTreeNode ins, InfoTreeNode parent) { - insertNodeInto(ins, parent, parent.getChildCount()); - } - - private class FunctionsNode extends InfoTreeNode { - - /** - * - */ - private static final long serialVersionUID = -5546552277804988834L; - private static final String COLLECTION = - "This node stands for a category of symbols; expand it to browse the symbols " - + "in the category."; - private static final String DEFAULT_FUNCTIONS_LABEL = - "Display descriptions for documented interpreted function and predicate symbols."; - - FunctionsNode(MetaSpace functionExplanations, NamespaceSet nss) { - super("Function Symbols", DEFAULT_FUNCTIONS_LABEL); - - Map categoryMap = new HashMap<>(); - - var sortedKeys = new ArrayList<>(nss.functions().allElements()); - sortedKeys.sort(Comparator.comparing(it -> it.name().toString())); - - for (Function function : sortedKeys) { - var key = function.name().toString(); - var category = function.sort().name().toString(); - var doc = functionExplanations.findDocumentation(function); - InfoTreeNode categoryNode = categoryMap.get(category); - if (categoryNode == null) { - categoryNode = new InfoTreeNode(category, COLLECTION); - categoryMap.put(category, categoryNode); - insertAsLast(categoryNode, this); - } - insertAsLast(new InfoTreeNode(key, doc), categoryNode); - } - } - } - - private class TermLabelsNode extends InfoTreeNode { - - /** - * - */ - private static final long serialVersionUID = 7447092361863294242L; - - TermLabelsNode(Proof proof, MetaSpace meta) { - super("Term Labels", "Show descriptions for currently available term labels."); - - var mgr = TermLabelManager.getTermLabelManager(proof.getServices()); - var factories = mgr.getFactories(); - - var labelNames = new ArrayList<>(factories.keySet()); - labelNames.sort(Comparator.comparing(Name::toString)); - - for (Name name : labelNames) { - var item = - new InfoTreeNode(name.toString(), factories.get(name).getDocumentation()); - insertAsLast(item, this); - } - } - } - - private class RulesNode extends InfoTreeNode { - - /** - * - */ - private static final long serialVersionUID = 7622830441420768861L; - - RulesNode(MetaSpace meta, Goal goal) { - super("Rules", "Browse descriptions for currently available rules."); - - InfoTreeNode builtInRoot = new InfoTreeNode("Built-In", ""); - insertAsLast(builtInRoot, this); - InfoTreeNode axiomTacletRoot = new InfoTreeNode(TACLET_BASE, ""); - insertAsLast(axiomTacletRoot, this); - InfoTreeNode proveableTacletsRoot = new InfoTreeNode(LEMMAS, ""); - insertAsLast(proveableTacletsRoot, this); - - if (goal != null && goal.proof() != null && goal.proof().mgt() != null) { - for (final BuiltInRule br : goal.ruleAppIndex().builtInRuleAppIndex() - .builtInRuleIndex().rules()) { - insertAsLast(new InfoTreeNode(br, meta), builtInRoot); - } - Set set = goal.ruleAppIndex().tacletIndex().allNoPosTacletApps(); - OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(goal.proof()); - if (simplifier != null && !simplifier.isShutdown()) { - set.addAll(simplifier.getCapturedTaclets()); - } - - for (final NoPosTacletApp app : sort(set)) { - RuleJustification just = goal.proof().mgt().getJustification(app); - if (just == null) { - continue; // do not break system because of this - } - if (just.isAxiomJustification()) { - insertAndGroup(new InfoTreeNode(app.taclet(), meta), axiomTacletRoot, ""); - } else { - insertAndGroup(new InfoTreeNode(app.taclet(), meta), proveableTacletsRoot, - ""); - } - } - } - - axiomTacletRoot - .setUserObject(TACLET_BASE + " (" + getChildCount(axiomTacletRoot) + ")"); - proveableTacletsRoot - .setUserObject(LEMMAS + " (" + getChildCount(proveableTacletsRoot) + ")"); - } - - private int getChildCount(InfoTreeNode root) { - int res = 0; - for (int i = 0; i < root.getChildCount(); i++) { - final InfoTreeNode child = (InfoTreeNode) root.getChildAt(i); - // there is no deeper nesting - final int grandchildren = child.getChildCount(); - res += grandchildren == 0 ? 1 : grandchildren; - } - return res; - } - - /** - * groups subsequent insertions with the same name under a new node - */ - private void insertAndGroup(InfoTreeNode ins, InfoTreeNode parent, - String ruleExplanations) { - InfoTreeNode insNode = ins; - if (parent.getChildCount() > 0) { - InfoTreeNode lastNode = - (InfoTreeNode) parent.getChildAt(parent.getChildCount() - 1); - if (getName(insNode).equals(getName(lastNode))) { - if (lastNode.getChildCount() == 0) { - removeNodeFromParent(lastNode); - InfoTreeNode oldParent = parent; - parent = new InfoTreeNode(getName(insNode), ruleExplanations); - insNode.setTitleToAltName(); - lastNode.setTitleToAltName(); - insertAsLast(parent, oldParent); - insertAsLast(lastNode, parent); - } else { - parent = lastNode; - insNode.setTitleToAltName(); - } - } - } - insertAsLast(ins, parent); - } - - private String getName(InfoTreeNode t1) { - if (t1.getUserObject() instanceof Taclet) { - return ((Taclet) t1.getUserObject()).displayName(); - } else { - String title = t1.toString(); - - // strip number of taclets - int parenIdx = title.lastIndexOf('('); - if (parenIdx >= 0) { - return title.substring(0, parenIdx - 1).intern(); - } else { - return title; - } - } - } - - private List sort(Set set) { - final ArrayList l = new ArrayList<>(set); - - l.sort((o1, o2) -> { - final Taclet t1 = o1.taclet(); - final Taclet t2 = o2.taclet(); - return t1.displayName().compareTo(t2.displayName()); - }); - return l; - } - } - -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeNode.java deleted file mode 100644 index c6511723b98..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeNode.java +++ /dev/null @@ -1,98 +0,0 @@ -/* 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; - -import java.util.Properties; -import javax.swing.tree.DefaultMutableTreeNode; - -import de.uka.ilkd.key.logic.MetaSpace; -import de.uka.ilkd.key.pp.LogicPrinter; -import de.uka.ilkd.key.pp.NotationInfo; -import de.uka.ilkd.key.rule.BuiltInRule; -import de.uka.ilkd.key.rule.Rule; -import de.uka.ilkd.key.rule.Taclet; - -/** - * Every node of {@link InfoTree} is an instance of this class. - * - * @author Kai Wallisch - */ -public class InfoTreeNode extends DefaultMutableTreeNode { - - private static final long serialVersionUID = 4187650510339169399L; - // the original rule name - private final String altName; - private String description; - - private Rule rule; - - /* - * This constructor should only be used for the invisible root node of {@link InfoTreeModel}. - */ - InfoTreeNode() { - super("root node"); - altName = null; - description = "This is the root node of InfoTreeModel. It should not be visible."; - } - - /** - * @param title The name of the node. - * @param explanations An XML resource containing node descriptions. - */ - InfoTreeNode(String title, Properties explanations) { - super(title); - - altName = null; - String desc = explanations.getProperty(title); - - if (desc == null) { - description = "No description available for " + title + "."; - } else { - description = desc; - } - - } - - InfoTreeNode(Taclet taclet, MetaSpace metaSpace) { - super(taclet.displayName()); - this.rule = taclet; - altName = taclet.name().toString(); - LogicPrinter lp = LogicPrinter.purePrinter(new NotationInfo(), null); - lp.printTaclet(taclet); - description = lp.result() + "\n\n Defined at:" + metaSpace.findOrigin(taclet) - + "\n\n under options:" + taclet.getChoices(); - } - - InfoTreeNode(String title, String description) { - super(title); - altName = null; - this.description = description; - } - - public InfoTreeNode(BuiltInRule br, MetaSpace ruleExplanations) { - this(br.displayName(), ruleExplanations.findDocumentation(br)); - rule = br; - description = "Defined at: " + br.getClass(); - } - - String getTitle() { - return (String) getUserObject(); - } - - /** - * switch title to alternative name (i.e., internal rule name) - */ - void setTitleToAltName() { - assert altName != null; - userObject = altName; - } - - String getDescription() { - return description; - } - - public Rule getRule() { - return rule; - } -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java index 1852e5d9659..b17b83763d3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java @@ -7,50 +7,115 @@ import java.awt.event.ComponentListener; import java.awt.event.MouseAdapter; import java.awt.event.MouseEvent; +import java.util.*; +import java.util.function.Supplier; +import java.util.stream.Collectors; +import java.util.stream.Stream; import javax.swing.*; -import javax.swing.event.TreeSelectionEvent; -import javax.swing.event.TreeSelectionListener; +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.DefaultTreeModel; +import javax.swing.tree.MutableTreeNode; import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.core.KeYSelectionEvent; import de.uka.ilkd.key.core.KeYSelectionListener; -import de.uka.ilkd.key.core.KeYSelectionModel; +import de.uka.ilkd.key.gui.InfoView.InfoNodeFactory.InfoTreeNode; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.extension.api.TabPanel; import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.gui.utilities.LexerHighlighter; +import de.uka.ilkd.key.logic.MetaSpace; +import de.uka.ilkd.key.logic.NamespaceSet; +import de.uka.ilkd.key.logic.label.TermLabelManager; +import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; +import de.uka.ilkd.key.logic.sort.ParametricSortDecl; +import de.uka.ilkd.key.logic.sort.SortAlias; +import de.uka.ilkd.key.pp.LogicPrinter; +import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; -import de.uka.ilkd.key.rule.Rule; -import de.uka.ilkd.key.util.ThreadUtilities; +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.proof.mgt.RuleJustification; +import de.uka.ilkd.key.rule.BuiltInRule; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.util.MiscTools; + +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; +import org.key_project.logic.Choice; +import org.key_project.logic.HasMeta; +import org.key_project.logic.Name; +import org.key_project.logic.Namespace; +import org.key_project.logic.op.Function; +import org.key_project.logic.sort.Sort; +import org.key_project.prover.rules.RuleApp; +import org.key_project.util.collection.ImmutableList; + +import com.google.common.collect.Multimap; +import com.google.common.collect.MultimapBuilder; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; /** * Class for info contents displayed in {@link MainWindow}. * - * @author Kai Wallisch + * @author Kai Wallisch + * @author weigl */ +@NullMarked public class InfoView extends JSplitPane implements TabPanel { - - private static final long serialVersionUID = -6944612837850368411L; public static final Icon INFO_ICON = IconFactory.INFO_VIEW.get(MainWindow.TAB_ICON_SIZE); - private final InfoTree infoTree; - private final InfoViewContentPane contentPane; + private final JTree infoTree = new JTree(); + private final JTextPane contentPane = createInfoArea(); private final ProofDisposedListener proofDisposedListener; - private final KeYSelectionListener selectionListener = new InfoViewSelectionListener(); - private Node lastShownGoalNode; - private MainWindow mainWindow; + private final InfoNodeFactory nodeFactory = new InfoNodeFactory(); + + private LexerHighlighter lexerHighlighter = new LexerHighlighter.KeYLexerHighlighter(); + + + private final KeYSelectionListener selectionListener = new KeYSelectionListener() { + @Override + public void selectedNodeChanged(KeYSelectionEvent e) { + update(); + } + + private void update() { + SwingUtilities.invokeLater(() -> { + if (mediator.getSelectedGoal() != null) { + updateModel(mediator.getSelectedGoal()); + } else if (mediator.getSelectedProof() != null) { + try { + updateModel(mediator.getSelectedProof().openGoals().head()); + } catch (NoSuchElementException ex) { + // nothing possible to do + } + } + }); + } + + public void selectedProofChanged(KeYSelectionEvent e) { + update(); + } + }; + + private @Nullable Node lastShownGoalNode; private KeYMediator mediator; - public InfoView() { + public InfoView(KeYMediator mediator) { super(VERTICAL_SPLIT); + setMediator(mediator); + // initial placement of the divider setDividerLocation(300); @@ -60,18 +125,13 @@ public InfoView() { // Setting a name for this causes PreferenceSaver to include this class. setName("infoViewPane"); - infoTree = new InfoTree(); - infoTree.addTreeSelectionListener(new TreeSelectionListener() { - @Override - public void valueChanged(TreeSelectionEvent e) { - InfoTreeNode node = infoTree.getLastSelectedPathComponent(); - if (node != null) { - contentPane.setNode(node); - } else { - contentPane.clear(); - } - } - }); + + DefaultMutableTreeNode root = new DefaultMutableTreeNode(); + root.add(nodeFactory.create("No proof loaded", + "In this pane, the available logical rules will be displayed and/or explained.")); + infoTree.setModel(new DefaultTreeModel(root)); + infoTree.setShowsRootHandles(true); + infoTree.setRootVisible(false); lastShownGoalNode = null; @@ -122,7 +182,8 @@ public void mousePressed(MouseEvent e) { private void checkPopup(MouseEvent e) { if (e.isPopupTrigger()) { - Rule selected = infoTree.getLastSelectedPathComponent().getRule(); + Object selected = + ((InfoTreeNode) infoTree.getLastSelectedPathComponent()).getUserObject(); JPopupMenu menu = KeYGuiExtensionFacade.createContextMenu( ContextMenuKind.INFO_TREE, selected, mediator); if (menu.getComponentCount() > 0) { @@ -132,26 +193,32 @@ private void checkPopup(MouseEvent e) { } }); - - contentPane = new InfoViewContentPane(); + infoTree.addTreeSelectionListener(e -> { + InfoTreeNode node = (InfoTreeNode) infoTree.getLastSelectedPathComponent(); + if (node != null) { + contentPane.setText(node.getDescription()); + lexerHighlighter.highlightPaneMarkdown(contentPane); + } else { + contentPane.setText(""); + } + }); setLeftComponent(new JScrollPane(infoTree)); - setRightComponent(contentPane); + setRightComponent(new JScrollPane(contentPane)); KeYGuiExtensionFacade.installKeyboardShortcuts(mediator, this, KeYGuiExtension.KeyboardShortcuts.INFO_VIEW); } - public InfoView(MainWindow window, KeYMediator mediator) { - this(); - setMainWindow(window); - setMediator(mediator); - } - + @Override + public void updateUI() { + // create new lexer highlighter for updating dark/light color + lexerHighlighter = new LexerHighlighter.KeYLexerHighlighter(); + super.updateUI(); + } public void setMediator(KeYMediator m) { - assert m != null; if (mediator != null) { mediator.removeKeYSelectionListener(selectionListener); } @@ -159,9 +226,6 @@ public void setMediator(KeYMediator m) { mediator = m; } - public void setMainWindow(MainWindow w) { - mainWindow = w; - } @Override public String getTitle() { @@ -178,53 +242,321 @@ public JComponent getComponent() { return this; } - private void updateModel(Goal g) { + private void updateModel(@Nullable Goal g) { if (g == null || lastShownGoalNode != g.node()) { if (lastShownGoalNode != null) { lastShownGoalNode.proof().removeProofDisposedListener(proofDisposedListener); } - final InfoTreeModel model; if (g != null) { - var metaSpace = g.proof().getServices().getNamespaces().docs(); - model = new InfoTreeModel(g, metaSpace, mainWindow); + infoTree.setModel(new DefaultTreeModel(nodeFactory.createInfoTreeRoot(g))); g.proof().addProofDisposedListener(proofDisposedListener); lastShownGoalNode = g.node(); } else { - model = null; + infoTree.setModel(null); lastShownGoalNode = null; } - contentPane.clear(); - infoTree.setModel(model); + contentPane.setText(""); } } - private class InfoViewSelectionListener implements KeYSelectionListener { + private JTextPane createInfoArea() { + var description = new JTextPane(); + description.setEditable(false); + description.setBorder(BorderFactory.createTitledBorder("")); + description.setCaretPosition(0); + return description; + } + - /** - * focused node has changed - */ - @Override - public void selectedNodeChanged(KeYSelectionEvent e) { + public static class InfoNodeFactory { + private static final String LEMMAS = "Lemmas"; + private static final String TACLET_BASE = "Taclet Base"; + + private static final String COLLECTION = + "This node stands for a category of symbols; expand it to browse the symbols " + + "in the category."; + private static final String DEFAULT_FUNCTIONS_LABEL = + "Display descriptions for documented interpreted function and predicate symbols."; + + + private DefaultMutableTreeNode createInfoTreeRoot(Goal g) { + InfoTreeNode root = create( + "This is the root node of InfoTreeModel. It should not be visible.", ""); + + MetaSpace docs = g.proof().getServices().getNamespaces().docs(); + + root.add(createNodeRules(docs, g)); + root.add(createNodeTermLabels(docs, g.proof())); + final var namespaces = g.getLocalNamespaces(); + root.add(createNodeFunctions(docs, namespaces.functions())); + root.add(createNodeTacletOptions(docs, g.proof().getInitConfig())); + root.add(createNodeChoices(docs, namespaces.choices())); + root.add(createNodeRS("Parametric Funcions", docs, + namespaces.parametricFunctions().allElements())); + root.add(createNodePS(docs, namespaces.parametricSorts().allElements())); + root.add(createNodeRS("Rule Sets", docs, + namespaces.ruleSets().allElements())); + root.add( + createNodeAliases(docs, namespaces.sortAliases().allElements())); + root.add(createNodeRS("Variables", docs, + namespaces.variables().allElements())); + root.add(createNodeRS("Program Variables", docs, + namespaces.programVariables().allElements())); + root.add(createNodeScripts(docs)); + return root; } - /** - * the selected proof has changed (e.g. a new proof has been loaded) - */ - @Override - public void selectedProofChanged(KeYSelectionEvent e) { - final KeYSelectionModel selectionModel = e.getSource(); - Runnable action = () -> { - if (isVisible()) { - if (selectionModel.getSelectedProof() == null) { - updateModel(null); - } else if (selectionModel.getSelectedGoal() != null) { - // keep old view if an inner node has been selected - updateModel(selectionModel.getSelectedGoal()); - } + private MutableTreeNode createNodeAliases(MetaSpace docs, + Collection sortAliases) { + var tlRoot = create("Sort Alias", ""); + for (var alias : sortAliases) { + tlRoot.add(new InfoTreeNode(alias.name().toString(), + () -> "Alias of " + alias.aliasedSort() + "\n" + + docs.findDocumentation(alias.aliasedSort()))); + } + return tlRoot; + } + + private MutableTreeNode createNodeRS(String title, MetaSpace docs, + Collection ruleSets) { + var tlRoot = create(title, ""); + for (var element : ruleSets) { + tlRoot.add( + new InfoTreeNode(element.toString(), () -> docs.findDocumentation(element))); + } + return tlRoot; + } + + private MutableTreeNode createNodePS(MetaSpace docs, @MonotonicNonNull Collection sorts) { + var tlRoot = create("Parametric Sorts", ""); + for (var element : sorts) { + tlRoot.add( + new InfoTreeNode(element.name().toString(), + () -> docs.findDocumentation(element) + "\n\n---\nparams:" + + element.getParameters() + "\n\n---\nextends: " + element.getExtendedSorts() + + "\n\n---\n")); + } + return tlRoot; + } + + private MutableTreeNode createNodePF(MetaSpace docs, + Namespace funcs) { + var tlRoot = create("Parametric Functions", ""); + for (var element : funcs.allElements()) { + tlRoot.add( + new InfoTreeNode(element.toString(), () -> docs.findDocumentation(element))); + } + return tlRoot; + } + + private InfoTreeNode createNodeChoices(MetaSpace docs, Namespace choices) { + var tlRoot = create("Choices", "Browse descriptions for currently available choices"); + Multimap map = + MultimapBuilder.hashKeys().arrayListValues(4).build(); + choices.allElements().forEach((c) -> map.put(c.category(), + new InfoTreeNode(c.name().toString(), () -> docs.findDocumentation(c)))); + for (var s : map.keySet()) { + var cat = new InfoTreeNode(s, + () -> docs.findDocumentation(new HasMeta.OptionCategory(s))); + map.get(s).forEach(cat::add); + tlRoot.add(cat); + } + return tlRoot; + } + + private InfoTreeNode createNodeScripts(MetaSpace docs) { + var tlRoot = create("Proof Script Commands", + "Browse descriptions for currently available proof script commands."); + ProofScriptEngine.loadCommands().forEach((key, value) -> { + tlRoot.add(new InfoTreeNode(key, () -> value.getDocumentation())); + }); + return tlRoot; + } + + private InfoTreeNode createNodeRules(MetaSpace docs, Goal g) { + var tlRoot = create("Rules", "Browse descriptions for currently available rules."); + + List set = + new ArrayList<>(g.ruleAppIndex().tacletIndex().allNoPosTacletApps()); + OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(g.proof()); + if (simplifier != null && !simplifier.isShutdown()) { + set.addAll(simplifier.getCapturedTaclets()); + } + set.sort(Comparator.comparing(RuleApp::displayName)); + + tlRoot.add(createNodeBuiltInRules(docs, g)); + tlRoot.add(createNodeAxiom(docs, + set.stream().filter(it -> { + RuleJustification just = g.proof().mgt().getJustification(it); + return just != null && just.isAxiomJustification(); + }))); + + tlRoot.add(createNodeLemmas(docs, set.stream().filter(it -> { + RuleJustification just = g.proof().mgt().getJustification(it); + return just != null && !just.isAxiomJustification(); + }))); + + return tlRoot; + } + + private MutableTreeNode createNodeBuiltInRules(MetaSpace docs, Goal g) { + InfoTreeNode builtInRoot = create("Built-In", + "Some logical rules are implemented in Java code. This is because their semantics " + + + "cannot easily be expressed in KeY's Taclet language."); + ImmutableList rules = + g.ruleAppIndex().builtInRuleAppIndex().builtInRuleIndex().rules(); + for (BuiltInRule br : rules) { + builtInRoot.add(create(br, docs)); + } + return builtInRoot; + } + + private MutableTreeNode createNodeAxiom(MetaSpace docs, Stream seq) { + InfoTreeNode axiomTacletRoot = create(TACLET_BASE, """ + Most logical rules are implemented as Taclets. + + Taclets are schematic logical rules formulated in the Taclet Language.\s + The language is defined and explained in the KeY book. + """); + Map> ruleAppIndex = new TreeMap<>(); + seq.forEach(it -> ruleAppIndex.computeIfAbsent(it.displayName(), k -> new ArrayList<>()) + .add(it)); + + ruleAppIndex.forEach((key, value) -> { + if (value.size() > 1) { + InfoTreeNode group = create("%s (%d)".formatted(key, value.size()), ""); + axiomTacletRoot.add(group); + value.forEach(it -> group.add(create(it.rule(), docs))); + } else { + value.forEach(it -> axiomTacletRoot.add(create(it.rule(), docs))); } - }; - ThreadUtilities.invokeOnEventQueue(action); + }); + var count = ruleAppIndex.values().stream().mapToInt(List::size).sum(); + axiomTacletRoot.setUserObject("%s (%d)".formatted(TACLET_BASE, count)); + return axiomTacletRoot; } + private MutableTreeNode createNodeLemmas(MetaSpace docs, Stream seq) { + InfoTreeNode proveableTacletsRoot = create(LEMMAS, + """ + Taclets which have been introduced using File->Load User-Defined Taclets are filed here. + + Loading User Defined Taclets opens side branches on which the soundness of the lemma taclets must be established. + """); + seq.forEach(it -> proveableTacletsRoot.add(create(it.rule(), docs))); + return proveableTacletsRoot; + } + + private MutableTreeNode createNodeTermLabels(MetaSpace docs, Proof proof) { + var tlRoot = + create("Term Labels", "Show descriptions for currently available term labels."); + var mgr = TermLabelManager.getTermLabelManager(proof.getServices()); + var factories = mgr.getFactories(); + + var labelNames = new ArrayList<>(factories.keySet()); + labelNames.sort(Comparator.comparing(Name::toString)); + + for (Name name : labelNames) { + tlRoot.add(new InfoTreeNode(name.toString(), + () -> factories.get(name).getDocumentation())); + } + return tlRoot; + } + + private InfoTreeNode createNodeFunctions(MetaSpace docs, + Namespace functions) { + var fnRoot = create("Function Symbols", DEFAULT_FUNCTIONS_LABEL); + var fnByName = create("By Name", DEFAULT_FUNCTIONS_LABEL); + var fnByReturnType = create("By Return Type", DEFAULT_FUNCTIONS_LABEL); + + fnRoot.add(fnByName); + fnRoot.add(fnByReturnType); + + var seq = new ArrayList<>(functions.allElements()); + seq.sort(Comparator.comparing(it -> it.name().toString())); + + var byReturn = new TreeMap>( + Comparator.comparing(it -> it.name().toString())); + + for (var fn : seq) { + var fnName = "%s(%s) : %s".formatted( + fn.name(), + fn.argSorts().stream().map(it -> it.name().toString()) + .collect(Collectors.joining(", ")), + fn.sort().name()); + var fnSort = fn.sort(); + + // flat list: + Supplier stringSupplier = () -> docs.findDocumentation(fn); + fnByName.add(new InfoTreeNode(fnName, stringSupplier)); + + // by return type + byReturn.putIfAbsent(fnSort, new ArrayList<>()); + byReturn.get(fnSort).add(new InfoTreeNode(fnName, stringSupplier)); + } + + for (var entry : byReturn.entrySet()) { + var node = create(entry.getKey().name().toString(), ""); + entry.getValue().forEach(node::add); + fnByReturnType.add(node); + } + + return fnRoot; + } + + private InfoTreeNode createNodeTacletOptions(MetaSpace docs, InitConfig initConfig) { + InfoTreeNode localRoot = + create("Active Taclet Options", "Shows the activated Taclet options"); + for (Choice activatedChoice : initConfig.getActivatedChoices()) { + localRoot.add( + create(activatedChoice.name().toString(), + docs.findDocumentation(activatedChoice))); + } + return localRoot; + } + + + public InfoTreeNode create(Taclet taclet, MetaSpace metaSpace) { + LogicPrinter lp = LogicPrinter.purePrinter(new NotationInfo(), null); + lp.printTaclet(taclet); + String doc = metaSpace.findDocumentation(taclet); + String origin = metaSpace.findOrigin(taclet); + + return create(taclet.name().toString(), + () -> (doc != null ? doc + "\n\n" : "") + + ("```key\n%s\n```\n\n".formatted(lp.result())) + + ("Defined at: %s \n under options: (%s)".formatted(origin, + taclet.getChoices()))); + } + + public InfoTreeNode create(BuiltInRule br, MetaSpace docs) { + var description = "Defined at in Java class" + br.getClass(); + return create(br.displayName(), () -> Stream.of(docs.findDocumentation(br), description) + .filter(Objects::nonNull) + .collect(Collectors.joining("\n\n"))); + } + + public InfoTreeNode create(String title, String description) { + return create(title, () -> description); + } + + public InfoTreeNode create(String title, Supplier description) { + return new InfoTreeNode(title, description); + } + + + public static class InfoTreeNode extends DefaultMutableTreeNode { + private final Supplier<@Nullable String> description; + + public InfoTreeNode(String name, Supplier<@Nullable String> description) { + super(name); + this.description = description; + } + + public @Nullable String getDescription() { + return description.get(); + } + } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoViewContentPane.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoViewContentPane.java deleted file mode 100644 index 3f61f68933e..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoViewContentPane.java +++ /dev/null @@ -1,42 +0,0 @@ -/* 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; - -import javax.swing.BorderFactory; -import javax.swing.JScrollPane; -import javax.swing.JTextArea; - -/** - * This class is used to display descriptions in {@link InfoView}. - * - * @author Kai Wallisch - */ -public class InfoViewContentPane extends JScrollPane { - - /** - * - */ - private static final long serialVersionUID = -7609483136106706196L; - private final JTextArea description; - - InfoViewContentPane() { - description = new JTextArea("", 15, 30); - description.setEditable(false); - description.setLineWrap(true); - description.setWrapStyleWord(true); - setViewportView(description); - } - - public void setNode(InfoTreeNode node) { - setBorder(BorderFactory.createTitledBorder(node.getTitle())); - description.setText(node.getDescription()); - description.setCaretPosition(0); - } - - public void clear() { - setBorder(BorderFactory.createTitledBorder("Description")); - description.setText(""); - } - -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 140604cd34f..8dfe8c28522 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -325,7 +325,7 @@ private MainWindow() { recentFileMenu = new RecentFileMenu(this); proofTreeView = new ProofTreeView(mediator); - infoView = new InfoView(this, mediator); + infoView = new InfoView(mediator); strategySelectionView = new StrategySelectionView(this, mediator); openGoalsView = new GoalList(mediator); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java index 5e24a53fe68..28a93432cbc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java @@ -32,7 +32,7 @@ public class MainWindowTabbedPane extends JTabbedPane { assert mainWindow != null; proofTreeView = new ProofTreeView(mediator); - InfoView infoView = new InfoView(mainWindow, mediator); + InfoView infoView = new InfoView(mediator); StrategySelectionView strategySelectionView = new StrategySelectionView(mainWindow, mediator); GoalList openGoalsView = new GoalList(mediator); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index 5f33d827557..26f8f43abbf 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -332,7 +332,7 @@ public void actionPerformed(ActionEvent actionEvent) { mainWindow.loadProblem(file, pl -> { if (profile != null) { pl.setProfileOfNewProofs(profile); - pl.setAdditionalProfileOptions(additionalProfileOptions); + // pl.setAdditionalProfileOptions(additionalProfileOptions); } pl.setLoadSingleJavaFile(fileEntry.singleJava); }); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index 609bdf7b755..ef81c7451ef 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -104,7 +104,7 @@ public void loadProblem(Path file, Consumer configure) { mainWindow.addRecentFile(file.toAbsolutePath().toString(), problemLoader.getProfileOfNewProofs(), problemLoader.isLoadSingleJavaFile(), - problemLoader.getAdditionalProfileOptions()); + null); problemLoader.runAsynchronously(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java index 2ea3152d913..1166fe79f2b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java @@ -15,6 +15,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.colors.ColorSettings; +import de.uka.ilkd.key.gui.utilities.LexerHighlighter; import de.uka.ilkd.key.pp.*; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -56,7 +57,7 @@ public final class InnerNodeView extends SequentView implements ProofDisposedLis private final InnerNodeViewListener listener; - private JTextArea tacletInfo = new JTextArea(); + private JTextPane tacletInfo = new JTextPane(); private Node node; private final RuleApp ruleApp; @@ -244,9 +245,13 @@ public synchronized void printSequent() { } private void updateTacletInfo() { - tacletInfo.setText( + final var tacletDescription = TacletDescriber.getTacletDescription(getMainWindow().getMediator(), ruleApp, - getLineWidth())); + getLineWidth()); + tacletInfo.setText(tacletDescription); + LexerHighlighter lh = new LexerHighlighter.KeYLexerHighlighter(); + lh.highlightPaneAll(tacletInfo, tacletDescription.indexOf('\n'), -1); + tacletInfo.setBackground(getBackground()); tacletInfo.setBorder(new CompoundBorder(new MatteBorder(3, 0, 0, 0, Color.black), new EmptyBorder(new Insets(4, 0, 0, 0)))); @@ -260,7 +265,7 @@ public void makeTacletInfoVisible(boolean visible) { tacletInfo.setVisible(visible); } - public JTextArea getTacletInfo() { + public JTextPane getTacletInfo() { return tacletInfo; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java new file mode 100644 index 00000000000..ee5fec76695 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java @@ -0,0 +1,202 @@ +/* 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.utilities; + +import java.awt.*; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import javax.swing.*; +import javax.swing.text.*; + +import de.uka.ilkd.key.gui.colors.ColorSettings; +import de.uka.ilkd.key.nparser.ParsingFacade; + +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.Token; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.nparser.JavaKeYLexer.*; + +/** + * Utilities for highlighting of text based on ANTLR-based Lexers. + * + * @author Alexander Weigl + * @version 1 (2/17/26) + */ +@NullMarked +public abstract class LexerHighlighter { + protected abstract @Nullable AttributeSet getStyle(int tokenType); + + private final StyleContext styleContext = new StyleContext(); + + protected AttributeSet define(Color fgColor, boolean bold, boolean italic) { + AttributeSet aset = + styleContext.addAttribute(SimpleAttributeSet.EMPTY, StyleConstants.Foreground, fgColor); + aset = styleContext.addAttribute(aset, StyleConstants.FontFamily, Font.MONOSPACED); + aset = styleContext.addAttribute(aset, StyleConstants.Bold, bold); + aset = styleContext.addAttribute(aset, StyleConstants.Italic, italic); + return aset; + } + + public final void highlightPaneMarkdown(JTextPane contentPane) { + String text = contentPane.getText(); + Pattern pattern = getMarkdownPattern(); + + Matcher match = pattern.matcher(text); + var sd = contentPane.getStyledDocument(); + + var prefixLength = getPatternPrefixLength(); + while (match.find()) { + var lexer = ParsingFacade.createLexer(CharStreams.fromString(match.group(1))); + var toks = lexer.getAllTokens(); + int startIdx = match.start() + prefixLength; + for (var tok : toks) { + highlightToken(sd, startIdx, tok); + } + } + contentPane.invalidate(); + contentPane.repaint(); + contentPane.repaint(); + } + + protected abstract int getPatternPrefixLength(); + + public final void highlightPaneAll(JTextPane contentPane, int startIdx, int stopIdx) { + String text = contentPane.getText(); + + if (stopIdx < 0) { + stopIdx = text.length(); + } + + text = text.substring(startIdx, stopIdx); + + var sd = contentPane.getStyledDocument(); + var lexer = ParsingFacade.createLexer(CharStreams.fromString(text)); + var toks = lexer.getAllTokens(); + for (var tok : toks) { + highlightToken(sd, startIdx, tok); + } + contentPane.invalidate(); + contentPane.repaint(); + contentPane.repaint(); + } + + public final void highlightPaneAll(JTextPane contentPane) { + highlightPaneAll(contentPane, 0, -1); + } + + + private void highlightToken(StyledDocument sd, int startIdx, Token tok) { + var attribute = getStyle(tok.getType()); + sd.setCharacterAttributes(startIdx + tok.getStartIndex(), + 1 + tok.getStopIndex() - tok.getStartIndex(), + attribute, true); + } + + protected abstract Pattern getMarkdownPattern(); + + public static class KeYLexerHighlighter extends LexerHighlighter { + public static final ColorSettings.ColorProperty COLOR_KEYWORD = + ColorSettings.define("infotree.syntax.keyword", "", Color.BLUE, Color.ORANGE); + + public static final ColorSettings.ColorProperty COLOR_IDENTIFIER = + ColorSettings.define("infotree.syntax.identifier", "", Color.BLACK, Color.WHITE); + + public static final ColorSettings.ColorProperty COLOR_COMMENT = + ColorSettings.define("infotree.syntax.comment", "", Color.GREEN, Color.GREEN); + + public static final ColorSettings.ColorProperty COLOR_OPERATORS = + ColorSettings.define("infotree.syntax.operators", "", Color.BLACK, Color.ORANGE); + + public static final ColorSettings.ColorProperty COLOR_ERROR = + ColorSettings.define("infotree.syntax.error", "", Color.RED, Color.WHITE); + + public static final ColorSettings.ColorProperty COLOR_LITERALS = + ColorSettings.define("infotree.syntax.literals", "", Color.GREEN, Color.GREEN); + + public static final ColorSettings.ColorProperty COLOR_MODALITY = + ColorSettings.define("infotree.syntax.modality", "", Color.PINK, Color.PINK); + + + private final AttributeSet STYLE_OPERATORS = define(COLOR_OPERATORS.get(), false, false); + private final AttributeSet STYLE_ERROR = define(COLOR_ERROR.get(), false, false); + private final AttributeSet STYLE_LITERALS = define(COLOR_LITERALS.get(), false, true); + private final AttributeSet STYLE_KEYWORDS = define(COLOR_KEYWORD.get(), true, false); + private final AttributeSet STYLE_IDENTIFIER = define(COLOR_IDENTIFIER.get(), true, false); + private final AttributeSet STYLE_COMMENT = define(COLOR_COMMENT.get(), false, true); + private final AttributeSet STYLE_MODALITY = define(COLOR_COMMENT.get(), false, true); + private final AttributeSet STYLE_DEFAULT = define(COLOR_IDENTIFIER.get(), false, false); + + + @Override + protected @Nullable AttributeSet getStyle(int tokType) { + return switch (tokType) { + case TERMLABEL, MODIFIABLE, PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, + HAS_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, IS_FINAL, CONTAINERTYPE, + SCHEMAVAR, FORMULA, + COMMENT_END, DOC_COMMENT, ML_COMMENT, MODALITYD, MODALITYB, + MODALITYBB, MODAILITYGENERIC1, MODAILITYGENERIC2, MODAILITYGENERIC3, + MODAILITYGENERIC4, MODAILITYGENERIC5, MODAILITYGENERIC6, MODAILITYGENERIC7, + MODALITYD_END, MODALITYD_STRING, MODALITYD_CHAR, MODALITYG_END, + MODALITYB_END, MODALITYBB_END, MODALOPERATOR, PROGRAM -> + STYLE_KEYWORDS; + + case MODALITY -> STYLE_MODALITY; + + case AT, PARALLEL, OR, AND, NOT, IMP, + EQUALS, NOT_EQUALS, SEQARROW, EXP, TILDE, PERCENT, + STAR, MINUS, PLUS, GREATER, GREATEREQUAL, + LESS, LESSEQUAL, LGUILLEMETS, RGUILLEMETS, EQV, + UTF_PRECEDES, UTF_IN, UTF_EMPTY, UTF_UNION, UTF_INTERSECT, + UTF_SUBSET_EQ, UTF_SUBSEQ, UTF_SETMINUS, SEMI, SLASH, + COLON, DOUBLECOLON, ASSIGN, DOT, DOTRANGE, COMMA, + LPAREN, RPAREN, LBRACE, RBRACE, LBRACKET, RBRACKET, + EMPTYBRACKETS -> + STYLE_OPERATORS; + case ERROR_UKNOWN_ESCAPE, ERROR_CHAR -> STYLE_ERROR; + case IDENT -> STYLE_IDENTIFIER; + case COMMENT, SL_COMMENT -> STYLE_COMMENT; + case CHAR_LITERAL, QUOTED_STRING_LITERAL, TRUE, FALSE, + STRING_LITERAL, BIN_LITERAL, HEX_LITERAL, INT_LITERAL, FLOAT_LITERAL, + DOUBLE_LITERAL, REAL_LITERAL -> + STYLE_LITERALS; + default -> STYLE_DEFAULT; + }; + } + + @Override + protected int getPatternPrefixLength() { + return "```key".length(); + } + + @Override + protected Pattern getMarkdownPattern() { + return Pattern.compile("```key(.*?)```", + Pattern.MULTILINE | Pattern.DOTALL | Pattern.CASE_INSENSITIVE); + } + } +}