diff -r 3b8b1da2ff29 -r 12b1f4649ab1 src/Tools/GraphBrowser/awt/MessageDialog.java --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/GraphBrowser/awt/MessageDialog.java Fri Jul 16 12:55:02 2021 +0200 @@ -0,0 +1,53 @@ +/*************************************************************************** + Title: awt/MessageDialog.java + Author: Stefan Berghofer, TU Muenchen + + This class defines a dialog window for displaying messages and buttons. +***************************************************************************/ + +package isabelle.awt; + +import java.awt.*; +import java.awt.event.*; + +public class MessageDialog extends Dialog implements ActionListener { + String txt; + + public String getText() { return txt; } + + public void actionPerformed(ActionEvent evt) { + txt = evt.getActionCommand(); + setVisible(false); + } + + public MessageDialog(Frame parent,String title,String text,String []buttons) { + super(parent,title,true); + int i; + Panel p1=new Panel(),p2=new Panel(); + p1.setLayout(new FlowLayout(FlowLayout.CENTER,0,0)); + p2.setLayout(new FlowLayout()); + setFont(new Font("Helvetica", Font.PLAIN, 14)); + setLayout(new GridLayout(2,1)); + + while (true) { + int pos=text.indexOf(' '); + if (pos<0) { + p1.add(new Label(text)); + break; + } else { + p1.add(new Label(text.substring(0,pos))); + if (pos+1==text.length()) + break; + else + text=text.substring(pos+1); + } + } + + add(p1);add(p2); + for (i=0;i