diff -r 3b8b1da2ff29 -r 12b1f4649ab1 src/Tools/GraphBrowser/awt/TextFrame.java --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/GraphBrowser/awt/TextFrame.java Fri Jul 16 12:55:02 2021 +0200 @@ -0,0 +1,27 @@ +/*************************************************************************** + Title: awt/TextFrame.java + Author: Stefan Berghofer, TU Muenchen + + This class defines a simple text viewer. +***************************************************************************/ + +package isabelle.awt; + +import java.awt.*; +import java.awt.event.*; + +public class TextFrame extends Frame implements ActionListener { + public void actionPerformed(ActionEvent evt) { + setVisible(false); + } + + public TextFrame(String title,String text) { + super(title); + TextArea ta = new TextArea(text,200,80); + Button bt = new Button("Dismiss"); + bt.addActionListener(this); + ta.setEditable(false); + add("Center", ta); + add("South", bt); + } +}