Skip to content

Commit

Permalink
Fix filters in file choosers
Browse files Browse the repository at this point in the history
  • Loading branch information
xeren committed Oct 16, 2024
1 parent b4bbfed commit 92ef219
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 1 deletion.
3 changes: 2 additions & 1 deletion ui/src/main/java/com/dat3m/ui/editor/Editor.java
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,8 @@ public class Editor extends RTextScrollPane implements ActionListener {
this.allowedFormats = ImmutableSet.copyOf(code.supportedExtensions());
this.chooser = new JFileChooser();
for (String format : allowedFormats) {
chooser.addChoosableFileFilter(new FileNameExtensionFilter("*" + format, format));
final String extension = format.startsWith(".") ? format.substring(1) : format;
chooser.addChoosableFileFilter(new FileNameExtensionFilter("*" + format, extension));
}

setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED);
Expand Down
2 changes: 2 additions & 0 deletions ui/src/main/java/com/dat3m/ui/options/OptionsPane.java
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
import javax.swing.*;
import javax.swing.border.Border;
import javax.swing.border.TitledBorder;
import javax.swing.filechooser.FileNameExtensionFilter;
import java.awt.*;
import java.awt.event.ActionEvent;
import java.awt.event.FocusAdapter;
Expand Down Expand Up @@ -108,6 +109,7 @@ public OptionsPane() {
setLayout(new BoxLayout(this, BoxLayout.X_AXIS));
extraOptionsButton.setToolTipText("Manage extra options.");
extraOptionsDialog = newDialog();
configurationFileChooser.addChoosableFileFilter(new FileNameExtensionFilter("*.properties", "properties"));

testButton = new TestButton();
clearButton = new ClearButton();
Expand Down

0 comments on commit 92ef219

Please sign in to comment.