Skip to content

Fix recent file menu; fix #3898 #3909

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wadoon wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Fix recent file menu; fix #3898 #3909

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e06b740
fix #3898
wadoon Jul 10, 2026
334c0de
make RecentFileMenu testable
wadoon Jul 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
99 changes: 87 additions & 12 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -73,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 {
Expand Down Expand Up @@ -104,19 +111,11 @@ 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();
}
}

private void addRecentFileNoSave(final String path,
void addRecentFileNoSave(final String path,
@Nullable Profile profile,
boolean singleJava,
@Nullable Configuration additionalOption) {
Expand Down Expand Up @@ -194,8 +193,17 @@ public final void loadFrom(Path filename) {
List<Configuration> 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))) {
Comment thread
wadoon marked this conversation as resolved.
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.)
Expand All @@ -205,6 +213,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) {
Expand All @@ -222,13 +232,44 @@ public String getMostRecent() {
return mostRecentFile != null ? mostRecentFile.getAbsolutePath() : null;
}

private void computeShortestUniqueFilenames() {
var map = new TreeMap<String, String>();
var actions = new ArrayList<RecentFileAction>();

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,
Comment thread
wadoon marked this conversation as resolved.
"<html>" + HtmlEscapers.htmlEscaper().escape(a.fileEntry.path) +
(option == null ? "" : "<br>" + option)
+ "</html>");
}
}


/**
* 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<Configuration> 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);
Expand All @@ -241,6 +282,10 @@ public void save() {
store(PathConfig.currentPaths.recentFileStorage);
}

public List<RecentFileEntry> getEntries() {
return this.recentFiles;
}

public class RecentFileEntry {
public static final String KEY_PATH = "path";
public static final String KEY_PROFILE = "profile";
Expand Down Expand Up @@ -295,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 {
Expand Down
9 changes: 5 additions & 4 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/ShortUniqueFileNames.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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<String> files) {
Comment thread
wadoon marked this conversation as resolved.
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;
}
Expand Down
60 changes: 36 additions & 24 deletions key.ui/src/test/java/de/uka/ilkd/key/gui/RecentFileMenuTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,13 @@
* 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.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
Expand All @@ -24,31 +20,47 @@
class RecentFileMenuTest {

@Test
void mostRecentIsFirstEntryAfterLoad(@TempDir Path tmp) throws Exception {
void mostRecentFilesTempFilesAreNotReloadedIfNotExisting(@TempDir Path tmp) throws Exception {
Path fileA = tmp.resolve("C.key");
Path fileB = tmp.resolve("D.key");

// do not create these files.

RecentFileMenu menu = new RecentFileMenu(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);
menu2.loadFrom(store);

Assertions.assertThat(menu2.getMostRecent()).isEqualTo(menu.getMostRecent());
Assertions.assertThat(menu2.getEntries()).isEmpty(); // <- non existing temp files
}

@Test
void mostRecentFilesTempFilesAreNotReloadedIfExisting(@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);
Files.createFile(fileA);
Files.createFile(fileB);

// mainWindow is only stored as a field and not used on the loadFrom/getMostRecent path.
RecentFileMenu menu = new RecentFileMenu(null);
menu.loadFrom(store);
menu.addRecentFileNoSave(fileA.toAbsolutePath().toString(), null, false, null);
menu.addRecentFileNoSave(fileB.toAbsolutePath().toString(), null, false, null);

assertEquals(fileA.toString(), menu.getMostRecent(),
"Reload should target the first (most recent) stored entry");
}
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);
menu2.loadFrom(store);

/** Writes a recent-files configuration in the same format {@code RecentFileMenu.store} uses. */
private static void writeRecentFileStore(Path store, Path... paths) throws Exception {
List<Configuration> 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);
}
Assertions.assertThat(menu2.getMostRecent()).isEqualTo(menu.getMostRecent());
Assertions.assertThat(menu2.getEntries()).containsExactlyElementsOf(menu.getEntries());
}
}
50 changes: 34 additions & 16 deletions key.ui/src/test/java/de/uka/ilkd/key/gui/ShortUniqueFileNamesTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -16,28 +20,38 @@ class ShortUniqueFileNamesTest {
@Test
void uniqueFileNamesTest() {
// (path, expected name after all insertions)
HashMap<String, String> 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());

Expand All @@ -47,4 +61,8 @@ void uniqueFileNamesTest() {
}
}
}

private static @NonNull String createPathString(String s, String... more) {
return Paths.get(s, more).toString();
}
}
Loading