← Back to branch summary

~yrke/tapaal/java11

« back to all changes in this revision

Viewing changes to src/pipe/gui/widgets/filebrowser/NativeFileBrowserFallback.java

  • Committer: Jiri Srba
  • Date: 2020-03-27 12:18:55 UTC
  • mfrom: (1041.1.2 tapaal)
  • Revision ID: srba@cs.aau.dk-20200327121855-d0j3aurjb7nvoehn
merged in lp:~tapaal-contributor/tapaal/open-on-windows-1868525 fixing .xml file open on windows 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/widgets/filebrowser/NativeFileBrowserFallback.java
17
17
class NativeFileBrowserFallback extends FileBrowser {
18
18
        private FileDialog fc;
19
19
        private String ext;
 
20
        private String optionalExt;
20
21
        private String specifiedPath;
21
22
        private JFileChooser fileChooser;
22
23
        /**
36
37
                //if(path == null) path = lastPath;
37
38
 
38
39
                this.ext = ext;
 
40
                this.optionalExt = optionalExt;
39
41
                //fc.setDirectory(path);
40
42
 
41
43
                /* Setup JFileChooser for multi file selection */
44
46
                FileNameExtensionFilter filter;
45
47
 
46
48
                // Setup filter if extension specified
 
49
                //This is needed for Linux and Mac
47
50
                if(!ext.equals("")){
48
51
                        if(!optionalExt.equals("")) {
49
52
                                fc.setFilenameFilter(new FilenameFilter() {
76
79
        public File openFile() {
77
80
                if(specifiedPath == null) specifiedPath = lastOpenPath;
78
81
                fc.setDirectory(specifiedPath);
79
 
                fc.setFile(ext.equals("")? "":"*."+ext);
 
82
                //This is needed for windows
 
83
                if(optionalExt.equals("")) fc.setFile(ext.equals("")? "":("*."+ext));
 
84
                else fc.setFile(ext.equals("")? "":("*."+ext+";*."+optionalExt));
80
85
                fc.setMode(FileDialog.LOAD);
81
86
                fc.setVisible(true);
82
87
                String selectedFile = fc.getFile();