ExploreAction.java 文件源码

/**
 * Creates a modal dialog that will interrupt this thread, when the
 * cancel button is pressed.
 */
private JDialog createCancelDialog() {
    JDialog result;
    // create message dialog
    JOptionPane message = new JOptionPane(
        isAnimated() ? getAnimationPanel()
            : new Object[] {getStateCountLabel(), getTransitionCountLabel()},
        JOptionPane.PLAIN_MESSAGE);
    message.setOptions(new Object[] {getCancelButton()});
    result = message.createDialog(getFrame(), "Exploring state space");
    result.pack();
    result.setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE);
    result.addWindowListener(new WindowAdapter() {
        @Override
        public void windowClosing(WindowEvent e) {
            ExploreThread.this.interrupt();
        }
    });
    result.setAlwaysOnTop(true);
    return result;
}