    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    }