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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/ActionEvent e) { escAction(GUI.CLEAR); } });
191
192 button = new JButton("Check");
193 button.addActionListener(new ActionListener() {
194 public void actionPerformed(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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(/*@non_null*/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 }