← Back to branch summary

~tapaal-contributor/tapaal/weight-values-fix-1770637

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/gui/BatchProcessingDialog.java

merged in branch lp:~tapaal-contributor/tapaal/Batch-export-PNML-XML-queries-1754675
adding batch export of files to PNML and XML

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/gui/BatchProcessingDialog.java
1478
1478
                enabledVerificationOptionButtons();
1479
1479
        }
1480
1480
 
1481
 
        // Custom cell renderer for the file list to only display the name of the
1482
 
        // file
1483
 
        // instead of the whole path.
1484
 
        private class FileNameCellRenderer extends JLabel implements
1485
 
                        ListCellRenderer {
1486
 
                private static final long serialVersionUID = 3071924451912979500L;
1487
 
 
1488
 
                public Component getListCellRendererComponent(JList list, Object value,
1489
 
                                int index, boolean isSelected, boolean cellHasFocus) {
1490
 
                        if (value instanceof File)
1491
 
                                setText(((File) value).getName());
1492
 
                        else
1493
 
                                setText(value.toString());
1494
 
                        if (isSelected) {
1495
 
                                setBackground(list.getSelectionBackground());
1496
 
                                setForeground(list.getSelectionForeground());
1497
 
                        } else {
1498
 
                                setBackground(list.getBackground());
1499
 
                                setForeground(list.getForeground());
1500
 
                        }
1501
 
                        setEnabled(list.isEnabled());
1502
 
                        setFont(list.getFont());
1503
 
                        setOpaque(true);
1504
 
                        return this;
1505
 
                }
1506
 
        }
1507
 
 
1508
1481
        // Custom cell renderer for the Query Column of the result table display the
1509
1482
        // property of the query
1510
1483
        private class ResultTableCellRenderer extends JLabel implements