~tapaal-contributor/tapaal/engine-option-matrix-dev

« back to all changes in this revision

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

  • Committer: ptaankvist at gmail
  • Date: 2020-08-10 09:47:18 UTC
  • mfrom: (1068.1.10 tapaal)
  • Revision ID: ptaankvist@gmail.com-20200810094718-5ml66wkuy1m2dpl0
add game as option for the engines and merge with trunk

Show diffs side-by-side

added added

removed removed

Lines of Context:
9
9
import java.awt.event.WindowEvent;
10
10
import java.io.*;
11
11
import java.net.*;
 
12
import java.nio.charset.StandardCharsets;
12
13
import java.util.*;
13
14
import java.util.jar.JarEntry;
14
15
import java.util.jar.JarFile;
15
 
import javax.imageio.ImageIO;
16
16
import javax.swing.*;
17
17
 
18
 
import com.apple.eawt.Application;
 
18
import com.sun.jna.Platform;
19
19
import dk.aau.cs.gui.*;
20
20
import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
21
21
import net.tapaal.Preferences;
22
 
import com.sun.jna.Platform;
23
22
import net.tapaal.TAPAAL;
24
23
import net.tapaal.helpers.Reference.MutableReference;
25
24
import net.tapaal.helpers.Reference.Reference;
27
26
import net.tapaal.swinghelpers.ToggleButtonWithoutText;
28
27
import pipe.gui.Pipe.ElementType;
29
28
import pipe.gui.action.GuiAction;
30
 
import pipe.gui.graphicElements.PetriNetObject;
31
 
import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
32
 
import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
33
 
import pipe.gui.handler.SpecialMacHandler;
34
29
import pipe.gui.widgets.WorkflowDialog;
35
30
import dk.aau.cs.debug.Logger;
36
31
import dk.aau.cs.gui.smartDraw.SmartDrawDialog;
45
40
    // for zoom combobox and dropdown
46
41
    private final int[] zoomLevels = {40, 60, 80, 100, 120, 140, 160, 180, 200, 300};
47
42
 
48
 
    private String frameTitle;
 
43
    private final String frameTitle;
49
44
 
50
45
    private Pipe.ElementType mode;
51
46
 
53
48
 
54
49
    final MutableReference<GuiFrameControllerActions> guiFrameController = new MutableReference<>();
55
50
 
56
 
    private ExtendedJTabbedPane<TabContent> appTab;
 
51
    private final ExtendedJTabbedPane<TabContent> appTab;
57
52
 
58
 
    private StatusBar statusBar;
 
53
    private final StatusBar statusBar;
59
54
    private JMenuBar menuBar;
60
55
    private JToolBar drawingToolBar;
61
56
    private final JLabel featureInfoText = new JLabel();
351
346
            guiFrameController.ifPresent(GuiFrameControllerActions::toggleQueries);
352
347
        }
353
348
    };
354
 
    private GuiAction showConstantsAction = new GuiAction("Display constants", "Show/hide global constants.", KeyStroke.getKeyStroke('4', shortcutkey), true) {
 
349
    private final GuiAction showConstantsAction = new GuiAction("Display constants", "Show/hide global constants.", KeyStroke.getKeyStroke('4', shortcutkey), true) {
355
350
        public void actionPerformed(ActionEvent e) {
356
351
            guiFrameController.ifPresent(GuiFrameControllerActions::toggleConstants);
357
352
        }
386
381
            guiFrameController.ifPresent(GuiFrameControllerActions::showSimpleWorkspace);
387
382
        }
388
383
    };
389
 
    private GuiAction saveWorkSpaceAction = new GuiAction("Save workspace", "Save the current workspace as the default one", false) {
 
384
    private final GuiAction saveWorkSpaceAction = new GuiAction("Save workspace", "Save the current workspace as the default one", false) {
390
385
        public void actionPerformed(ActionEvent e) {
391
386
            guiFrameController.ifPresent(GuiFrameControllerActions::saveWorkspace);
392
387
        }
444
439
            currentTab.ifPresent(TabContentActions::stepBackwards);
445
440
        }
446
441
    };
447
 
    private GuiAction timeAction = new GuiAction("Delay one time unit", "Let time pass one time unit", "W") {
 
442
    private final GuiAction timeAction = new GuiAction("Delay one time unit", "Let time pass one time unit", "W") {
448
443
        public void actionPerformed(ActionEvent e) {
449
444
            currentTab.ifPresent(TabContentActions::timeDelay);
450
445
        }
451
446
    };
452
 
    private GuiAction delayFireAction = new GuiAction("Delay and fire", "Delay and fire selected transition", "F") {
 
447
    private final GuiAction delayFireAction = new GuiAction("Delay and fire", "Delay and fire selected transition", "F") {
453
448
        public void actionPerformed(ActionEvent e) {
454
449
            currentTab.ifPresent(TabContentActions::delayAndFire);
455
450
        }
456
451
    };
457
 
    private GuiAction prevcomponentAction = new GuiAction("Previous component", "Previous component", "pressed UP") {
 
452
    private final GuiAction prevcomponentAction = new GuiAction("Previous component", "Previous component", "pressed UP") {
458
453
        public void actionPerformed(ActionEvent e) {
459
454
            currentTab.ifPresent(TabContentActions::previousComponent);
460
455
        }
461
456
    };
462
 
    private GuiAction nextcomponentAction = new GuiAction("Next component", "Next component", "pressed DOWN") {
 
457
    private final GuiAction nextcomponentAction = new GuiAction("Next component", "Next component", "pressed DOWN") {
463
458
        public void actionPerformed(ActionEvent e) {
464
459
            currentTab.ifPresent(TabContentActions::nextComponent);
465
460
        }
488
483
        this.setMinimumSize(new Dimension(825, 480));
489
484
 
490
485
        setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);
491
 
 
492
 
        //XXX: Moved appTab from creategui needs further refacotring
493
 
        //kyrke 2018-05-20
494
 
        appTab = new ExtendedJTabbedPane<TabContent>() {
 
486
        appTab= new ExtendedJTabbedPane<TabContent>() {
495
487
            @Override
496
488
            public Component generator() {
497
489
                return new TabComponent(this) {
556
548
            Logger.log("Error loading L&F: " + exc);
557
549
        }
558
550
 
559
 
        if (Platform.isMac()) {
560
 
 
561
 
            try {
562
 
                new SpecialMacHandler(guiFrameController);
563
 
            } catch (NoClassDefFoundError e) {
564
 
                //Failed loading special mac handler, ignore and run program without MacOS integration
565
 
            }
566
 
 
567
 
            //XXX Refactor to sperate function, only a test to see of this fixes issues for TAPAAL on Java9 bug #1764383
568
 
            Application app = Application.getApplication();
569
 
            try {
570
 
                Image appImage;
571
 
                appImage = ImageIO.read(Thread.currentThread().getContextClassLoader().getResource(ResourceManager.imgPath + "icon.png"));
572
 
                app.setDockIconImage(appImage);
573
 
            } catch (IOException e) {
574
 
                Logger.log("Error loading Image");
575
 
            }
 
551
 
 
552
        if (Platform.isMac()){
576
553
 
577
554
            //Set specific settings
578
555
            System.setProperty("apple.laf.useScreenMenuBar", "true");
603
580
    private void buildMenus() {
604
581
        menuBar = new JMenuBar();
605
582
 
606
 
        int shortcutkey = Toolkit.getDefaultToolkit().getMenuShortcutKeyMask();
607
 
 
608
 
        menuBar.add(buildMenuFiles(shortcutkey));
609
 
        menuBar.add(buildMenuEdit(shortcutkey));
610
 
        menuBar.add(buildMenuView(shortcutkey));
 
583
        menuBar.add(buildMenuFiles());
 
584
        menuBar.add(buildMenuEdit());
 
585
        menuBar.add(buildMenuView());
611
586
        menuBar.add(buildMenuDraw());
612
587
        menuBar.add(buildMenuAnimation());
613
588
        menuBar.add(buildMenuTools());
617
592
 
618
593
    }
619
594
 
620
 
    private JMenu buildMenuEdit(int shortcutkey) {
 
595
    private JMenu buildMenuEdit() {
621
596
 
622
597
        /* Edit Menu */
623
598
        JMenu editMenu = new JMenu("Edit");
672
647
        return drawMenu;
673
648
    }
674
649
 
675
 
    private JMenu buildMenuView(int shortcutkey) {
 
650
    private JMenu buildMenuView() {
676
651
        /* ViewMenu */
677
652
        JMenu viewMenu = new JMenu("View");
678
653
        viewMenu.setMnemonic('V');
786
761
 
787
762
        toolsMenu.add(netStatisticsAction).setMnemonic('i');
788
763
 
789
 
 
790
 
        //JMenuItem batchProcessing = new JMenuItem("Batch processing");
791
764
        JMenuItem batchProcessing = new JMenuItem(batchProcessingAction);
792
765
        batchProcessing.setMnemonic('b');
793
766
        toolsMenu.add(batchProcessing);
800
773
        smartDrawDialog.setMnemonic('D');
801
774
        toolsMenu.add(smartDrawDialog);
802
775
 
803
 
        //Stip off timing information
804
776
        JMenuItem stripTimeDialog = new JMenuItem(stripTimeDialogAction);
805
777
        stripTimeDialog.setMnemonic('e');
806
778
        toolsMenu.add(stripTimeDialog);
940
912
                }
941
913
            };
942
914
 
943
 
            //JMenuItem newItem = new JMenuItem(a);
944
 
 
945
915
            zoomMenu.add(newZoomAction);
946
916
        }
947
917
 
1262
1232
                // Enable all draw actions
1263
1233
                startAction.setSelected(false);
1264
1234
 
1265
 
                if (getCurrentTab().isInAnimationMode()) {
1266
 
                    getCurrentTab().getAnimator().restoreModel();
1267
 
                    hideComponentWindow();
1268
 
                }
1269
 
 
1270
 
                getCurrentTab().switchToEditorComponents();
1271
 
 
1272
1235
                break;
1273
1236
            case animation:
1274
 
                getCurrentTab().switchToAnimationComponents(true);
1275
1237
                startAction.setSelected(true);
1276
1238
 
1277
1239
                break;
1299
1261
        a.dispose();
1300
1262
    }
1301
1263
 
1302
 
    private void hideComponentWindow() {
1303
 
        ArrayList<PetriNetObject> selection = getCurrentTab().drawingSurface().getGuiModel().getPNObjects();
1304
 
 
1305
 
        for (PetriNetObject pn : selection) {
1306
 
            if (pn instanceof TimedPlaceComponent) {
1307
 
                TimedPlaceComponent place = (TimedPlaceComponent) pn;
1308
 
                place.showAgeOfTokens(false);
1309
 
            } else if (pn instanceof TimedTransitionComponent) {
1310
 
                TimedTransitionComponent transition = (TimedTransitionComponent) pn;
1311
 
                transition.showDInterval(false);
1312
 
            }
1313
 
        }
1314
 
    }
1315
 
 
1316
1264
    //XXX temp while refactoring, kyrke - 2019-07-25, should only be called from TabContent
1317
1265
    @Override
1318
1266
    public void updateMode(Pipe.ElementType _mode) {
1384
1332
 
1385
1333
    @Override
1386
1334
    public void setShowToolTipsSelected(boolean b) {
1387
 
        showTokenAgeAction.setSelected(b);
 
1335
        showToolTipsAction.setSelected(b);
1388
1336
    }
1389
1337
 
1390
1338
    @Override
1444
1392
        return false;
1445
1393
    }
1446
1394
 
1447
 
    private JMenu buildMenuFiles(int shortcutkey) {
 
1395
    private JMenu buildMenuFiles() {
1448
1396
        JMenu fileMenu = new JMenu("File");
1449
1397
        fileMenu.setMnemonic('F');
1450
1398
 
1575
1523
                /* A JAR path */
1576
1524
                String jarPath = dirURL.getPath().substring(5, dirURL.getPath().indexOf('!')); // strip out only the JAR
1577
1525
                // file
1578
 
                JarFile jar = new JarFile(URLDecoder.decode(jarPath, "UTF-8"));
 
1526
                JarFile jar = new JarFile(URLDecoder.decode(jarPath, StandardCharsets.UTF_8));
1579
1527
                Enumeration<JarEntry> entries = jar.entries(); // gives ALL entries in jar
1580
1528
                Set<String> result = new HashSet<String>(); // avoid duplicates in case it is a subdirectory
1581
1529
                while (entries.hasMoreElements()) {
1626
1574
        return appTab.getTitleAt(appTab.getSelectedIndex());
1627
1575
    }
1628
1576
 
 
1577
    //XXX: Needs further cleanup
 
1578
    @Deprecated
1629
1579
    public boolean isShowingDelayEnabledTransitions() {
1630
 
        //XXX:
1631
 
        return true;
1632
 
        //return showDelayEnabledTransitions;
 
1580
        return showDelayEnabledTransitionsAction.isSelected();
1633
1581
    }
1634
1582
 
1635
1583
    public boolean showZeroToInfinityIntervals() {