~tapaal-contributor/tapaal/unselect-objects-after-undo-1894108

import java.net.*;

import java.nio.charset.StandardCharsets;

import java.util.*;

import java.util.jar.JarEntry;

import java.util.jar.JarFile;

import javax.swing.*;

import net.tapaal.helpers.Reference.Reference;

import net.tapaal.swinghelpers.ExtendedJTabbedPane;

import net.tapaal.swinghelpers.ToggleButtonWithoutText;

import pipe.gui.Pipe.ElementType;

import pipe.gui.action.GuiAction;

import pipe.gui.widgets.WorkflowDialog;

 

    private final String frameTitle;

 

    private int newNameCounter = 1;

 

    final MutableReference<GuiFrameControllerActions> guiFrameController = new MutableReference<>();

 

    private final StatusBar statusBar;

    private JMenuBar menuBar;

    private JToolBar drawingToolBar;

    private final JLabel featureInfoText = new JLabel();

    private JComboBox<String> timeFeatureOptions = new JComboBox(new String[]{"No", "Yes"});

            currentTab.ifPresent(o -> o.setMode(ElementType.ANNOTATION));

        }

    };

 

    private final GuiAction showTokenAgeAction = new GuiAction("Display token age", "Show/hide displaying the token age 0.0 (when hidden the age 0.0 is drawn as a dot)", KeyStroke.getKeyStroke('9', shortcutkey), true) {

        public void actionPerformed(ActionEvent e) {

            currentTab.ifPresent(TabContentActions::stepBackwards);

        }

    };

        public void actionPerformed(ActionEvent e) {

            currentTab.ifPresent(TabContentActions::previousComponent);

        }

 

    private JCheckBoxMenuItem showZeroToInfinityIntervalsCheckBox;

    private JCheckBoxMenuItem showTokenAgeCheckBox;

 

    private JMenu zoomMenu;

 

        this.setMinimumSize(new Dimension(825, 480));

 

        setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);

            @Override

            public Component generator() {

                return new TabComponent(this) {

        }

 

 

 

            //Set specific settings

            System.setProperty("apple.laf.useScreenMenuBar", "true");

     **/

    private void buildMenus() {

        menuBar = new JMenuBar();

        menuBar.add(buildMenuFiles());

        menuBar.add(buildMenuEdit());

        menuBar.add(buildMenuView());

        menuBar.add(buildMenuDraw());

        menuBar.add(buildMenuAnimation());

        menuBar.add(buildMenuTools());

        menuBar.add(buildMenuHelp());

 

    private JMenu buildMenuDraw() {

        /* Draw menu */

        drawMenu.setMnemonic('D');

        return drawMenu;

    }

 

    private JMenu buildMenuView() {

        /* ViewMenu */

        viewMenu.setMnemonic('V');

 

        zoomMenu = new JMenu("Zoom");

 

        addCheckboxMenuItem(viewMenu, showEnabledTransitionsAction);

 

 

        showZeroToInfinityIntervalsCheckBox = addCheckboxMenuItem(viewMenu, showZeroToInfinityIntervals(), showZeroToInfinityIntervalsAction);

 

 

    private JMenu buildMenuAnimation() {

        /* Simulator */

        animateMenu.setMnemonic('A');

        animateMenu.add(startAction);

 

        animateMenu.add(stepbackwardAction);

        animateMenu.add(stepforwardAction);

 

        animateMenu.add(prevcomponentAction);

 

        animateMenu.add(nextcomponentAction);

        drawingToolBar.addSeparator();

        drawingToolBar.setRequestFocusEnabled(false);

 

        // Create panel to put toolbars in

        JPanel toolBarPanel = new JPanel();

        toolBarPanel.setLayout(new FlowLayout(FlowLayout.LEFT, 0, 0));

                exportTraceAction.setEnabled(false);

                importTraceAction.setEnabled(false);

 

                annotationAction.setEnabled(true);

                deleteAction.setEnabled(true);

                selectAllAction.setEnabled(true);

 

                stepbackwardAction.setEnabled(false);

                stepforwardAction.setEnabled(false);

                prevcomponentAction.setEnabled(false);

                    WorkflowDialog.showDialog();

                }

 

                //Enable editor focus traversal policy

                setFocusTraversalPolicy(new EditorFocusTraversalPolicy());

                fixBug812694GrayMenuAfterSimulationOnMac();

            case animation:

                enableAllActions(true);

 

                annotationAction.setEnabled(false);

                deleteAction.setEnabled(false);

                selectAllAction.setEnabled(false);

 

                alignToGrid.setEnabled(false);

 

                showConstantsAction.setEnabled(false);

                showQueriesAction.setEnabled(false);

 

                stepbackwardAction.setEnabled(true);

                stepforwardAction.setEnabled(true);

                prevcomponentAction.setEnabled(true);

 

                getCurrentTab().getAnimationController().requestFocusInWindow();

 

                //Enable simulator focus traversal policy

                setFocusTraversalPolicy(new SimulatorFocusTraversalPolicy());

 

                importTraceAction.setEnabled(false);

                verifyAction.setEnabled(false);

 

                annotationAction.setEnabled(false);

                selectAllAction.setEnabled(false);

 

                stepbackwardAction.setEnabled(false);

                stepforwardAction.setEnabled(false);

 

                enableAllActions(false);

 

                // Disable All Actions

                setFocusTraversalPolicy(null);

 

                break;

                break;

            case noNet:

                setFeatureInfoText(null);

                break;

 

            default:

 

        // Enable actions based on GUI mode

        enableGUIActions(mode);

    }

 

    private void fixBug812694GrayMenuAfterSimulationOnMac() {

        a.dispose();

    }

 

    @Override

    }

 

 

        showTokenAgeAction.setSelected(b);

    }

 

    public void setTitle(String title) {

        super.setTitle((title == null) ? frameTitle : frameTitle + ": " + title);

    }

        zoomComboBox.addActionListener(zoomComboListener);

    }

 

    private boolean canNetBeSavedAndShowMessage() {

        if (getCurrentTab().network().paintNet()) {

            return true;