Skip to content

Fix for #3683: Hiding package prefixes in sequent view#3684

Merged
wadoon merged 5 commits intomainfrom
pfeifer/3683hidePackageOptionFix
Mar 19, 2026
Merged

Fix for #3683: Hiding package prefixes in sequent view#3684
wadoon merged 5 commits intomainfrom
pfeifer/3683hidePackageOptionFix

Conversation

@WolframPfeifer
Copy link
Member

@WolframPfeifer WolframPfeifer commented Nov 12, 2025

Quick fix: Hiding package prefixes in sequent view now works as expected. In addition, highlighting for the SortDependingFunction instance is added as for exactInstance.

Explanation: I noticed that while the code for hiding the prefixes was (partially) implemented, the view setting was never queried in the printer. I made the printer respect the setting, and added a missing case.

Known issues/missing features:

  • Inside modalities, the prefixes are still kept as is, even with the setting switched on. While this would not be difficult to implement, I am not sure if we should hide the prefixes there.
  • There might be clashes now, for example when two class names pkg1.A and pkg2.A both appear on the sequent, they are not visually distinguishable. This would probably be difficult to implement ...

Related Issue

This pull request resolves #3683.

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • There are changes to the (Java) code

Ensuring quality

  • I made sure that introduced/changed code is well documented (inline comments).
  • I have tested the feature manually on a small example

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@WolframPfeifer WolframPfeifer self-assigned this Nov 12, 2025
@WolframPfeifer
Copy link
Member Author

WolframPfeifer commented Nov 12, 2025

@FliegendeWurst: Can you try to use that "in production" and see if there are missing cases where the prefix is still shown? I only tried on a very small example.

@WolframPfeifer WolframPfeifer marked this pull request as draft November 12, 2025 17:28
@FliegendeWurst
Copy link
Member

FliegendeWurst commented Nov 14, 2025

I tried this PR on a bigger example (proof of an accessible clause) and it works well.

@WolframPfeifer WolframPfeifer marked this pull request as ready for review November 14, 2025 10:59
@WolframPfeifer WolframPfeifer added the Review Request Waiting for review label Nov 14, 2025
@FliegendeWurst
Copy link
Member

FliegendeWurst commented Nov 17, 2025

Actually, there is one case where this change still shows the full package prefix: typed seqGet expressions. When using the pretty syntax, you still see the full package name in the cast.

@FliegendeWurst
Copy link
Member

FliegendeWurst commented Dec 2, 2025

Actually, this change causes a rather serious regression in proof saving: #3691

@FliegendeWurst FliegendeWurst mentioned this pull request Dec 2, 2025
Open
@WolframPfeifer
Copy link
Member Author

WolframPfeifer commented Dec 3, 2025

Actually, there is one case where this change still shows the full package prefix: typed seqGet expressions. When using the pretty syntax, you still see the full package name in the cast.

From the meeting just now: This seems to happen for the sort when printing SortDependingFunctions.

@WolframPfeifer
Copy link
Member Author

WolframPfeifer commented Dec 3, 2025

I think, #3691 is a bug/problem that was already present before, but became visible with the changes here.
In my opinion, the save functionality should not use the pretty printer, since not everything printed with that is parsable again.

@Drodt Drodt self-requested a review December 5, 2025 13:09
@WolframPfeifer WolframPfeifer added this to the v3.0.0 milestone Jan 7, 2026
WolframPfeifer and others added 2 commits January 30, 2026 16:06
@WolframPfeifer
pass pretty printing options to pretty printer, disable hidePackagePr…
590dbf2 
…efix when saving proofs
@wadoon
Merge remote-tracking branch 'origin/main' into pfeifer/3683hidePacka…
ed2ca04 
…geOptionFix

# By Alexander Weigl (48) and others
# Via GitHub (35) and others
* origin/main: (117 commits)
  Add containsGenerics method to sort
  spotless
  look in top-level project.key for includes to allow for dl escapes in Java files
  Simplify
  Remove tokens file
  Fix inst with sort depending fn
  Fix parsing of proof files
  Fix proof loading/storing when generics are instantiated in NoFindTaclets
  Some documentation
  Fix test classes
  Slightly improve error messages
  Fix taclets for datatypes w/ polymorphic params
  Prepare datatype handling
  Spotless
  Finish example; slight fixes
  Fix fns and preds parsing; add test
  Fix SortDepFn and add test
  Start on polymorphic sorts and functions
  directly creating issues in Github inside KeY
  Bump the gradle-deps group across 1 directory with 9 updates
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
@wadoon wadoon enabled auto-merge March 18, 2026 22:43
@wadoon wadoon added this pull request to the merge queue Mar 18, 2026
Merged via the queue into main with commit de6e44b Mar 19, 2026
36 checks passed
@wadoon wadoon deleted the pfeifer/3683hidePackageOptionFix branch March 19, 2026 01:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Drodt Drodt Drodt approved these changes

Assignees

@WolframPfeifer WolframPfeifer

Labels

GUI 🐞 Bug Review Request Waiting for review

Projects

None yet

Milestone

v3.0.0

Development

Successfully merging this pull request may close these issues.

View option 'hide package prefix' doesn't work

4 participants

@WolframPfeifer @FliegendeWurst @Drodt @wadoon