Skip to content

Fix recent file menu; fix #3898#3909

Open
wadoon wants to merge 1 commit into
mainfrom
weigl/rcfiles
Open

Fix recent file menu; fix #3898#3909
wadoon wants to merge 1 commit into
mainfrom
weigl/rcfiles

Conversation

@wadoon

@wadoon wadoon commented Jul 10, 2026

Copy link
Copy Markdown
Member

Related Issue

This pull request resolves #3898

Intended Change

  1. Make filenames as short as possible, but as long as needed for uniqueness, again.
  2. Show profile information directly and options in the tooltip.
  3. Do not show entries if they were temporary and already deleted.

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • New feature (non-breaking change which adds functionality)

Ensuring quality

  • Looking at it, visually.

@wadoon wadoon self-assigned this Jul 10, 2026
@wadoon wadoon requested a review from unp1 July 10, 2026 13:40
@wadoon wadoon added the GUI label Jul 10, 2026
@wadoon wadoon added this to the v3.0.0 milestone Jul 10, 2026
@wadoon wadoon changed the title fix #3898 Fix recent file menu; fix #3898 Jul 10, 2026
@wadoon wadoon force-pushed the weigl/rcfiles branch 3 times, most recently from 019e387 to affa3d6 Compare July 10, 2026 14:06

@unp1 unp1 left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks. Just a few minor issues. The problem with tmp is not a blocker just sth to be aware of.


// if file not present, and it was stored in the tmp folder,
// we allow us to silently ignore it.
if (e.path.startsWith(tmpFolder) && !Files.exists(Paths.get(e.path))) {

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Breaks RecentFileMenuTest (#3711): @TempDir sits under java.io.tmpdir and the test never creates A.key/B.key on disk, so both match the guard and are skipped and getMostRecent() returns null (CI stays red).

One problem tobe aware with java.io.tmpdir is that it is unreliable under macOS /var is a symlink to /private/var, so java.io.tmpdir reads as /var/folders/… while the same file, once canonicalized, is /private/var/folders/…

Comment thread key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java
Comment thread key.ui/src/main/java/de/uka/ilkd/key/gui/ShortUniqueFileNames.java
Comment thread key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java Outdated
Comment thread key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java Outdated
@KeYProject KeYProject deleted a comment from unp1 Jul 10, 2026
@wadoon wadoon force-pushed the weigl/rcfiles branch 2 times, most recently from b1e7b41 to 30b58f8 Compare July 10, 2026 18:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Recent files entries broken

2 participants