    001    /*  Copyright 2004, David R. Cok
    002        Originally generated as part of a GUI interface to the
    003        Esc/Java2 application.
    004    */
    005
    006    package escjava.gui;
    007
    008    import javax.swing.*;
    009    import javax.swing.event.*;
    010    import java.awt.*;
    011    import java.awt.event.*;
    012
    013    /** This class generates a JFrame that contains the given
    014        uneditable text.  The text is in a Monospaced font
    015        appropriate for showing text where column alignment from
    016        line to line is important.
    017     */
    018    public class EscOutputFrame extends JFrame {
    019
    020        /** Create a JFrame with the given frame title and text.
    021         */
    022        //@ requires title != null;
    023        //@ requires text != null;
    024        public EscOutputFrame(String title, String text) {
    025            textArea = new JTextArea(text);
    026            textArea.setFont(new Font("Monospaced",Font.PLAIN,textArea.getFont().getSize()));
    027            textArea.setColumns(50);
    028            textArea.setEditable(false);
    029            textArea.setLineWrap(true);
    030            textArea.addMouseListener( new MouseInputAdapter() {
    031                /* On receiving a mouse click, we identify the line in which
    032                   the click occurred, grab the text for that line and send the
    033                   text for that line as a task to the windowTasks queue (which
    034                   is supposed to launch an editor).
    035                */
    036                public void mouseClicked(MouseEvent e) {
    037                    JTextArea textArea = (JTextArea)e.getSource();
    038                    try {
    039                        int p = textArea.getCaretPosition();
    040                        int line = textArea.getLineOfOffset(p);
    041                        textArea.setSelectionStart(textArea.getLineStartOffset(line));
    042                        textArea.setSelectionEnd(textArea.getLineEndOffset(line));
    043                        String s = textArea.getSelectedText();
    044                        WindowThread.windowTasks.addTask(s);
    045                    } catch (Exception ee) {}
    046                            // If an exception occurs, we simply don't display a window
    047                }
    048            });
    049            JScrollPane scroll = new JScrollPane(textArea);
    050            scroll.setPreferredSize(new Dimension(400,300));
    051            getContentPane().add(scroll, BorderLayout.CENTER);
    052            setLocation(500,100);
    053            setTitle(title);
    054            pack();
    055            showit();
    056        }
    057
    058        /** Causes the event subsystem to display the frame. */
    059        public void showit() {
    060            FrameShower.show(this);
    061        }
    062
    063        //@ non_null
    064        private JTextArea textArea;
    065
    066        /** Appends text to that already contained in the frame. */
    067        //@ requires s != null;
    068        public void appendText(String s) {
    069            textArea.append(s);
    070            showit();
    071        }
    072
    073        /** Replaces the text in the frame with the given text. */
    074        //@ requires s != null;
    075        public void setText(String s) {
    076            textArea.setText(s);
    077            showit();
    078        }
    079    }