diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java index 3a10756d56e..88fc3194a76 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java @@ -46,7 +46,7 @@ public LoopInvariantBuiltInRuleApp getAppliedRuleApp() { @Override protected String lazyComputeName() { return getLoopInvariant().getPlainText(getServices(), getAppliedRuleApp().getHeapContext(), - getSettings().usePrettyPrinting(), getSettings().useUnicode()).trim(); + getSettings().usePrettyPrinting(), getSettings().useUnicode(), false).trim(); } /** diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java index 516e7904a5c..741fdf95ce5 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java @@ -131,7 +131,8 @@ protected String lazyComputeName() throws ProofInputException { // Compute contract text return FunctionalOperationContractImpl.getText(contract, contractParams, resultTerm, selfTerm, exceptionTerm, baseHeap, baseHeapTerm, heapContext, atPres, false, - services, getSettings().usePrettyPrinting(), getSettings().useUnicode()).trim(); + services, getSettings().usePrettyPrinting(), getSettings().useUnicode(), + false).trim(); } else { return null; } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java index a688d5aa657..99590025ec6 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java @@ -3949,7 +3949,7 @@ public static String formatTerm(JTerm term, Services services, boolean useUnicod if ((useUnicode || usePrettyPrinting) && services != null) { NotationInfo ni = new NotationInfo(); LogicPrinter logicPrinter = LogicPrinter.purePrinter(ni, services); - logicPrinter.getNotationInfo().refresh(services, usePrettyPrinting, useUnicode); + logicPrinter.getNotationInfo().refresh(services, usePrettyPrinting, useUnicode, false); logicPrinter.printTerm(term); return logicPrinter.result(); } else { 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..2a2b1ba5ecf 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 @@ -133,10 +133,11 @@ public PosTableLayouter layouter() { } public static SequentViewLogicPrinter quickPrinter(Services services, - boolean usePrettyPrinting, boolean useUnicodeSymbols) { + boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { final NotationInfo ni = new NotationInfo(); if (services != null) { - ni.refresh(services, usePrettyPrinting, useUnicodeSymbols); + ni.refresh(services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); } // Use a SequentViewLogicPrinter instead of a plain LogicPrinter, @@ -154,7 +155,7 @@ public static SequentViewLogicPrinter quickPrinter(Services services, */ public static String quickPrintTerm(JTerm t, Services services) { return quickPrintTerm(t, services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX); } /** @@ -164,11 +165,12 @@ public static String quickPrintTerm(JTerm t, Services services) { * @param services services. * @param usePrettyPrinting whether to use pretty-printing. * @param useUnicodeSymbols whether to use unicode symbols. + * @param hidePackagePrefix * @return the printed term. */ public static String quickPrintTerm(JTerm t, Services services, boolean usePrettyPrinting, - boolean useUnicodeSymbols) { - var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols); + boolean useUnicodeSymbols, boolean hidePackagePrefix) { + var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); p.printTerm(t); return p.result(); } @@ -182,7 +184,7 @@ public static String quickPrintTerm(JTerm t, Services services, boolean usePrett */ public static String quickPrintSemisequent(Semisequent s, Services services) { var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX); p.printSemisequent(s); return p.result(); } @@ -196,7 +198,7 @@ public static String quickPrintSemisequent(Semisequent s, Services services) { */ public static String quickPrintSequent(Sequent s, Services services) { var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX); p.printSequent(s); return p.result(); } @@ -616,7 +618,7 @@ protected void printSchemaVariable(SchemaVariable sv) { private void printSourceElement(SourceElement element) { new PrettyPrinter(layouter, instantiations, services, notationInfo.isPrettySyntax(), - notationInfo.isUnicodeEnabled()).print(element); + notationInfo.isUnicodeEnabled(), notationInfo.isHidePackagePrefix()).print(element); } /** @@ -936,19 +938,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 +995,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..bfffbe983f8 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 @@ -146,7 +146,14 @@ public NotationInfo() { this.notationTable = createDefaultNotation(); } - + public NotationInfo(boolean prettySyntax, boolean unicodeEnabled, boolean hidePackagePrefix) { + this.notationTable = createDefaultNotation(); + this.prettySyntax = prettySyntax; + this.unicodeEnabled = unicodeEnabled; + this.hidePackagePrefix = hidePackagePrefix; + // TODO: Do we need this in addition? + // this.finalImmutable = finalImmutable; + } // ------------------------------------------------------------------------- // internal methods @@ -405,12 +412,15 @@ private HashMap createUnicodeNotation(Services services) { // ------------------------------------------------------------------------- public void refresh(Services services) { - refresh(services, DEFAULT_PRETTY_SYNTAX, DEFAULT_UNICODE_ENABLED); + refresh(services, DEFAULT_PRETTY_SYNTAX, DEFAULT_UNICODE_ENABLED, + DEFAULT_HIDE_PACKAGE_PREFIX); } - public void refresh(Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols) { + public void refresh(Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { this.unicodeEnabled = useUnicodeSymbols; this.prettySyntax = usePrettyPrinting; + this.hidePackagePrefix = hidePackagePrefix; if (usePrettyPrinting && services != null) { if (useUnicodeSymbols) { this.notationTable = createUnicodeNotation(services); @@ -420,7 +430,6 @@ public void refresh(Services services, boolean usePrettyPrinting, boolean useUni } else { this.notationTable = createDefaultNotation(); } - hidePackagePrefix = DEFAULT_HIDE_PACKAGE_PREFIX; if (services != null && services.getProof() != null) { ProofSettings settings = services.getProof().getSettings(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index df7141b3eea..8b3c47dd313 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -71,21 +71,23 @@ public class PrettyPrinter implements Visitor { private final SVInstantiations instantiations; private final @Nullable Services services; - private boolean usePrettyPrinting; - private boolean useUnicodeSymbols; + private final boolean usePrettyPrinting; + private final boolean useUnicodeSymbols; + private final boolean hidePackagePrefix; /** creates a new PrettyPrinter */ public PrettyPrinter(PosTableLayouter out) { - this(out, SVInstantiations.EMPTY_SVINSTANTIATIONS, null, true, true); + this(out, SVInstantiations.EMPTY_SVINSTANTIATIONS, null, true, true, true); } public PrettyPrinter(PosTableLayouter o, SVInstantiations svi, @Nullable Services services, - boolean usePrettyPrinting, boolean useUnicodeSymbols) { + boolean usePrettyPrinting, boolean useUnicodeSymbols, boolean hidePackagePrefix) { this.layouter = o; this.instantiations = svi; this.services = services; this.usePrettyPrinting = usePrettyPrinting; this.useUnicodeSymbols = useUnicodeSymbols; + this.hidePackagePrefix = hidePackagePrefix; } /** @@ -1991,7 +1993,8 @@ public void performActionOnSetStatement(SetStatement x) { } public String printInLogicPrinter(JTerm t) { - var lp = LogicPrinter.quickPrinter(services, usePrettyPrinting, useUnicodeSymbols); + var lp = LogicPrinter.quickPrinter(services, usePrettyPrinting, useUnicodeSymbols, + hidePackagePrefix); lp.printTerm(t); return lp.result(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 0db5b7fd9f5..d777934fe67 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -873,7 +873,7 @@ private static String printSequent(Sequent val, Services services) { private static LogicPrinter createLogicPrinter(Services serv, boolean shortAttrNotation) { - final NotationInfo ni = new NotationInfo(); + final NotationInfo ni = new NotationInfo(false, false, false); return LogicPrinter.purePrinter(ni, (shortAttrNotation ? serv : null)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java index d503b51932c..96e56aa3935 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java @@ -658,7 +658,8 @@ private String getText(boolean includeHtmlMarkup, Services services) { hasMby(), originalMby, originalModifiables, hasRealModifiable, globalDefs, originalPres, originalFreePres, originalPosts, originalFreePosts, originalAxioms, getModalityKind(), transactionApplicableContract(), includeHtmlMarkup, services, - NotationInfo.DEFAULT_PRETTY_SYNTAX, NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_PRETTY_SYNTAX, NotationInfo.DEFAULT_UNICODE_ENABLED, + NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX); } public static String getText(FunctionalOperationContract contract, @@ -666,7 +667,8 @@ public static String getText(FunctionalOperationContract contract, JTerm excTerm, LocationVariable baseHeap, JTerm baseHeapTerm, List heapContext, Map atPres, boolean includeHtmlMarkup, Services services, - boolean usePrettyPrinting, boolean useUnicodeSymbols) { + boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { Operator originalSelfVar = contractSelf != null ? contractSelf.op() : null; Operator originalResultVar = resultTerm != null ? resultTerm.op() : null; final TermBuilder tb = services.getTermBuilder(); @@ -747,14 +749,14 @@ public static String getText(FunctionalOperationContract contract, hasRealModifiable, globalDefs, originalPres, originalFreePres, originalPosts, originalFreePosts, originalAxioms, contract.getModalityKind(), contract.transactionApplicableContract(), includeHtmlMarkup, services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); } private static String getSignatureText(IProgramMethod pm, Operator originalResultVar, Operator originalSelfVar, ImmutableList originalParamVars, LocationVariable originalExcVar, Services services, boolean usePrettyPrinting, - boolean useUnicodeSymbols) { + boolean useUnicodeSymbols, boolean hidePackagePrefix) { final StringBuilder sig = new StringBuilder(); if (originalResultVar != null) { sig.append(originalResultVar); @@ -774,7 +776,7 @@ private static String getSignatureText(IProgramMethod pm, Operator originalResul sig.append(named.name()).append(", "); } else if (subst instanceof JTerm) { sig.append(LogicPrinter.quickPrintTerm((JTerm) subst, services, usePrettyPrinting, - useUnicodeSymbols)).append(", "); + useUnicodeSymbols, hidePackagePrefix)).append(", "); } else { sig.append(subst).append(", "); } @@ -793,13 +795,15 @@ private static String getSignatureText(IProgramMethod pm, Operator originalResul private static String printClauseText(final String text, boolean includeHtmlMarkup, - Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols, String clause, - LocationVariable h, final JTerm clauseTerm) { + Services services, String clause, LocationVariable h, + final JTerm clauseTerm, boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); final LocationVariable baseHeap = heapLDT.getHeap(); String printClause = - LogicPrinter.quickPrintTerm(clauseTerm, services, usePrettyPrinting, useUnicodeSymbols); + LogicPrinter.quickPrintTerm(clauseTerm, services, usePrettyPrinting, useUnicodeSymbols, + hidePackagePrefix); clause = clause + (includeHtmlMarkup ? "
" : "\n") + text + (h == baseHeap ? "" : "[" + h + "]") + (includeHtmlMarkup ? " " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(printClause, false) @@ -809,7 +813,8 @@ private static String printClauseText(final String text, boolean includeHtmlMark private static String getClauseText(final String text, Map originalClause, boolean includeHtmlMarkup, - Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols) { + Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { String clause = ""; final TermBuilder tb = services.getTermBuilder(); final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); @@ -818,21 +823,23 @@ private static String getClauseText(final String text, JTerm clauseTerm = originalClause.get(h); if (clauseTerm != null && !clauseTerm.equals(tb.tt())) { clauseTerm = includeHtmlMarkup ? tb.unlabelRecursive(clauseTerm) : clauseTerm; - clause = printClauseText(text, includeHtmlMarkup, services, usePrettyPrinting, - useUnicodeSymbols, clause, h, clauseTerm); + clause = printClauseText(text, includeHtmlMarkup, services, clause, h, clauseTerm, + usePrettyPrinting, + useUnicodeSymbols, hidePackagePrefix); } } return clause; } private static String getGlobalUpdatesText(JTerm globalDefs, boolean includeHtmlMarkup, - Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols) { + Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { String globalUpdates = ""; final TermBuilder tb = services.getTermBuilder(); if (globalDefs != null) { globalDefs = includeHtmlMarkup ? tb.unlabelRecursive(globalDefs) : globalDefs; final String printUpdates = LogicPrinter.quickPrintTerm(globalDefs, services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); globalUpdates = (includeHtmlMarkup ? "
" : "\n") + "defs" + (includeHtmlMarkup ? " " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(printUpdates, false) @@ -843,7 +850,8 @@ private static String getGlobalUpdatesText(JTerm globalDefs, boolean includeHtml private static String getModifiableText(Map originalModifiables, Map hasRealModifiable, boolean includeHtmlMarkup, - Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols) { + Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { String modifiables = ""; final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); @@ -851,8 +859,9 @@ private static String getModifiableText(Map originalMod final JTerm modifiableTerm = originalModifiables.get(h); if (modifiableTerm != null) { modifiables = - printClauseText("modifiable", includeHtmlMarkup, services, usePrettyPrinting, - useUnicodeSymbols, modifiables, h, modifiableTerm); + printClauseText("modifiable", includeHtmlMarkup, services, modifiables, h, + modifiableTerm, usePrettyPrinting, + useUnicodeSymbols, hidePackagePrefix); if (!hasRealModifiable.get(h)) { modifiables = modifiables + (includeHtmlMarkup ? "" : "") + ", creates no new objects" @@ -865,12 +874,13 @@ private static String getModifiableText(Map originalMod private static String getPostText(Map originalPosts, Map originalAxioms, boolean includeHtmlMarkup, - Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols) { + Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { String posts = getClauseText("post", originalPosts, includeHtmlMarkup, services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); if (originalAxioms != null) { posts = posts + getClauseText("axiom", originalAxioms, includeHtmlMarkup, services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); } return posts; } @@ -887,33 +897,34 @@ private static String getText(IProgramMethod pm, Operator originalResultVar, Map originalAxioms, JModality.JavaModalityKind modalityKind, boolean transaction, boolean includeHtmlMarkup, Services services, boolean usePrettyPrinting, - boolean useUnicodeSymbols) { + boolean useUnicodeSymbols, boolean hidePackagePrefix) { final String sig = getSignatureText(pm, originalResultVar, originalSelfVar, - originalParamVars, originalExcVar, services, usePrettyPrinting, useUnicodeSymbols); + originalParamVars, originalExcVar, services, usePrettyPrinting, useUnicodeSymbols, + hidePackagePrefix); final String mby = hasMby ? LogicPrinter.quickPrintTerm(originalMby, services, usePrettyPrinting, - useUnicodeSymbols) + useUnicodeSymbols, hidePackagePrefix) : null; final String modifiables = getModifiableText(originalModifiables, hasRealModifiable, includeHtmlMarkup, - services, usePrettyPrinting, useUnicodeSymbols); + services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); final String globalUpdates = getGlobalUpdatesText(globalDefs, includeHtmlMarkup, services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); final String pres = getClauseText("pre", originalPres, includeHtmlMarkup, services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); final String freePres = getClauseText("free pre", originalFreePres, includeHtmlMarkup, - services, usePrettyPrinting, useUnicodeSymbols); + services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); final String freePosts = getClauseText("free post", originalFreePosts, includeHtmlMarkup, - services, usePrettyPrinting, useUnicodeSymbols); + services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); final String posts = getPostText(originalPosts, originalAxioms, includeHtmlMarkup, services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); final String clauses = globalUpdates + pres + freePres + posts + freePosts + modifiables; if (includeHtmlMarkup) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java index 585d16c59ec..ede7bedf083 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java @@ -449,17 +449,20 @@ public String toString() { * @param services the services object * @param usePrettyPrinting determines whether we get pretty or raw text * @param useUnicodeSymbols determines whether unicode will be used + * @param hidePackagePrefix * @return the plain text representation as a string */ public String getPlainText(Services services, boolean usePrettyPrinting, - boolean useUnicodeSymbols) { + boolean useUnicodeSymbols, boolean hidePackagePrefix) { final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); - return getPlainText(services, heapLDT.getAllHeaps(), usePrettyPrinting, useUnicodeSymbols); + return getPlainText(services, heapLDT.getAllHeaps(), usePrettyPrinting, useUnicodeSymbols, + hidePackagePrefix); } @Override public String getPlainText(Services services, Iterable heapContext, - boolean usePrettyPrinting, boolean useUnicodeSymbols) { + boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix) { final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); final LocationVariable baseHeap = heapLDT.getHeap(); @@ -467,7 +470,7 @@ public String getPlainText(Services services, Iterable heapCon for (LocationVariable h : heapContext) { if (originalModifiable.get(h) != null) { String printMods = LogicPrinter.quickPrintTerm(originalModifiable.get(h), services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); mods.append("\n").append("mod").append(h == baseHeap ? "" : "[" + h + "]") .append(": ").append(printMods); } @@ -477,7 +480,7 @@ public String getPlainText(Services services, Iterable heapCon for (LocationVariable h : heapContext) { if (originalInvariants.get(h) != null) { String printPosts = LogicPrinter.quickPrintTerm(originalInvariants.get(h), services, - usePrettyPrinting, useUnicodeSymbols); + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); invariants.append("\n").append("invariant") .append(h == baseHeap ? "" : "[" + h + "]").append(": ").append(printPosts); } @@ -485,7 +488,7 @@ public String getPlainText(Services services, Iterable heapCon return invariants + (originalVariant != null ? ";\nvariant: " + LogicPrinter.quickPrintTerm(originalVariant, services, - usePrettyPrinting, useUnicodeSymbols) + usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix) : ";") + mods; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java index df2487a68dc..90b8e3b865b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java @@ -291,10 +291,12 @@ LoopSpecification setInvariant(Map invariants, * @param heapContext all corresponding heaps. * @param usePrettyPrinting whether the text should be pretty-printed. * @param useUnicodeSymbols whether Unicode symbols should be used. + * @param hidePackagePrefix * @return a String containing the plain text representation of this invariant. */ String getPlainText(Services services, Iterable heapContext, - boolean usePrettyPrinting, boolean useUnicodeSymbols); + boolean usePrettyPrinting, boolean useUnicodeSymbols, + boolean hidePackagePrefix); String getUniqueName(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java index b811423c95e..ec421276dee 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java @@ -709,7 +709,7 @@ private static String printTerm(KeYMediator mediator, JTerm term) { final JTerm t = TermLabelManager.removeIrrelevantLabels(term, services); LogicPrinter p = LogicPrinter.purePrinter(ni, services); boolean pretty = mediator.getNotationInfo().isPrettySyntax(); - ni.refresh(services, pretty, false); + ni.refresh(services, pretty, false, false); Map tbl = ni.getNotationTable(); if (pretty) { 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)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java index 4a03a6caa76..85aab39670a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java @@ -699,7 +699,7 @@ private class TermView extends SequentView { final NotationInfo ni = new NotationInfo(); if (services != null) { ni.refresh(services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX); } setLogicPrinter(new TermViewLogicPrinter(pos, ni, services)); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFormula.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFormula.java index 2cd155d6fb1..befd2ba1d1a 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFormula.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFormula.java @@ -74,7 +74,8 @@ public String toString(boolean abbreviated, boolean omitBranch) { (JTerm) formula.formula(), services, true, // pretty print - true // using unicode symbols + true, // using unicode symbols + true // hide package prefix ).trim(); if (!omitBranch) { term = term + branchLocation.toString();