Skip to content

Commit de6e44b

Browse files
wadoonwadoon
authored
Fix for #3683: Hiding package prefixes in sequent view (#3684)
2 parents 8cc1e8e + ed2ca04 commit de6e44b

14 files changed

Lines changed: 119 additions & 68 deletions

File tree

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ public LoopInvariantBuiltInRuleApp getAppliedRuleApp() {
4646
@Override
4747
protected String lazyComputeName() {
4848
return getLoopInvariant().getPlainText(getServices(), getAppliedRuleApp().getHeapContext(),
49-
getSettings().usePrettyPrinting(), getSettings().useUnicode()).trim();
49+
getSettings().usePrettyPrinting(), getSettings().useUnicode(), false).trim();
5050
}
5151

5252
/**

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,8 @@ protected String lazyComputeName() throws ProofInputException {
131131
// Compute contract text
132132
return FunctionalOperationContractImpl.getText(contract, contractParams, resultTerm,
133133
selfTerm, exceptionTerm, baseHeap, baseHeapTerm, heapContext, atPres, false,
134-
services, getSettings().usePrettyPrinting(), getSettings().useUnicode()).trim();
134+
services, getSettings().usePrettyPrinting(), getSettings().useUnicode(),
135+
false).trim();
135136
} else {
136137
return null;
137138
}

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3949,7 +3949,7 @@ public static String formatTerm(JTerm term, Services services, boolean useUnicod
39493949
if ((useUnicode || usePrettyPrinting) && services != null) {
39503950
NotationInfo ni = new NotationInfo();
39513951
LogicPrinter logicPrinter = LogicPrinter.purePrinter(ni, services);
3952-
logicPrinter.getNotationInfo().refresh(services, usePrettyPrinting, useUnicode);
3952+
logicPrinter.getNotationInfo().refresh(services, usePrettyPrinting, useUnicode, false);
39533953
logicPrinter.printTerm(term);
39543954
return logicPrinter.result();
39553955
} else {

‎key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java‎

Lines changed: 36 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -133,10 +133,11 @@ public PosTableLayouter layouter() {
133133
}
134134

135135
public static SequentViewLogicPrinter quickPrinter(Services services,
136-
boolean usePrettyPrinting, boolean useUnicodeSymbols) {
136+
boolean usePrettyPrinting, boolean useUnicodeSymbols,
137+
boolean hidePackagePrefix) {
137138
final NotationInfo ni = new NotationInfo();
138139
if (services != null) {
139-
ni.refresh(services, usePrettyPrinting, useUnicodeSymbols);
140+
ni.refresh(services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix);
140141
}
141142

142143
// Use a SequentViewLogicPrinter instead of a plain LogicPrinter,
@@ -154,7 +155,7 @@ public static SequentViewLogicPrinter quickPrinter(Services services,
154155
*/
155156
public static String quickPrintTerm(JTerm t, Services services) {
156157
return quickPrintTerm(t, services, NotationInfo.DEFAULT_PRETTY_SYNTAX,
157-
NotationInfo.DEFAULT_UNICODE_ENABLED);
158+
NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX);
158159
}
159160

160161
/**
@@ -164,11 +165,12 @@ public static String quickPrintTerm(JTerm t, Services services) {
164165
* @param services services.
165166
* @param usePrettyPrinting whether to use pretty-printing.
166167
* @param useUnicodeSymbols whether to use unicode symbols.
168+
* @param hidePackagePrefix
167169
* @return the printed term.
168170
*/
169171
public static String quickPrintTerm(JTerm t, Services services, boolean usePrettyPrinting,
170-
boolean useUnicodeSymbols) {
171-
var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols);
172+
boolean useUnicodeSymbols, boolean hidePackagePrefix) {
173+
var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix);
172174
p.layouter().beginC();
173175
p.printTerm(t);
174176
p.layouter().end();
@@ -184,7 +186,7 @@ public static String quickPrintTerm(JTerm t, Services services, boolean usePrett
184186
*/
185187
public static String quickPrintSemisequent(Semisequent s, Services services) {
186188
var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX,
187-
NotationInfo.DEFAULT_UNICODE_ENABLED);
189+
NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX);
188190
p.printSemisequent(s);
189191
return p.result();
190192
}
@@ -198,7 +200,7 @@ public static String quickPrintSemisequent(Semisequent s, Services services) {
198200
*/
199201
public static String quickPrintSequent(Sequent s, Services services) {
200202
var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX,
201-
NotationInfo.DEFAULT_UNICODE_ENABLED);
203+
NotationInfo.DEFAULT_UNICODE_ENABLED, NotationInfo.DEFAULT_HIDE_PACKAGE_PREFIX);
202204
p.printSequent(s);
203205
return p.result();
204206
}
@@ -618,7 +620,7 @@ protected void printSchemaVariable(SchemaVariable sv) {
618620
private void printSourceElement(SourceElement element) {
619621
new PrettyPrinter(layouter, instantiations, services,
620622
notationInfo.isPrettySyntax(),
621-
notationInfo.isUnicodeEnabled()).print(element);
623+
notationInfo.isUnicodeEnabled(), notationInfo.isHidePackagePrefix()).print(element);
622624
}
623625

624626
/**
@@ -940,19 +942,32 @@ && getNotationInfo().isHidePackagePrefix()) {
940942
} else {
941943
String name = t.op().name().toString();
942944
layouter.startTerm(t.arity());
943-
boolean alreadyPrinted = false;
945+
944946
if (t.op() instanceof SortDependingFunction op) {
945-
if (op.getKind().compareTo(JavaDLTheory.EXACT_INSTANCE_NAME) == 0) {
946-
layouter.print(op.getSortDependingOn().declarationString());
947+
948+
// remove package prefix from SortDependingFunction
949+
if (notationInfo.isHidePackagePrefix()) {
950+
String sort = op.getSortDependingOn().declarationString();
951+
int index = sort.lastIndexOf('.');
952+
sort = sort.substring(index + 1);
953+
layouter.print(sort);
947954
layouter.print("::");
948-
layouter.keyWord(op.getKind().toString());
949-
alreadyPrinted = true;
955+
956+
name = op.getKind().toString();
957+
}
958+
959+
// mark instance and exactInstance as keywords
960+
if (op.getKind().compareTo(JavaDLTheory.EXACT_INSTANCE_NAME) == 0
961+
|| op.getKind().compareTo(JavaDLTheory.INSTANCE_NAME) == 0) {
962+
isKeyword = true;
950963
}
951964
}
952965
if (isKeyword) {
953966
layouter.markStartKeyword();
954967
}
955-
if (!alreadyPrinted) {
968+
if (isKeyword) {
969+
layouter.keyWord(name);
970+
} else {
956971
layouter.print(name);
957972
}
958973
if (isKeyword) {
@@ -984,7 +999,13 @@ public void printCast(String pre, String post, JTerm t, int ass) {
984999

9851000
layouter.startTerm(t.arity());
9861001
layouter.print(pre);
987-
layouter.print(cast.getSortDependingOn().toString());
1002+
String sort = cast.getSortDependingOn().toString();
1003+
// remove package prefix from sort name
1004+
if (notationInfo.isHidePackagePrefix()) {
1005+
int index = sort.lastIndexOf('.');
1006+
sort = sort.substring(index + 1);
1007+
}
1008+
layouter.print(sort);
9881009
layouter.print(post);
9891010
maybeParens(t.sub(0), ass);
9901011
}

‎key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java‎

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -146,7 +146,14 @@ public NotationInfo() {
146146
this.notationTable = createDefaultNotation();
147147
}
148148

149-
149+
public NotationInfo(boolean prettySyntax, boolean unicodeEnabled, boolean hidePackagePrefix) {
150+
this.notationTable = createDefaultNotation();
151+
this.prettySyntax = prettySyntax;
152+
this.unicodeEnabled = unicodeEnabled;
153+
this.hidePackagePrefix = hidePackagePrefix;
154+
// TODO: Do we need this in addition?
155+
// this.finalImmutable = finalImmutable;
156+
}
150157

151158
// -------------------------------------------------------------------------
152159
// internal methods
@@ -405,12 +412,15 @@ private HashMap<Object, Notation> createUnicodeNotation(Services services) {
405412
// -------------------------------------------------------------------------
406413

407414
public void refresh(Services services) {
408-
refresh(services, DEFAULT_PRETTY_SYNTAX, DEFAULT_UNICODE_ENABLED);
415+
refresh(services, DEFAULT_PRETTY_SYNTAX, DEFAULT_UNICODE_ENABLED,
416+
DEFAULT_HIDE_PACKAGE_PREFIX);
409417
}
410418

411-
public void refresh(Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols) {
419+
public void refresh(Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols,
420+
boolean hidePackagePrefix) {
412421
this.unicodeEnabled = useUnicodeSymbols;
413422
this.prettySyntax = usePrettyPrinting;
423+
this.hidePackagePrefix = hidePackagePrefix;
414424
if (usePrettyPrinting && services != null) {
415425
if (useUnicodeSymbols) {
416426
this.notationTable = createUnicodeNotation(services);
@@ -420,7 +430,6 @@ public void refresh(Services services, boolean usePrettyPrinting, boolean useUni
420430
} else {
421431
this.notationTable = createDefaultNotation();
422432
}
423-
hidePackagePrefix = DEFAULT_HIDE_PACKAGE_PREFIX;
424433

425434
if (services != null && services.getProof() != null) {
426435
ProofSettings settings = services.getProof().getSettings();

‎key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -71,21 +71,23 @@ public class PrettyPrinter implements Visitor {
7171

7272
private final SVInstantiations instantiations;
7373
private final @Nullable Services services;
74-
private boolean usePrettyPrinting;
75-
private boolean useUnicodeSymbols;
74+
private final boolean usePrettyPrinting;
75+
private final boolean useUnicodeSymbols;
76+
private final boolean hidePackagePrefix;
7677

7778
/** creates a new PrettyPrinter */
7879
public PrettyPrinter(PosTableLayouter out) {
79-
this(out, SVInstantiations.EMPTY_SVINSTANTIATIONS, null, true, true);
80+
this(out, SVInstantiations.EMPTY_SVINSTANTIATIONS, null, true, true, true);
8081
}
8182

8283
public PrettyPrinter(PosTableLayouter o, SVInstantiations svi, @Nullable Services services,
83-
boolean usePrettyPrinting, boolean useUnicodeSymbols) {
84+
boolean usePrettyPrinting, boolean useUnicodeSymbols, boolean hidePackagePrefix) {
8485
this.layouter = o;
8586
this.instantiations = svi;
8687
this.services = services;
8788
this.usePrettyPrinting = usePrettyPrinting;
8889
this.useUnicodeSymbols = useUnicodeSymbols;
90+
this.hidePackagePrefix = hidePackagePrefix;
8991
}
9092

9193
/**
@@ -1991,7 +1993,8 @@ public void performActionOnSetStatement(SetStatement x) {
19911993
}
19921994

19931995
public String printInLogicPrinter(JTerm t) {
1994-
var lp = LogicPrinter.quickPrinter(services, usePrettyPrinting, useUnicodeSymbols);
1996+
var lp = LogicPrinter.quickPrinter(services, usePrettyPrinting, useUnicodeSymbols,
1997+
hidePackagePrefix);
19951998
lp.printTerm(t);
19961999
return lp.result();
19972000
}

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -863,7 +863,7 @@ private static String printSequent(Sequent val, Services services) {
863863

864864
private static LogicPrinter createLogicPrinter(Services serv, boolean shortAttrNotation) {
865865

866-
final NotationInfo ni = new NotationInfo();
866+
final NotationInfo ni = new NotationInfo(false, false, false);
867867

868868
return LogicPrinter.purePrinter(ni, (shortAttrNotation ? serv : null));
869869
}

0 commit comments

Comments
 (0)