← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/pipe/gui/GuiFrame.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/pipe/gui/GuiFrame.java
117
117
        private FileAction createAction, openAction, closeAction, saveAction,
118
118
        saveAsAction, exitAction, printAction, importPNMLAction, importSUMOAction,
119
119
        importXMLAction, exportPNGAction, exportPSAction, exportToTikZAction,
120
 
        exportToPNMLAction, exportToXMLAction, exportTraceAction, importTraceAction;
 
120
        exportToPNMLAction, exportToXMLAction, exportTraceAction, importTraceAction, 
 
121
        exportBatchAction;
121
122
 
122
123
        private VerificationAction runUppaalVerification;
123
124
 
430
431
                addMenuItem(exportMenu, exportToXMLAction = new FileAction("XML Queries",
431
432
                                "Export the queries to XML format", "ctrl H"));
432
433
                exportToXMLAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('H', shortcutkey));
 
434
                addMenuItem(exportMenu, exportBatchAction = new FileAction("Batch Export to PNML and XML Queries", "Export multiple nets into PNML together with the XML queries, while removing the timing information", "ctrl K"));
 
435
                exportBatchAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('K', shortcutkey));
433
436
                
434
437
                fileMenu.add(exportMenu);
435
438
 
1190
1193
                        stripTimeDialogAction.setEnabled(false);
1191
1194
 
1192
1195
                        enableAllActions(false);
 
1196
 
1193
1197
                        break;
1194
1198
                }
1195
1199
 
1208
1212
 
1209
1213
                saveAction.setEnabled(enable);
1210
1214
                saveAsAction.setEnabled(enable);
1211
 
 
1212
 
                exportMenu.setEnabled(enable);
 
1215
                
1213
1216
                exportPNGAction.setEnabled(enable);
1214
1217
                exportPSAction.setEnabled(enable);
1215
1218
                exportToTikZAction.setEnabled(enable);
2723
2726
                        } else if(this == importTraceAction){
2724
2727
                                TraceImportExport.importTrace();
2725
2728
                        }
 
2729
                        else if(this == exportBatchAction) {
 
2730
                                ExportBatchDialog.ShowExportBatchDialog();
 
2731
                        }
2726
2732
                }
2727
2733
 
2728
2734
        }