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);
+	}
+}