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    }