~tapaal-contributor/tapaal/disappearing-tokens-1940098

« back to all changes in this revision

Viewing changes to src/pipe/gui/GuiFrame.java

  • Committer: Jiri Srba
  • Date: 2020-12-16 08:35:17 UTC
  • mfrom: (1113.1.7 batch-export)
  • Revision ID: srba@cs.aau.dk-20201216083517-e5o167vms7xw6f0z
merged in lp:~tapaal-contributor/tapaal/add-export-options adding the option of batch export to all engines

Show diffs side-by-side

added added

removed removed

Lines of Context:
18
18
 
19
19
import com.sun.jna.Platform;
20
20
import dk.aau.cs.gui.*;
 
21
import dk.aau.cs.model.tapn.TimedArcPetriNet;
21
22
import dk.aau.cs.util.JavaUtil;
22
23
import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
 
24
import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNExporter;
23
25
import net.tapaal.Preferences;
24
26
import net.tapaal.TAPAAL;
25
27
import net.tapaal.helpers.Reference.MutableReference;
27
29
import net.tapaal.swinghelpers.ExtendedJTabbedPane;
28
30
import net.tapaal.swinghelpers.ToggleButtonWithoutText;
29
31
import org.jetbrains.annotations.NotNull;
 
32
import pipe.dataLayer.TAPNQuery;
30
33
import pipe.gui.Pipe.ElementType;
31
34
import pipe.gui.action.GuiAction;
32
35
import pipe.gui.widgets.WorkflowDialog;
173
176
            currentTab.ifPresent(TabContentActions::importTrace);
174
177
        }
175
178
    };
176
 
    private final GuiAction exportBatchAction = new GuiAction("Batch Export to PNML and XML Queries", "Export multiple nets into PNML together with the XML queries, while removing the timing information", KeyStroke.getKeyStroke('D', (shortcutkey + InputEvent.SHIFT_DOWN_MASK))) {
 
179
    private final GuiAction exportBatchAction = new GuiAction("Batch Export of model and queries", "Export multiple nets into PNML together with the XML queries, while removing the timing information", KeyStroke.getKeyStroke('D', (shortcutkey + InputEvent.SHIFT_DOWN_MASK))) {
177
180
        public void actionPerformed(ActionEvent e) {
178
181
            ExportBatchDialog.ShowExportBatchDialog();
179
182
        }
1380
1383
 
1381
1384
        exportMenu.add(exportPSAction);
1382
1385
 
1383
 
 
1384
1386
        exportMenu.add(exportToTikZAction);
1385
1387
 
1386
 
 
1387
1388
        exportMenu.add(exportToPNMLAction);
1388
1389
 
1389
 
 
1390
1390
        exportMenu.add(exportToXMLAction);
1391
1391
 
1392
1392
        exportMenu.add(exportBatchAction);