From e06b74057a02a23ef2259831f6fd8051981a78bb Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 10 Jul 2026 15:39:37 +0200 Subject: [PATCH 1/2] fix #3898 --- .../de/uka/ilkd/key/gui/RecentFileMenu.java | 63 +++++++++++++++---- .../ilkd/key/gui/ShortUniqueFileNames.java | 9 +-- .../uka/ilkd/key/gui/RecentFileMenuTest.java | 56 ++++++++++------- .../key/gui/ShortUniqueFileNamesTest.java | 50 ++++++++++----- 4 files changed, 126 insertions(+), 52 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index 83dde969d95..8267a39f052 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -4,7 +4,9 @@ package de.uka.ilkd.key.gui; import java.awt.event.ActionEvent; -import java.io.*; +import java.io.File; +import java.io.FileNotFoundException; +import java.io.IOException; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; @@ -19,6 +21,7 @@ import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.PathConfig; +import com.google.common.html.HtmlEscapers; import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -104,15 +107,7 @@ private void addNewToModelAndView(final String path, insertFirstEntry(entry); // Recalculate unique names - final String[] paths = - recentFiles.stream().map(RecentFileEntry::getAbsolutePath).toArray(String[]::new); - final ShortUniqueFileNames.Name[] names = ShortUniqueFileNames.makeUniqueNames(paths); - - // Set the names - for (int i = 0; i < names.length; i++) { - var text = names[i].toString(); - recentFiles.get(i).createMenuItem().getAction().putValue(Action.NAME, text); - } + computeShortestUniqueFilenames(); } } @@ -194,8 +189,17 @@ public final void loadFrom(Path filename) { List recent = file.asConfigurationList(); this.recentFiles.clear(); this.mostRecentFile = null; + + String tmpFolder = System.getProperty("java.io.tmpdir"); for (var c : recent) { final var e = new RecentFileEntry(c); + + // 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))) { + continue; + } + // The list is stored most-recent-first, so the first entry is the most recent. // (Previously this condition was inverted and overwrote mostRecentFile with every // entry, leaving it null after startup -- issue #3711.) @@ -205,6 +209,8 @@ public final void loadFrom(Path filename) { recentFiles.add(e); menu.add(e.createMenuItem()); } + + computeShortestUniqueFilenames(); } catch (FileNotFoundException ex) { LOGGER.info("Could not read RecentFileList. Did not find file {}", filename); } catch (IOException ioe) { @@ -222,13 +228,44 @@ public String getMostRecent() { return mostRecentFile != null ? mostRecentFile.getAbsolutePath() : null; } + private void computeShortestUniqueFilenames() { + var map = new TreeMap(); + var actions = new ArrayList(); + + for (var menuComponent : menu.getMenuComponents()) { + var action = ((RecentFileAction) ((JMenuItem) menuComponent).getAction()); + map.put(action.fileEntry.path, action.fileEntry.path); + actions.add(action); + } + + var seq = map.keySet().stream().toList(); + var names = ShortUniqueFileNames.makeUniqueNames(seq); + for (int i = 0; i < seq.size(); i++) { + map.put(seq.get(i), names[i].getName()); + } + + for (RecentFileAction a : actions) { + var p = a.fileEntry.profile; + var option = a.fileEntry.additionalOption; + a.putValue(Action.NAME, map.get(a.fileEntry.path) + + ((p == null || p.equals("null")) ? "" : " (Profile: %s)".formatted(p))); + + a.putValue(Action.SHORT_DESCRIPTION, + "" + HtmlEscapers.htmlEscaper().escape(a.fileEntry.path) + + (option == null ? "" : "
" + option) + + ""); + } + } + + /** * write the recent file names to the given properties file. the file will be read (if it * exists) and then re-written so no information will be lost. */ public void store(Path filename) { List config = - recentFiles.stream().map(RecentFileEntry::asConfiguration).toList(); + recentFiles.stream().map(RecentFileEntry::asConfiguration) + .toList(); try (var fin = Files.newBufferedWriter(filename)) { var writer = new Configuration.ConfigurationWriter(fin); writer.printValue(config); @@ -241,6 +278,10 @@ public void save() { store(PathConfig.currentPaths.recentFileStorage); } + public List getEntries() { + return this.recentFiles; + } + public class RecentFileEntry { public static final String KEY_PATH = "path"; public static final String KEY_PROFILE = "profile"; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ShortUniqueFileNames.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ShortUniqueFileNames.java index 344bc26565c..6411e3c06c5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ShortUniqueFileNames.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ShortUniqueFileNames.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.gui; import java.io.File; +import java.util.List; /** * Algorithm to construct short unique file names for a set of paths. @@ -93,10 +94,10 @@ private static void prepareForInsertionOf( * @param files unique list of files * @return named files */ - public static Name[] makeUniqueNames(String[] files) { - Name[] names = new Name[files.length]; - for (int i = 0; i < files.length; i++) { - Name entry = new Name(files[i]); + public static Name[] makeUniqueNames(List files) { + Name[] names = new Name[files.size()]; + for (int i = 0; i < files.size(); i++) { + Name entry = new Name(files.get(i)); prepareForInsertionOf(names, i, entry); names[i] = entry; } diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java index e751166fc66..7500d281ef9 100644 --- a/key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java +++ b/key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java @@ -3,12 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui; -import java.io.BufferedWriter; import java.nio.file.Files; import java.nio.file.Path; -import java.util.List; - -import de.uka.ilkd.key.settings.Configuration; import org.junit.jupiter.api.Test; import org.junit.jupiter.api.io.TempDir; @@ -24,31 +20,49 @@ class RecentFileMenuTest { @Test - void mostRecentIsFirstEntryAfterLoad(@TempDir Path tmp) throws Exception { + void mostRecentFilesTempFilesAreNotReloadedIfNotExisting(@TempDir Path tmp) throws Exception { Path fileA = tmp.resolve("A.key"); Path fileB = tmp.resolve("B.key"); - Path store = tmp.resolve("recent.props"); - writeRecentFileStore(store, fileA, fileB); + // do not create these files. - // mainWindow is only stored as a field and not used on the loadFrom/getMostRecent path. RecentFileMenu menu = new RecentFileMenu(null); + menu.addRecentFile(fileA.toAbsolutePath().toString(), null, false, null); + menu.addRecentFile(fileB.toAbsolutePath().toString(), null, false, null); + + assertEquals(2, menu.getEntries().size(), "There should be two entries. Filtering happens later"); + + Path store = tmp.resolve("recent.json"); + menu.store(store); + + // mainWindow is only stored as a field and not used on the loadFrom/getMostRecent path. + RecentFileMenu menu2 = new RecentFileMenu(null); menu.loadFrom(store); - assertEquals(fileA.toString(), menu.getMostRecent(), - "Reload should target the first (most recent) stored entry"); + assertEquals(menu.getMostRecent(), menu2.getMostRecent()); + assertEquals(menu.getEntries(), menu2.getEntries()); } - /** Writes a recent-files configuration in the same format {@code RecentFileMenu.store} uses. */ - private static void writeRecentFileStore(Path store, Path... paths) throws Exception { - List entries = java.util.Arrays.stream(paths).map(p -> { - Configuration c = new Configuration(); - c.set("path", p.toString()); - c.set("singleJava", false); - return c; - }).toList(); - try (BufferedWriter w = Files.newBufferedWriter(store)) { - new Configuration.ConfigurationWriter(w).printValue(entries); - } + @Test + void mostRecentFilesTempFilesAreNotReloadedIfExisting(@TempDir Path tmp) throws Exception { + Path fileA = tmp.resolve("A.key"); + Path fileB = tmp.resolve("B.key"); + + Files.createFile(fileA); + Files.createFile(fileB); + + RecentFileMenu menu = new RecentFileMenu(null); + menu.addRecentFile(fileA.toAbsolutePath().toString(), null, false, null); + menu.addRecentFile(fileB.toAbsolutePath().toString(), null, false, null); + + Path store = tmp.resolve("recent.json"); + menu.store(store); + + // mainWindow is only stored as a field and not used on the loadFrom/getMostRecent path. + RecentFileMenu menu2 = new RecentFileMenu(null); + menu.loadFrom(store); + + assertEquals(menu.getMostRecent(), menu2.getMostRecent()); + assertEquals(menu.getEntries(), menu2.getEntries()); } } diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/ShortUniqueFileNamesTest.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/ShortUniqueFileNamesTest.java index 7c03a209923..219f3911377 100644 --- a/key.ui/src/test/java/de/uka/ilkd/key/gui/ShortUniqueFileNamesTest.java +++ b/key.ui/src/test/java/de/uka/ilkd/key/gui/ShortUniqueFileNamesTest.java @@ -4,8 +4,12 @@ package de.uka.ilkd.key.gui; import java.nio.file.Paths; -import java.util.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Map; +import java.util.Random; +import org.jspecify.annotations.NonNull; import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; @@ -16,28 +20,38 @@ class ShortUniqueFileNamesTest { @Test void uniqueFileNamesTest() { // (path, expected name after all insertions) - HashMap pathsToName = new HashMap<>(); - pathsToName.put(Paths.get("z", "a", "b", "c").toString(), - Paths.get("z", "a", "b", "c").toString()); - pathsToName.put(Paths.get("a", "b", "c").toString(), Paths.get("a", "b", "c").toString()); - pathsToName.put(Paths.get("b", "b", "c").toString(), Paths.get("b", "b", "c").toString()); - pathsToName.put(Paths.get("z", "b", "b", "c").toString(), - Paths.get("z", "b", "b", "c").toString()); - pathsToName.put(Paths.get("b", "c").toString(), Paths.get("b", "c").toString()); - pathsToName.put(Paths.get("b", "d").toString(), Paths.get("d").toString()); - pathsToName.put(Paths.get("x", "y").toString(), Paths.get("y").toString()); + var pathsToName = Map.of( + createPathString("z", "a", "b", "c"), + createPathString("z", "a", "b", "c"), + + createPathString("a", "b", "c"), + createPathString("a", "b", "c"), + + createPathString("b", "b", "c"), + createPathString("b", "b", "c"), + + createPathString("z", "b", "b", "c"), + createPathString("z", "b", "b", "c"), + + createPathString("b", "c"), + createPathString("b", "c"), + + createPathString("b", "d"), createPathString("d"), + createPathString("x", "y"), createPathString("y")); + Random random = new Random(42); // Test that insertion order does not matter - String[] paths = pathsToName.keySet().toArray(String[]::new); + var paths = new ArrayList<>(pathsToName.keySet()); // weigl: enforce array list for + // efficient shuffle. for (int i = 0; i < 1000; ++i) { - Collections.shuffle(Arrays.asList(paths), random); + Collections.shuffle(paths, random); ShortUniqueFileNames.Name[] names = ShortUniqueFileNames.makeUniqueNames(paths); - Assertions.assertEquals(names.length, paths.length); + Assertions.assertEquals(names.length, paths.size()); - for (int j = 0; j < paths.length; ++j) { - String path = paths[j]; + for (int j = 0; j < paths.size(); ++j) { + String path = paths.get(j); ShortUniqueFileNames.Name name = names[j]; Assertions.assertEquals(path, name.getPath()); @@ -47,4 +61,8 @@ void uniqueFileNamesTest() { } } } + + private static @NonNull String createPathString(String s, String... more) { + return Paths.get(s, more).toString(); + } } From 334c0de5625ab1ef2f78e3e168b2eeefbcc0a61e Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 12 Jul 2026 00:35:55 +0200 Subject: [PATCH 2/2] make RecentFileMenu testable --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 2 ++ .../de/uka/ilkd/key/gui/RecentFileMenu.java | 36 ++++++++++++++++++- .../uka/ilkd/key/gui/RecentFileMenuTest.java | 28 +++++++-------- 3 files changed, 50 insertions(+), 16 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 7181510b9de..3542f7c505b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -331,6 +331,8 @@ private MainWindow() { notificationManager = new NotificationManager(mediator, this); recentFileMenu = new RecentFileMenu(this); + // Postpone load for faster UI creation. + SwingUtilities.invokeLater(recentFileMenu::loadEntries); proofTreeView = new ProofTreeView(mediator); infoView = new InfoView(mediator); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index 8267a39f052..1416a019c2a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -76,7 +76,11 @@ public RecentFileMenu(final MainWindow mediator) { // menu.setEnabled(menu.getItemCount() != 0); menu.setIcon(IconFactory.recentFiles(16)); + } + /// Loads entries from the current default configuration folder. + /// @see PathConfig.KeyPaths#recentFileStorage + public void loadEntries() { if (Files.exists(PathConfig.currentPaths.recentFileStorage)) { loadFrom(PathConfig.currentPaths.recentFileStorage); } else { @@ -111,7 +115,7 @@ private void addNewToModelAndView(final String path, } } - private void addRecentFileNoSave(final String path, + void addRecentFileNoSave(final String path, @Nullable Profile profile, boolean singleJava, @Nullable Configuration additionalOption) { @@ -336,6 +340,36 @@ public JMenuItem createMenuItem() { } return menuItem; } + + @Override + public String toString() { + return "RecentFileEntry{" + + "additionalOption=" + additionalOption + + ", path='" + path + '\'' + + ", profile='" + profile + '\'' + + ", singleJava=" + singleJava + + '}'; + } + + @Override + public final boolean equals(Object o) { + if (!(o instanceof RecentFileEntry that)) + return false; + + return singleJava == that.singleJava + && path.equals(that.path) + && Objects.equals(profile, that.profile) + && Objects.equals(additionalOption, that.additionalOption); + } + + @Override + public int hashCode() { + int result = path.hashCode(); + result = 31 * result + Objects.hashCode(profile); + result = 31 * result + Boolean.hashCode(singleJava); + result = 31 * result + Objects.hashCode(additionalOption); + return result; + } } private class RecentFileAction extends KeyAction { diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java index 7500d281ef9..b5c5ff1be5e 100644 --- a/key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java +++ b/key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java @@ -6,10 +6,10 @@ import java.nio.file.Files; import java.nio.file.Path; +import org.assertj.core.api.Assertions; import org.junit.jupiter.api.Test; import org.junit.jupiter.api.io.TempDir; -import static org.junit.jupiter.api.Assertions.assertEquals; /** * Regression test for issue #3711: after loading the recent-files list from disk, the "most @@ -21,26 +21,24 @@ class RecentFileMenuTest { @Test void mostRecentFilesTempFilesAreNotReloadedIfNotExisting(@TempDir Path tmp) throws Exception { - Path fileA = tmp.resolve("A.key"); - Path fileB = tmp.resolve("B.key"); + Path fileA = tmp.resolve("C.key"); + Path fileB = tmp.resolve("D.key"); // do not create these files. RecentFileMenu menu = new RecentFileMenu(null); - menu.addRecentFile(fileA.toAbsolutePath().toString(), null, false, null); - menu.addRecentFile(fileB.toAbsolutePath().toString(), null, false, null); - - assertEquals(2, menu.getEntries().size(), "There should be two entries. Filtering happens later"); + menu.addRecentFileNoSave(fileA.toAbsolutePath().toString(), null, false, null); + menu.addRecentFileNoSave(fileB.toAbsolutePath().toString(), null, false, null); Path store = tmp.resolve("recent.json"); menu.store(store); // mainWindow is only stored as a field and not used on the loadFrom/getMostRecent path. RecentFileMenu menu2 = new RecentFileMenu(null); - menu.loadFrom(store); + menu2.loadFrom(store); - assertEquals(menu.getMostRecent(), menu2.getMostRecent()); - assertEquals(menu.getEntries(), menu2.getEntries()); + Assertions.assertThat(menu2.getMostRecent()).isEqualTo(menu.getMostRecent()); + Assertions.assertThat(menu2.getEntries()).isEmpty(); // <- non existing temp files } @Test @@ -52,17 +50,17 @@ void mostRecentFilesTempFilesAreNotReloadedIfExisting(@TempDir Path tmp) throws Files.createFile(fileB); RecentFileMenu menu = new RecentFileMenu(null); - menu.addRecentFile(fileA.toAbsolutePath().toString(), null, false, null); - menu.addRecentFile(fileB.toAbsolutePath().toString(), null, false, null); + menu.addRecentFileNoSave(fileA.toAbsolutePath().toString(), null, false, null); + menu.addRecentFileNoSave(fileB.toAbsolutePath().toString(), null, false, null); Path store = tmp.resolve("recent.json"); menu.store(store); // mainWindow is only stored as a field and not used on the loadFrom/getMostRecent path. RecentFileMenu menu2 = new RecentFileMenu(null); - menu.loadFrom(store); + menu2.loadFrom(store); - assertEquals(menu.getMostRecent(), menu2.getMostRecent()); - assertEquals(menu.getEntries(), menu2.getEntries()); + Assertions.assertThat(menu2.getMostRecent()).isEqualTo(menu.getMostRecent()); + Assertions.assertThat(menu2.getEntries()).containsExactlyElementsOf(menu.getEntries()); } }