001    package escjava.gui;
002    import java.awt.Dimension;
003    import java.awt.Rectangle;
004    import java.awt.Font;
005    import java.awt.event.KeyAdapter;
006    import java.awt.event.KeyEvent;
007    import java.io.*;
008    import javax.swing.*;
009    import javax.swing.text.html.*;
010    import javax.swing.event.*;
011    import java.awt.event.ActionListener;
012    import java.awt.event.ActionEvent;
013    import java.util.Map;
014    import java.util.HashMap;
015    import java.net.*;
016    import java.util.jar.*;
017    
018    public class EscEditor extends JFrame implements ActionListener {
019    
020        final JEditorPane editor;
021        final JScrollPane scroll;
022        final JComboBox fileChoice = null;
023        String[] files;
024    
025        /** Launches an editable text window positioned at the given line,
026            if line is positive (positioned at the beginning if line <= 0). 
027    <p>
028            If istream is not null, then the data is read from that stream, and
029            the filename is treated as the title.
030    <P>
031            If istream is null, then the data is read from the filename.
032    
033        */
034        public EscEditor(String filename, InputStream istream, int line, String[] files, String[] labels) {
035            this.files = files;
036            if (filename != null) setTitle(filename);
037    
038    
039            // setJMenuBar(EscFrame.menubar); // It appears a JMenuBar
040            // cannot be shared - FIXME - but want to use the menus while
041            // looking at the documentation
042    
043            getContentPane().setLayout(new BoxLayout(getContentPane(),BoxLayout.PAGE_AXIS));
044            final File f = istream != null ? null : new File(filename);
045            JEditorPane editor = null;
046            JScrollPane scroll = null;
047            Reader r = null;
048            try {
049                editor = new JEditorPane();
050                editor.setFont(new Font("Monospaced",Font.PLAIN,editor.getFont().getSize()));
051                scroll = new JScrollPane(editor);
052    
053                JPanel jp = new JPanel();
054                jp.setLayout(new BoxLayout(jp,BoxLayout.LINE_AXIS));
055                getContentPane().add(jp);
056    
057                JButton jb;
058                if (f != null) {
059                    jp.add(jb = new JButton("Save"));
060                    jb.addActionListener(new ActionListener() {
061                        public void actionPerformed(ActionEvent e) {
062                            try {
063                            EscEditor.this.editor.write(new FileWriter(f));
064                            } catch (IOException ee) {} // FIXME
065                        }
066                    });
067                    jp.add(jb = new JButton("Reload"));
068                    jb.addActionListener(new ActionListener() {
069                        public void actionPerformed(ActionEvent e) {
070                            try {
071                            EscEditor.this.editor.read(new FileReader(f),null);
072                            } catch (IOException ee) {} // FIXME
073                        }
074                    });
075                }
076                jp.add(new JLabel("Go to line:"));
077                final JTextField jt = new JTextField("");
078                jp.add(jt);
079                jt.setColumns(10);
080                jt.setMaximumSize(jt.getPreferredSize());
081                jt.addActionListener(new ActionListener() {
082                    public void actionPerformed(ActionEvent e) {
083                        String s = jt.getText();
084                        try {
085                                int i = Integer.parseInt(s.trim());
086                                EscEditor.this.scrollToLine(i);
087                        } catch(Exception ee) {}
088                    }
089                });
090                if (files != null) {
091                    final JComboBox fileChoice = new JComboBox(labels);
092                    for (int i = 0; i<files.length; ++i) {
093                        if (files[i].equals(filename)) fileChoice.setSelectedIndex(i);
094                    }
095                    jp.add(fileChoice);
096                    fileChoice.addActionListener(this);
097                }
098    
099                getContentPane().add(scroll);
100                scroll.setPreferredSize(new Dimension(700,400));
101            
102                editor.setEditable(f != null);
103                if (f != null) editor.addKeyListener(
104                    new KeyAdapter() {
105                        public void keyTyped(KeyEvent e) {
106                            if (e.getModifiers() != KeyEvent.META_MASK) return;
107                            if (e.getKeyChar() != 's') return;
108                            try {
109                                EscEditor.this.editor.write(new FileWriter(f));
110                            } catch (Exception ee) {
111                                // FIXME - failed to save
112                        }
113                    }
114                });
115            
116                if (istream == null) {
117                    if (f != null) editor.setPage(f.toURL());
118                } else {
119                    // FIXME - It seems there ought to be a way to read from
120                    // the jar file and entry as a URL, but I cannot get that to
121                    // work
122                    
123                    char[] ca = new char[10000];
124                    r = new InputStreamReader(
125                                    new BufferedInputStream(istream));
126                    StringBuffer sb = new StringBuffer(10000);
127                    while (true) {  // FIXME - presuming ready() does not block
128                        int n = r.read(ca);
129                        if (n <= 0) break;
130                        sb.append(ca,0,n);
131                    }
132                    editor.setText(sb.toString());
133    
134                }
135    
136                pack();
137                
138            } catch (Exception e) {
139                if (editor != null) editor.setText("An exception occurred while trying to set up an editor for file " + filename + ": " + e);
140                line = 0;
141            } finally {
142                try {
143                    if (r != null) r.close();
144                } catch (IOException e) {
145                    if (editor != null) editor.setText("An exception occurred while trying to set up an editor for file " + filename + ": " + e);
146                }
147            }
148            this.editor = editor;
149            this.scroll = scroll;
150            if (line>0 && editor != null) scrollToLine(line);
151        }
152    
153        public void actionPerformed(ActionEvent e) {
154            if (e.getSource() == fileChoice) {
155                int i = fileChoice.getSelectedIndex();
156                String filename = files[i];
157                try {
158                    editor.setPage(new File(filename).toURL());
159                    setTitle(filename);
160                } catch (Exception ee) {
161                    JOptionPane.showMessageDialog(this,
162                        "Failed to read from file " + filename + ": " +
163                        ee);
164                }
165            }
166        }
167    
168        public void scrollToLine(int line) {
169            try { if (line > 0) { 
170                int ceol = Project.eol.charAt(0);
171                int neol = Project.eol.length();
172                String text = editor.getText();
173                int i = line;
174                int npos = -neol;
175                int pos = 0;
176                while (--i>=0) {
177                    pos = npos + neol;
178                    npos = text.indexOf(ceol,pos);
179                    if (npos == -1) {
180                        npos = text.length()-1;
181                        break;
182                    }
183                }
184                Rectangle r = editor.modelToView(pos);
185                int height = scroll.getViewport().getExtentSize().height;
186                int top = r.y - height*4/10;
187                r = new Rectangle(0,top,50,top+height*9/10);
188                editor.scrollRectToVisible(r);
189                //editor.setCaretPosition(pos);
190                //editor.moveCaretPosition(npos-1);
191                editor.select(pos,npos-1);
192    //          editor.setSelectionStart(pos);
193    //          editor.setSelectionEnd(npos-1);
194                pack();
195            }} catch (Exception e) {} 
196                    // If an exception occurs, just don't bother to scroll
197        }
198    
199    
200        static Map map = new HashMap();
201    
202        static public EscEditor make(String filename, int line, 
203                                    String[] files, String[] labels) {
204            try {
205    
206                int p = filename.indexOf(".jar:");
207                File f = null;
208                String id;
209                InputStream is = null;
210                if (p != -1) {
211                    String jarname = filename.substring(0,p+4);
212                    String fn = filename.substring(p+5);
213                    JarFile jf = new JarFile(jarname);
214                    JarEntry je = jf.getJarEntry(fn);
215                    id = ("jar:file:/" + jarname + "!/" + fn);
216                    is = jf.getInputStream(je);
217                    
218                } else {
219                    f = new File(filename);
220                    id = f.getCanonicalPath();
221                }
222                Object o = map.get(id);
223                EscEditor e;
224                if (o == null) {
225                        e = new EscEditor(filename,is,line,files,labels);
226                        map.put(id,e);
227                } else {
228                        e = (EscEditor)o;
229                        e.scrollToLine(line);
230                }
231                return e;
232    
233            } catch (Exception ee) {
234                EscEditor ed = new EscEditor(null,null,1,null,null);
235                ed.editor.setText("ERROR - Failed to create an editor for file " + filename + " :: " + ee);
236                return ed;
237            }
238        }
239    
240        public void showit() {
241            FrameShower.show(this);
242        }
243    }