    001    package escjava.gui;
    002
    003    import javax.swing.*;
    004    import javax.swing.tree.*;
    005    import javax.swing.event.*;
    006    import java.awt.*;
    007    import java.awt.event.*;
    008    import java.io.File;
    009    import javax.swing.filechooser.FileFilter;
    010    import java.io.StringReader;
    011    import java.io.BufferedReader;
    012    import java.util.Iterator;
    013    import java.util.ArrayList;
    014    import java.util.Timer;
    015    import java.util.TimerTask;
    016
    017    import escjava.Status;
    018    import javafe.InputEntry;
    019    import javafe.ast.CompilationUnit;
    020
    021    //import com.apple.eawt.*;
    022
    023    public class EscFrame extends JFrame {
    024
    025        static public final boolean runningOnMac = (System.getProperty("mrj.version") != null);
    026
    027        static public /*@non_null*/ String addDots(/*@non_null*/ String s) {
    028            if (!runningOnMac) return s + "...";
    029            return s;
    030        }
    031
    032        static {
    033            // Checks to see if we are running on a Mac
    034            if (runningOnMac) {
    035                // If so, then puts the menubar at the top of the screen
    036                // instead of the top of the window
    037                System.setProperty("apple.laf.useScreenMenuBar","true");
    038            }
    039        }
    040
    041        static public final /*@non_null*/ JMenuBar menubar = new JMenuBar();
    042        public EscOptions escoptionPanel;
    043        public GuiOptionsPanel guioptionPanel;
    044        private JTextArea listArea;
    045        static JLabel label;
    046        JScrollPane treeView;
    047        JLabel sizeinfo;
    048        JComponent guilight;
    049        JComponent proverlight;
    050        static JTree tree;
    051
    052        JTextField currentdirText;
    053        JTextField classpathText, specspathText;
    054        JFileChooser fc = new JFileChooser(GUI.gui.options.currentdir);
    055
    056        public EscFrame() {
    057            setTitle("ESC/Java2 (Version: " + escjava.Version.VERSION+ ")");
    058            setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE);
    059
    060            buildGUI(this);
    061
    062            pack();
    063
    064            EscHtml jf = EscHtml.make("Welcome","escjava/gui/welcome.html",
    065                            this,100,100,500,500);
    066
    067            FrameShower.show(this);
    068
    069            jf.showit();
    070
    071        }
    072
    073        private void buildGUI(final /*@non_null*/ JFrame frame) {
    074            JTabbedPane tabbedPane = new JTabbedPane();
    075            frame.getContentPane().add(tabbedPane, BorderLayout.CENTER);
    076            guioptionPanel = new GuiOptionsPanel();
    077            tabbedPane.addTab("GUI Options",null,guioptionPanel,
    078                    "Options for controlling the User Interface");
    079
    080            escoptionPanel = new EscOptions(GUI.options());
    081            tabbedPane.addTab("ESC Options", null, escoptionPanel,
    082                    "Options for controlling the static checking tool");
    083
    084            JPanel filesPanel = new JPanel(new BorderLayout());
    085            tabbedPane.addTab("Project files", null, filesPanel,
    086                    "Tools to control the files used in this project");
    087            JPanel topFilesPanel = new JPanel(new GridLayout(0,1));
    088            filesPanel.add(topFilesPanel,BorderLayout.NORTH);
    089    /* Changing the user.dir during a program appears to be problematic - at
    090       least on a Mac, new File instances do not appear to use the new value.
    091
    092            topFilesPanel.add(new JLabel("Current directory:"));
    093            topFilesPanel.add(currentdirText = new JTextField(escjava.Main.options.currentdir));
    094            currentdirText.addActionListener( new ActionListener() {
    095                public void actionPerformed(ActionEvent e) {
    096                    String s = currentdirText.getText();
    097                    if (s.equals(escjava.Main.options.currentdir)) return;
    098                    escjava.Main.options.currentdir = s;
    099                    System.setProperty("user.dir",s);
    100                    GUI.gui.restart(null);
    101                    label.setText("Clearing all results because the Working Directory changed");
    102                }
    103            });
    104            currentdirText.addFocusListener( new FocusAdapter() {
    105                public void focusLost(FocusEvent e) {
    106                    String s = currentdirText.getText();
    107                    if (s.equals(escjava.Main.options.currentdir)) return;
    108                    escjava.Main.options.currentdir = s;
    109                    System.setProperty("user.dir",s);
    110                    GUI.gui.restart(null);
    111                    label.setText("Clearing all results because the Working Directory changed");
    112                }
    113            });
    114    */
    115            topFilesPanel.add(new JLabel("CLASSPATH:"));
    116            topFilesPanel.add(classpathText = new JTextField(escjava.Main.options.userPath,50));
    117            classpathText.addActionListener( new ActionListener() {
    118                public void actionPerformed(ActionEvent e) {
    119                    String s = classpathText.getText();
    120                    if (s.equals(escjava.Main.options.userPath)) return;
    121                    escjava.Main.options.userPath = s;
    122                    GUI.gui.restart(null);
    123                    label.setText("Clearing all results because the CLASSPATH changed");
    124                }
    125            });
    126            classpathText.addFocusListener( new FocusAdapter() {
    127                public void focusLost(FocusEvent e) {
    128                    String s = classpathText.getText();
    129                    if (s.equals(escjava.Main.options.userPath)) return;
    130                    escjava.Main.options.userPath = s;
    131                    GUI.gui.restart(null);
    132                    label.setText("Clearing all results because the CLASSPATH changed");
    133                }
    134            });
    135
    136            topFilesPanel.add(new JLabel("Specs path:"));
    137            topFilesPanel.add(specspathText = new JTextField(escjava.Main.options().specspath,50));
    138            specspathText.addActionListener( new ActionListener() {
    139                public void actionPerformed(ActionEvent e) {
    140                    String s = specspathText.getText();
    141                    if (s.equals(escjava.Main.options().specspath)) return;
    142                    escjava.Main.options().specspath = s;
    143                    GUI.gui.restart(null);
    144                    label.setText("Clearing all results because the Specs path changed");
    145                }
    146            });
    147            specspathText.addFocusListener( new FocusAdapter() {
    148                public void focusLost(FocusEvent e) {
    149                    String s = specspathText.getText();
    150                    if (s.equals(GUI.gui.options().specspath)) return;
    151                    GUI.gui.options().specspath = s;
    152                    GUI.gui.restart(null);
    153                    label.setText("Clearing all results because the Specs path changed");
    154                }
    155            });
    156
    157
    158
    159            topFilesPanel.add(new JLabel("Files, directories, classes, packages and lists to process:"));
    160            listArea = new JTextArea();
    161            filesPanel.add(new JScrollPane(listArea),BorderLayout.CENTER);
    162            //listArea.getParent().setPreferredSize(new Dimension(300,200));
    163            loadTextArea();
    164            listArea.addFocusListener(
    165                new FocusAdapter() {
    166                    public void focusLost(FocusEvent e) {
    167                        if (saveTextArea()) {
    168                            GUI.gui.restart(null);
    169                            label.setText("Clearing all results because the input changed");
    170                        }
    171                    }
    172                });
    173
    174
    175            JPanel panel = new JPanel(new GridLayout(2,1));
    176
    177            JPanel buttonPanel = new JPanel(new FlowLayout());
    178            panel.add(buttonPanel);
    179
    180            JButton button = new JButton("Reload");
    181            buttonPanel.add(button);
    182            button.addActionListener(new ActionListener() {
    183                public void actionPerformed(ActionEvent e) {
    184                    GUI.processTasks.addTask(new Integer(GUI.RELOAD));
    185            } });
    186
    187            button = new JButton("Clear");
    188            buttonPanel.add(button);
    189            button.addActionListener(new ActionListener() {
    190                public void actionPerformed(ActionEvent e) { escAction(GUI.CLEAR); } });
    191
    192            button = new JButton("Check");
    193            button.addActionListener(new ActionListener() {
    194                public void actionPerformed(ActionEvent e) { escAction(GUI.CHECK); } });
    195            buttonPanel.add(button);
    196
    197            button = new JButton("Stop");
    198            buttonPanel.add(button);
    199            button.addActionListener(new ActionListener() {
    200                public void actionPerformed(ActionEvent e) {
    201                    synchronized (GUI.processTasks) {
    202                        GUI.processTasks.clear();
    203                        GUI.gui.stop = true;
    204                        escjava.ProverManager.kill();
    205                        GUI.processTasks.addTask(GUI.STOP);
    206                        //System.out.println("REQUESTED STOP");
    207                    }
    208                } });
    209
    210            JPanel infopanel = new JPanel();
    211            infopanel.setLayout(new BoxLayout(infopanel,BoxLayout.LINE_AXIS));
    212            panel.add(infopanel);
    213
    214            label = new JLabel(" ");
    215            infopanel.add(label);
    216            frame.getContentPane().add(panel, BorderLayout.NORTH);
    217
    218            infopanel.add(Box.createHorizontalGlue());
    219            sizeinfo = new JLabel(" ");
    220            infopanel.add(sizeinfo);
    221            updateSizeInfo();
    222            TimerTask tt = new TimerTask() {
    223                public void run() { updateSizeInfo(); }
    224            };
    225            Timer ttt = new Timer(true);
    226            ttt.schedule(tt,0,1000);
    227
    228            guilight = new JPanel();
    229            Dimension d = new Dimension(10,10);
    230            guilight.setMaximumSize(d);
    231            guilight.setMinimumSize(d);
    232            guilight.setToolTipText("Shows the status of the GUI:" +
    233                    "Blue - waiting for processing commands; " +
    234                    "Green - parsing, typechecking, VC generation; " +
    235                    "Yellow - waiting for the prover");
    236            infopanel.add(guilight);
    237
    238            proverlight = new JPanel();
    239            proverlight.setMaximumSize(d);
    240            proverlight.setMinimumSize(d);
    241            proverlight.setToolTipText("Shows the status of the Prover:" +
    242                    "Blue - waiting for VCs to check; " +
    243                    "Green - proving; " +
    244                    "Black - prover is not executing");
    245            infopanel.add(proverlight);
    246
    247            showGuiLight(0);
    248            showProverLight(0);
    249            escjava.ProverManager.listener = new escjava.ProverManager.Listener() {
    250                public void stateChanged(int i) {
    251                    showProverLight(i);
    252                    if (i != 0) showGuiLight(3-i);
    253                }};
    254
    255            tree = new JTree(GUI.gui.treeModel);
    256            tree.getSelectionModel().setSelectionMode(TreeSelectionModel.DISCONTIGUOUS_TREE_SELECTION);
    257            if (guioptionPanel.settings.autoExpand) {
    258                int k=GUI.gui.treeModel.getChildCount(GUI.gui.treeModel.getRoot());
    259                while (k > 0) tree.expandRow(--k);
    260            }
    261            DefaultTreeCellRenderer r = new EscRenderer();
    262            r.setLeafIcon(null);
    263            r.setOpenIcon(null);
    264            r.setClosedIcon(null);
    265    /*
    266            TreeCellRenderer r = new EscTreeCellRenderer();
    267    */
    268            tree.addMouseListener(
    269                new MouseInputAdapter() {
    270                  //@ also
    271                  //@    requires e != null;
    272                    public void mouseClicked(MouseEvent e) {
    273                        if (e.getClickCount() != 1) return;
    274                        Object o = ((DefaultMutableTreeNode)
    275                            tree.getClosestPathForLocation(e.getX(),e.getY()).
    276                                        getLastPathComponent()).getUserObject();
    277                        if ((e.getModifiers() & MouseEvent.ALT_MASK) != 0)
    278                            // Alt + click --> error window
    279                            WindowThread.windowTasks.addTask(o);
    280                        else if ((e.getModifiers() & MouseEvent.CTRL_MASK) != 0) {
    281                            // Ctrl + click --> editor window
    282                            if (o instanceof GUI.EscTreeValue) {
    283                                showEditor((GUI.EscTreeValue)o);
    284                            }
    285                        }
    286                    }});
    287            tree.setCellRenderer(r);
    288
    289            tree.putClientProperty("JTree.lineStyle", "Angled");
    290            tree.setShowsRootHandles(true);
    291            ToolTipManager.sharedInstance().registerComponent(tree);
    292            tree.setRootVisible(false);
    293            //tree.setEditable(true);
    294            //tree.setDragEnabled(true);
    295            treeView = new JScrollPane(tree);
    296            //treeView.setPreferredSize(new Dimension(400,300));
    297            treeView.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_NEVER);
    298            tabbedPane.addTab("Results", null, treeView,
    299                    "Results of checking the project files");
    300            // Default tab is Project tab if there are no files set,
    301            // otherwise it is the Results tab
    302            int def = 3;
    303            if (listArea.getText().length() == 0) def = 2;
    304            tabbedPane.setSelectedIndex(def);
    305
    306            // Menus
    307
    308            frame.setJMenuBar(menubar);
    309            JMenu menu = new JMenu("File");
    310            menubar.add(menu);
    311
    312            JMenuItem mi;
    313            menu.add(mi = new JMenuItem("New Project"));
    314            mi.addActionListener(
    315                new ActionListener() {
    316                    public void actionPerformed(ActionEvent e) {
    317                        Project.init();
    318                    }
    319                });
    320
    321            menu.add(mi = new JMenuItem(addDots("Open Project")));
    322            mi.addActionListener(
    323                new ActionListener() {
    324                    public void actionPerformed(ActionEvent e) {
    325                        fc.addChoosableFileFilter(
    326                            new FileFilter() {
    327                                public boolean accept(File f) {
    328                                    return !f.isFile() || f.getName().endsWith(".esc");
    329                                }
    330                                public String getDescription() {
    331                                    return "*.esc";
    332                                }
    333                            });
    334                        int returnVal = fc.showOpenDialog(frame);
    335                        if (returnVal == JFileChooser.APPROVE_OPTION) {
    336                            File file = fc.getSelectedFile();
    337                            Project.read(file);
    338                            escoptionPanel.init(escjava.Main.options());
    339                        }
    340                    }
    341                });
    342
    343            menu.add(mi = new JMenuItem("Save Project"));
    344            mi.addActionListener(
    345                new ActionListener() {
    346                    public void actionPerformed(ActionEvent e) {
    347                        if (Project.currentProject != null)
    348                            Project.write();
    349                        else {
    350                            int returnVal = fc.showSaveDialog(frame);
    351                            if (returnVal == JFileChooser.APPROVE_OPTION) {
    352                                File file = fc.getSelectedFile();
    353                                if (file.exists()) {
    354                                    boolean b = JOptionPane.showConfirmDialog(
    355                                        EscFrame.this,
    356                                       "The file " + file.getAbsolutePath() +
    357                                       " already exists - do you want to overwrite it?",
    358                                       "Confirm Save",JOptionPane.OK_CANCEL_OPTION)
    359                                            == JOptionPane.OK_OPTION;
    360                                    if (!b) return;
    361                                }
    362                                Project.write(file);
    363                            }
    364                        }
    365                    }
    366                });
    367
    368            menu.add(mi = new JMenuItem(addDots("SaveAs Project")));
    369            mi.addActionListener(
    370                new ActionListener() {
    371                    public void actionPerformed(ActionEvent e) {
    372                        int returnVal = fc.showSaveDialog(frame);
    373                        if (returnVal == JFileChooser.APPROVE_OPTION) {
    374                            File file = fc.getSelectedFile();
    375                            if (file.exists()) {
    376                                boolean b = JOptionPane.showConfirmDialog(
    377                                    EscFrame.this,
    378                                   "The file " + file.getAbsolutePath() +
    379                                   " already exists - do you want to overwrite it?",
    380                                   "Confirm Save",JOptionPane.OK_CANCEL_OPTION)
    381                                        == JOptionPane.OK_OPTION;
    382                                if (!b) return;
    383                            }
    384                            Project.write(file);
    385                        }
    386                    }
    387                });
    388
    389            if (!runningOnMac) {
    390                menu.add(mi = new JMenuItem("Exit"));
    391                mi.addActionListener( new ActionListener() {
    392                    public void actionPerformed(ActionEvent e) { System.exit(0); }
    393                } );
    394            }
    395
    396            menubar.add(menu = new JMenu("View"));
    397            menu.add(mi = new JMenuItem("Error window"));
    398            mi.addActionListener( new ActionListener() {
    399                public void actionPerformed(ActionEvent e) {
    400                    TreePath[] paths = tree.getSelectionPaths();
    401                    for (int i=0; i<paths.length; ++i) {
    402                        Object o = ((DefaultMutableTreeNode)paths[i].
    403                                        getLastPathComponent()).
    404                                        getUserObject();
    405                        WindowThread.windowTasks.addTask(o);
    406                    }
    407                }
    408            });
    409            menu.add(mi = new JMenuItem("Editor window"));
    410            mi.addActionListener( new ActionListener() {
    411                public void actionPerformed(ActionEvent e) {
    412                    TreePath[] paths = tree.getSelectionPaths();
    413                    for (int i=0; i<paths.length; ++i) {
    414                        Object o = ((DefaultMutableTreeNode)paths[i].
    415                                        getLastPathComponent()).
    416                                        getUserObject();
    417                        GUI.EscTreeValue v = (GUI.EscTreeValue)o;
    418                        showEditor(v);
    419                    }
    420                }
    421            } );
    422
    423
    424
    425            menubar.add(menu = new JMenu("Check"));
    426
    427            menu.add(mi = new JMenuItem("Check All"));
    428            mi.addActionListener(
    429                new ActionListener() {
    430                    public void actionPerformed(ActionEvent e) {
    431                        GUI.processTasks.addTask(new Integer(GUI.CHECK));
    432                    }});
    433
    434            menu.add(mi = new JMenuItem("Check Selected"));
    435            mi.addActionListener(
    436                new ActionListener() {
    437                    public void actionPerformed(ActionEvent e) {
    438                        if (!tree.isSelectionEmpty()) escAction(GUI.CHECK);
    439                    }});
    440
    441            menu.add(mi = new JMenuItem("TypeCheck All"));
    442            mi.addActionListener(
    443                new ActionListener() {
    444                    public void actionPerformed(ActionEvent e) {
    445                        GUI.processTasks.addTask(new Integer(GUI.TYPECHECK));
    446                    }});
    447
    448            menu.add(mi = new JMenuItem("TypeCheck Selected"));
    449            mi.addActionListener(
    450                new ActionListener() {
    451                    public void actionPerformed(ActionEvent e) {
    452                        if (!tree.isSelectionEmpty()) escAction(GUI.TYPECHECK);
    453                    }});
    454
    455            menu.add(mi = new JMenuItem("Parse All"));
    456            mi.addActionListener(
    457                new ActionListener() {
    458                    public void actionPerformed(ActionEvent e) {
    459                        GUI.processTasks.addTask(new Integer(GUI.PARSE));
    460                    }});
    461
    462            menu.add(mi = new JMenuItem("Parse Selected"));
    463            mi.addActionListener(
    464                new ActionListener() {
    465                    public void actionPerformed(ActionEvent e) {
    466                        if (!tree.isSelectionEmpty()) escAction(GUI.PARSE);
    467                    }});
    468
    469            menu.add(mi = new JMenuItem("Resolve All"));
    470            mi.addActionListener(
    471                new ActionListener() {
    472                    public void actionPerformed(ActionEvent e) {
    473                        GUI.processTasks.addTask(new Integer(GUI.RESOLVE));
    474                    }});
    475
    476            menu.add(mi = new JMenuItem("Resolve Selected"));
    477            mi.addActionListener(
    478                new ActionListener() {
    479                    public void actionPerformed(ActionEvent e) {
    480                        if (!tree.isSelectionEmpty()) escAction(GUI.RESOLVE);
    481                    }});
    482
    483            menu.add(mi = new JMenuItem("Clear All"));
    484            mi.addActionListener(
    485                new ActionListener() {
    486                    public void actionPerformed(ActionEvent e) {
    487                        GUI.processTasks.addTask(new Integer(GUI.CLEAR));
    488                    }});
    489
    490            menu.add(mi = new JMenuItem("Clear Selected"));
    491            mi.addActionListener(
    492                new ActionListener() {
    493                    public void actionPerformed(ActionEvent e) {
    494                        if (!tree.isSelectionEmpty()) escAction(GUI.CLEAR);
    495                    }});
    496
    497            menubar.add(menu = new JMenu("Tools"));
    498            menu.add(mi = new JMenuItem("Gen. Skeleton"));
    499            mi.addActionListener( notimp(frame) );
    500
    501            menu.add(mi = new JMenuItem("Garbage Collect"));
    502            mi.addActionListener( new ActionListener() {
    503                    public void actionPerformed(ActionEvent e) {
    504                        System.gc();
    505                    }
    506            });
    507
    508            menubar.add(menu = new JMenu("L&F"));
    509            UIManager.LookAndFeelInfo[] looks = UIManager.getInstalledLookAndFeels();
    510            try {
    511                UIManager.setLookAndFeel(
    512                  UIManager.getSystemLookAndFeelClassName());
    513            } catch (Exception eee) {}  // FIXME
    514            LookAndFeel current = UIManager.getLookAndFeel();
    515            String name = current.getClass().toString().substring(6); // 6 is the length of "class "
    516            ButtonGroup bg = new ButtonGroup();
    517            LAF milaf;
    518            for (int i=0; i<looks.length; ++i) {
    519                menu.add(milaf = new LAF(looks[i]));
    520                milaf.addActionListener(milaf);
    521                if (name.equals(looks[i].getClassName())) {
    522                    milaf.setSelected(true);
    523                }
    524                bg.add(milaf);
    525            }
    526
    527            menubar.add(menu = new JMenu("Help"));
    528    /*
    529            menu.add(mi = new JMenuItem("Usage"));
    530            mi.addActionListener(
    531                new ActionListener() {
    532                    public void actionPerformed(ActionEvent e) {
    533                        new EscOutputFrame("Escjava2 usage","USAGE");
    534                    }
    535                });
    536    */
    537
    538            menu.add(mi = new JMenuItem("Documentation"));
    539            mi.addActionListener(
    540                new ActionListener() {
    541                    public void actionPerformed(ActionEvent e) {
    542                        WindowThread.windowTasks.addTask(new WindowThread.HtmlTask("Documentation",
    543                                    "escjava/gui/escjava2gui.html"));
    544                    }
    545                });
    546
    547            menu.add(mi = new JMenuItem("Issues/Bugs"));
    548            mi.addActionListener(
    549                new ActionListener() {
    550                    public void actionPerformed(ActionEvent e) {
    551                        WindowThread.windowTasks.addTask(new WindowThread.HtmlTask(
    552                                    "Issues & Notes","escjava/gui/issues.html"));
    553                    }
    554                });
    555
    556        }
    557
    558        static private class LAF extends JRadioButtonMenuItem implements ActionListener {
    559            public UIManager.LookAndFeelInfo laf;
    560            public LAF(/*@non_null*/ UIManager.LookAndFeelInfo laf) {
    561                super(laf.getName());
    562                this.laf = laf;
    563            }
    564            public void actionPerformed(ActionEvent e) {
    565                try {
    566                    UIManager.setLookAndFeel(laf.getClassName());
    567                    SwingUtilities.updateComponentTreeUI(GUI.gui.escframe);
    568                } catch (Exception ee) {
    569                    JOptionPane.showMessageDialog(GUI.gui.escframe,"Could not find Look & Feel named " + laf.getName());
    570                }
    571            }
    572        }
    573
    574        public void showEditor(/*@non_null*/ GUI.EscTreeValue v) {
    575            String vname = v.getFilename();
    576            if (vname == null) return;
    577            if (v instanceof GUI.GFCUTreeValue) {
    578                GUI.GFCUTreeValue vv = (GUI.GFCUTreeValue)v;
    579                CompilationUnit cu = vv.cu;
    580                if (cu != null && cu instanceof escjava.RefinementSequence) {
    581                    ArrayList a = ((escjava.RefinementSequence)cu).refinements();
    582                    Iterator i = a.iterator();
    583                    while (i.hasNext()) {
    584                        CompilationUnit rcu = (CompilationUnit)i.next();
    585                        String name = rcu.sourceFile().getHumanName();
    586                        if (!name.equals(vname))
    587                            WindowThread.windowTasks.addTask(name + ":1:");
    588                            // FIXME - would like other elements of the compilation
    589                            // unit to be scrolled to the same method
    590                    }
    591                }
    592            }
    593
    594            WindowThread.windowTasks.addTask( vname + ":" + v.getLine() + ":");
    595        }
    596
    597        public void init() {
    598            classpathText.setText(GUI.gui.options.userPath);
    599            loadTextArea();
    600            tree.setModel(GUI.gui.treeModel);
    601            GUI.gui.treeModel.reload();
    602        }
    603
    604        static /*@non_null*/ ActionListener notimp(final /*@non_null*/ JFrame parent) {
    605            return new ActionListener() {
    606                public void actionPerformed(ActionEvent e) {
    607                    //System.out.println("NOT IMPLEMENTED");
    608                    JOptionPane.showMessageDialog(parent,"Menu item not implemented");
    609                }
    610            };
    611        }
    612
    613        static public void checkAction() {
    614            if (tree.isSelectionEmpty()) {
    615                System.out.println("CHECKING EVERYTHING");
    616                GUI.processTasks.addTask(PROCESS_ALL);
    617            } else {
    618                TreePath[] paths = tree.getSelectionPaths();
    619                for (int i=0; i<paths.length; ++i) {
    620                    GUI.processTasks.addTask(((DefaultMutableTreeNode)paths[i].getLastPathComponent()).
    621                                    getUserObject());
    622                }
    623            }
    624        }
    625
    626        static public void escAction(int action) {
    627            if (tree.isSelectionEmpty()) {
    628                GUI.processTasks.addTask(new Integer(action));
    629            } else {
    630                TreePath[] paths = tree.getSelectionPaths();
    631                for (int i=0; i<paths.length; ++i) {
    632                    Object o = ((DefaultMutableTreeNode)paths[i].
    633                                    getLastPathComponent()).
    634                                    getUserObject();
    635                    GUI.EscTreeValue v = (GUI.EscTreeValue)o;
    636                    v.action = action;
    637                    GUI.processTasks.addTask(v);
    638                }
    639            }
    640        }
    641
    642
    643
    644        static private class EscRenderer extends DefaultTreeCellRenderer {
    645        //@ also
    646        //@   requires value != null;
    647            public Component getTreeCellRendererComponent(
    648                            JTree tree,
    649                            Object value,
    650                            boolean sel,
    651                            boolean expanded,
    652                            boolean leaf,
    653                            int row,
    654                            boolean hasFocus) {
    655
    656                super.getTreeCellRendererComponent(
    657                                tree, value, sel,
    658                                expanded, leaf, row,
    659                                hasFocus);
    660                Object userValue = ((DefaultMutableTreeNode)value).getUserObject();
    661                if (userValue instanceof GUI.EscTreeValue) {
    662                    GUI.EscTreeValue u = (GUI.EscTreeValue)userValue;
    663                    Color c = Status.toColor(u.status);
    664                    Color cc = c == null ? new Color(200,200,255) :
    665                                    new Color((c.getRed()+510)/3,(c.getGreen()+510)/3,
    666                                            (c.getBlue()+510)/3);
    667                    if (c == null) c = Color.WHITE;
    668
    669                    setBackgroundNonSelectionColor(c);
    670                    setBackgroundSelectionColor(cc);
    671                    setToolTipText(u.getStatusText());
    672                }
    673
    674                return this;
    675            }
    676        }
    677
    678        private String cachedText = null;
    679        public boolean saveTextArea() {
    680            String s = listArea.getText();
    681            if (s.equals(cachedText)) return false;
    682            cachedText = s;
    683            ArrayList opts = GUI.options().inputEntries;
    684            opts.clear();
    685            BufferedReader r = new BufferedReader(new StringReader(s));
    686            try {
    687                while ((s = r.readLine()) != null) {
    688                    String type = null;
    689                    if (s.startsWith("-")) {
    690                        int p = s.indexOf(' ');
    691                        if (p != -1) {
    692                            type = s.substring(1,p);
    693                            s = s.substring(p+1);
    694                        }
    695                    }
    696                    s = s.trim();
    697                    if (s.length() == 0) continue;
    698                    if (s.charAt(0) == '"' && s.charAt(s.length()-1) == '"')
    699                        s = s.substring(1,s.length()-1);
    700                    InputEntry ie = (InputEntry.make(type,s));
    701                    if (ie != null) opts.add(ie);
    702                    else if (type != null) {
    703                        JOptionPane.showMessageDialog(this,
    704                            "An invalid type in the list of inputs: "
    705                            + type);
    706                    }
    707                }
    708            } catch (java.io.IOException e) {
    709                // Not quite sure why this could ever happen, since we are
    710                // simply reading from a StringReader, but we'll pop a dialog
    711                // just in case.
    712                JOptionPane.showMessageDialog(this,
    713                    "An error happened interpreting the list of input sources: "
    714                    + e);
    715            }
    716            return true;
    717        }
    718
    719        public void loadTextArea() {
    720            listArea.setText("");
    721            Iterator ii = GUI.options().inputEntries.iterator();
    722            while (ii.hasNext()) {
    723                InputEntry s = (InputEntry)ii.next();
    724                if (!s.auto) {
    725                    listArea.append("-" + s.typeOption() + " ");
    726                }
    727                boolean q = s.name.indexOf(' ') != -1;
    728                if (q) listArea.append("\"");
    729                listArea.append(s.name);
    730                if (q) listArea.append("\"");
    731                listArea.append(Project.eol);
    732            }
    733        }
    734
    735
    736        static final /*@non_null*/ Object PROCESS_ALL = new Object();
    737
    738        public void updateSizeInfo() {
    739            Runtime rt = Runtime.getRuntime();
    740            long memUsedBytes = rt.totalMemory() - rt.freeMemory();
    741            sizeinfo.setText(memUsedBytes + " bytes");
    742        }
    743
    744        public void showGuiLight(int i) {
    745            guilight.setBackground( i==0 ? Color.BLUE : i == 1 ? Color.YELLOW : Color.GREEN);
    746        }
    747        public void showProverLight(int i) {
    748            proverlight.setBackground(i == 0? Color.BLACK : i == 2? Color.GREEN : Color.BLUE);
    749        }
    750
    751        public class EscTreeCellRenderer extends JPanel implements TreeCellRenderer {
    752            /*@non_null*/ JLabel label;
    753            /*@non_null*/ JCheckBox cb;
    754
    755            public EscTreeCellRenderer() {
    756                setLayout(new BoxLayout(this,BoxLayout.LINE_AXIS));
    757                add(label = new JLabel());
    758                add(Box.createHorizontalGlue());
    759                add(cb = new JCheckBox("",true));
    760            }
    761
    762            public void setText(String s) {
    763                label.setText(s);
    764            }
    765
    766            public boolean isShowing() { return true; }
    767
    768            public /*@non_null*/ Component getTreeCellRendererComponent(JTree tree,
    769                                                  Object value,
    770                                                  boolean selected,
    771                                                  boolean expanded,
    772                                                  boolean leaf,
    773                                                  int row,
    774                                                  boolean hasFocus) {
    775
    776                if (value instanceof DefaultMutableTreeNode) {
    777                    Object o = ((DefaultMutableTreeNode)value).getUserObject();
    778                    if (o instanceof GUI.EscTreeValue) {
    779                        GUI.EscTreeValue u = (GUI.EscTreeValue)o;
    780                        Color c = Status.toColor(u.status);
    781                        Color cc = c == null ? new Color(200,200,255) :
    782                                        new Color((c.getRed()+510)/3,(c.getGreen()+510)/3,
    783                                                (c.getBlue()+510)/3);
    784                        if (c == null) c = Color.WHITE;
    785
    786                        setBackground(selected ? cc : c);
    787                        setToolTipText(u.getStatusText());
    788                        setText(u.toString());
    789                        //Dimension d1 = getMinimumSize();
    790                        Dimension d2 = getPreferredSize();
    791                        //Dimension d3 = getMaximumSize();
    792    //System.out.println("DIM " + d1.width + " " + d1.height + " " + d2.width + " " + d2.height + " " + d3.width + " " + d3.height);
    793                        int w = treeView.getViewport().getWidth();
    794    //System.out.println("SZ " + w);
    795                        if (w == 0) w = 500;
    796    //System.out.println("LOC " + getX() + " " + getY());
    797                        setPreferredSize(new Dimension(w - 100,d2.height));
    798    //                  CellRendererPane cp = (CellRendererPane)getParent();
    799    //                  if (cp != null) cp.setSize(600,d2.height);
    800    //if (cp != null) System.out.println("PAR " + cp.getPreferredSize().width + " " + cp.getPreferredSize().height + " " + cp.getMaximumSize().width + " " + cp.getMaximumSize().height + " " + cp.getX() + " " + cp.getY());
    801                    }
    802                }
    803                return this;
    804
    805            }
    806
    807
    808        }
    809
    810    /*
    811    Still puts up the Java about box.
    812    Need to make a nicer about box - and not a modal one.
    813    Also make this cross platform.
    814
    815        static About about = new About();
    816
    817        static public class About extends Application {
    818
    819            public About() {
    820                addApplicationListener(new AboutH());
    821            }
    822
    823        }
    824        static public class AboutH extends ApplicationAdapter {
    825
    826            public void handleAbout(ApplicationEvent e) {
    827                JOptionPane.showMessageDialog(GUI.gui.escframe,"ABOUT");
    828            }
    829            public void handleQuit(ApplicationEvent e) {
    830                System.exit(0);
    831            }
    832        }
    833    */
    834    }