From b08bdb6d573e4245f11b4828d71d8f041ae278f1 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 12 Nov 2025 18:12:26 +0100 Subject: [PATCH 1/2] fix view option 'Hide Package Prefix', highlight 'instance' function --- .../java/de/uka/ilkd/key/pp/LogicPrinter.java | 33 +++++++++++++++---- .../java/de/uka/ilkd/key/pp/NotationInfo.java | 4 ++- .../gui/nodeviews/HTMLSyntaxHighlighter.java | 4 +-- 3 files changed, 31 insertions(+), 10 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 4602204a739..3ce7752089c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -936,19 +936,32 @@ && getNotationInfo().isHidePackagePrefix()) { } else { String name = t.op().name().toString(); layouter.startTerm(t.arity()); - boolean alreadyPrinted = false; + if (t.op() instanceof SortDependingFunction op) { - if (op.getKind().compareTo(JavaDLTheory.EXACT_INSTANCE_NAME) == 0) { - layouter.print(op.getSortDependingOn().declarationString()); + + // remove package prefix from SortDependingFunction + if (notationInfo.isHidePackagePrefix()) { + String sort = op.getSortDependingOn().declarationString(); + int index = sort.lastIndexOf('.'); + sort = sort.substring(index + 1); + layouter.print(sort); layouter.print("::"); - layouter.keyWord(op.getKind().toString()); - alreadyPrinted = true; + + name = op.getKind().toString(); + } + + // mark instance and exactInstance as keywords + if (op.getKind().compareTo(JavaDLTheory.EXACT_INSTANCE_NAME) == 0 + || op.getKind().compareTo(JavaDLTheory.INSTANCE_NAME) == 0) { + isKeyword = true; } } if (isKeyword) { layouter.markStartKeyword(); } - if (!alreadyPrinted) { + if (isKeyword) { + layouter.keyWord(name); + } else { layouter.print(name); } if (isKeyword) { @@ -980,7 +993,13 @@ public void printCast(String pre, String post, JTerm t, int ass) { layouter.startTerm(t.arity()); layouter.print(pre); - layouter.print(cast.getSortDependingOn().toString()); + String sort = cast.getSortDependingOn().toString(); + // remove package prefix from sort name + if (notationInfo.isHidePackagePrefix()) { + int index = sort.lastIndexOf('.'); + sort = sort.substring(index + 1); + } + layouter.print(sort); layouter.print(post); maybeParens(t.sub(0), ass); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java index e124f39f0cc..cd99da9ce43 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java @@ -11,6 +11,7 @@ import de.uka.ilkd.key.ldt.*; import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.util.UnicodeHelper; @@ -420,7 +421,8 @@ public void refresh(Services services, boolean usePrettyPrinting, boolean useUni } else { this.notationTable = createDefaultNotation(); } - hidePackagePrefix = DEFAULT_HIDE_PACKAGE_PREFIX; + ProofIndependentSettings pis = ProofIndependentSettings.DEFAULT_INSTANCE; + hidePackagePrefix = pis.getViewSettings().isHidePackagePrefix(); if (services != null && services.getProof() != null) { ProofSettings settings = services.getProof().getSettings(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java index 6ddea51c6ef..8fb30c3d642 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java @@ -76,8 +76,8 @@ public class HTMLSyntaxHighlighter { private final static String[] DYNAMIC_LOGIC_KEYWORDS = { "\\forall", "\\exists", "TRUE", "FALSE", "\\if", "\\then", "\\else", "\\sum", "bsum", - "\\in", "exactInstance", "wellFormed", "measuredByEmpty", "", "", "\\cup", - "" + FORALL, "" + EXISTS, "" + IN, "" + EMPTY }; + "\\in", "instance", "exactInstance", "wellFormed", "measuredByEmpty", "", + "", "\\cup", "" + FORALL, "" + EXISTS, "" + IN, "" + EMPTY }; private final static String DYNAMIC_LOGIC_KEYWORDS_REGEX = concat("|", Arrays.asList(DYNAMIC_LOGIC_KEYWORDS), input -> Pattern.quote((String) input)); From c47ef231f04c3a5f225b8be7c57493a409fc8ac2 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 12 Nov 2025 18:46:13 +0100 Subject: [PATCH 2/2] formatting --- key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 3ce7752089c..92230ca0a0c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -952,7 +952,7 @@ && getNotationInfo().isHidePackagePrefix()) { // mark instance and exactInstance as keywords if (op.getKind().compareTo(JavaDLTheory.EXACT_INSTANCE_NAME) == 0 - || op.getKind().compareTo(JavaDLTheory.INSTANCE_NAME) == 0) { + || op.getKind().compareTo(JavaDLTheory.INSTANCE_NAME) == 0) { isKeyword = true; } }