Fix for #3683: Hiding package prefixes in sequent view

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();
     }
 
     /**

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;
         }

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 {

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);
     }

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<Object, Notation> 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();

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();
     }

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));
     }