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