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    }