    001    /*  Copyright 2004, David R. Cok
    002        Originally generated as part of a GUI interface to the
    003        Esc/Java2 application.
    004    */
    005
    006    package escjava.gui;
    007
    008    import java.awt.Frame;
    009    import java.awt.EventQueue;
    010
    011    /** The FrameShower is used to be sure that a Frame is shown
    012        through a call that is made on the Event thread.
    013        This is generally advised in order to avoid race conditions
    014        in the GUI painting itself.  Use this class by calling the
    015        static method to queue a new instance of an object to be
    016        shown.
    017     */
    018    public class FrameShower implements Runnable {
    019
    020        //@ non_null spec_public
    021        final private Frame frame;
    022
    023        /** Creates a FrameShower object holding the given Frame.
    024         */
    025        //@ requires frame != null;
    026        //@ also ensures this.frame == frame;
    027        //@ pure
    028        protected FrameShower(Frame frame) {
    029            this.frame = frame;
    030        }
    031
    032        /** Called by the EventQueue as the task to be
    033            accomplished - it shows/makes visible the
    034            given frame.
    035         */
    036        // Cannot call this pure because it certainly changes the GUI.
    037        //@ also ensures \not_modified(frame);
    038        public void run() {
    039            frame.show();
    040        }
    041
    042        // This is going to need some kind of modifies clause - it
    043        // modifies the event logic and the gui at least.
    044        //@ requires frame != null;
    045        static void show(Frame frame) {
    046            EventQueue.invokeLater(new FrameShower(frame));
    047        }
    048    }
    049
    050