← 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/components/ExportBatchResultTableModel.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/components/ExportBatchResultTableModel.java
 
1
package dk.aau.cs.gui.components;
 
2
 
 
3
import java.util.ArrayList;
 
4
import javax.swing.table.AbstractTableModel;
 
5
 
 
6
import dk.aau.cs.util.Require;
 
7
import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationResult;
 
8
 
 
9
 
 
10
public class ExportBatchResultTableModel extends AbstractTableModel {
 
11
 static final long serialVersionUID = 959574725280211159L;
 
12
        private final String[] HEADINGS = new String[]{ "File name", "Destination", "Status" };
 
13
        private ArrayList<String[]> results;
 
14
        
 
15
        public ExportBatchResultTableModel() {
 
16
                results = new ArrayList<String[]>();
 
17
        }
 
18
        
 
19
        public void addResult(String[] result){
 
20
                int lastRow = results.size();
 
21
                results.add(result);
 
22
                fireTableRowsInserted(lastRow, lastRow);
 
23
        }
 
24
        public String getColumnName(int column) {
 
25
                return HEADINGS[column];
 
26
        }
 
27
        
 
28
        public int getColumnCount() {
 
29
                return HEADINGS.length;
 
30
        }
 
31
 
 
32
        public int getRowCount() {
 
33
                if(results == null)
 
34
                        return 0;
 
35
                else            
 
36
                        return results.size();
 
37
        }
 
38
        public Object getValueAt(int rowIndex, int columnIndex) {
 
39
                if(rowIndex >= results.size())  return null;
 
40
                String[] result = results.get(rowIndex);
 
41
                
 
42
                switch(columnIndex){
 
43
                case 0: return result[0];
 
44
                case 1: return result[1];
 
45
                case 2: return result[2];
 
46
                default:
 
47
                        return null;
 
48
                }
 
49
        }
 
50
        public void clear() {
 
51
                results.clear();
 
52
                fireTableDataChanged();
 
53
        }
 
54
        public String[] getResult(int index) {
 
55
                Require.that(index >= 0 && index < results.size(), "Index out of range");
 
56
                
 
57
                return results.get(index);
 
58
        }
 
59
 
 
60
}