src/Tools/GraphBrowser/awt/TextFrame.java
changeset 74015 12b1f4649ab1
parent 74011 1d366486a812
equal deleted inserted replaced
74014:3b8b1da2ff29 74015:12b1f4649ab1
       
     1 /***************************************************************************
       
     2   Title:      awt/TextFrame.java
       
     3   Author:     Stefan Berghofer, TU Muenchen
       
     4 
       
     5   This class defines a simple text viewer.
       
     6 ***************************************************************************/
       
     7 
       
     8 package isabelle.awt;
       
     9 
       
    10 import java.awt.*;
       
    11 import java.awt.event.*;
       
    12 
       
    13 public class TextFrame extends Frame implements ActionListener {
       
    14 	public void actionPerformed(ActionEvent evt) {
       
    15 		setVisible(false);
       
    16 	}
       
    17 
       
    18 	public TextFrame(String title,String text) {
       
    19 		super(title);
       
    20 		TextArea ta = new TextArea(text,200,80);
       
    21 		Button bt = new Button("Dismiss");
       
    22 		bt.addActionListener(this);
       
    23 		ta.setEditable(false);
       
    24 		add("Center", ta);
       
    25 		add("South", bt);
       
    26 	}
       
    27 }