equal
deleted
inserted
replaced
|
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 } |