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