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 }