Inspector.java

00001 /*
00002  *  Main authors:
00003  *     Mikael Lagerkvist <lagerkvist@gecode.org>
00004  *     Guido Tack <tack@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Mikael Lagerkvist, 2006
00008  *     Guido Tack, 2006
00009  *
00010  *  Last modified:
00011  *     $Date: 2006-02-23 11:30:04 +0100 (Thu, 23 Feb 2006) $ by $Author: zayenz $
00012  *     $Revision: 3016 $
00013  *
00014  *  This file is part of Gecode, the generic constraint
00015  *  development environment:
00016  *     http://www.gecode.org
00017  *
00018  *  See the file "LICENSE" for information on usage and
00019  *  redistribution of this file, and for a
00020  *     DISCLAIMER OF ALL WARRANTIES.
00021  *
00022  */
00023 
00024 package org.gecode.explorer.swing;
00025 
00026 import javax.swing.*;
00027 import java.awt.*;
00028 import java.awt.event.*;
00029 import java.awt.BorderLayout;
00030 
00031 class Inspector implements WindowListener, ActionListener {
00032 
00033     JFrame frame;
00034     JEditorPane textArea;
00035     JButton clearButton, plusSize, minusSize;
00036     String text = "";
00037     int size = 14;
00038     static int minSize = 3, maxSize = 26;
00039 
00040     Inspector(String s) {
00041         text = "<pre>"+s+"</pre>";
00042         init();
00043     }
00044 
00045     void init() {
00046         frame = new JFrame("Gecode inspector");
00047         frame.getContentPane().setLayout(new BorderLayout());
00048         frame.setIconImage(new ImageIcon(TreeCanvas.gecodeLogo).getImage());
00049 
00050         textArea = new JEditorPane("text/html", addFont(text));
00051         textArea.setEditable(false);
00052         JScrollPane scrollPane = new JScrollPane( textArea );
00053         frame.getContentPane().add(scrollPane, BorderLayout.CENTER);
00054 
00055         // Construct toolbar
00056         JToolBar toolbar = new JToolBar();
00057 
00058 
00059         toolbar.setFloatable(false);
00060         clearButton = new JButton("Clear");
00061         clearButton.addActionListener(this);
00062         toolbar.add(clearButton);
00063         toolbar.addSeparator();
00064         toolbar.add(new JLabel("Font Size: "));
00065         plusSize = new JButton("+");
00066         plusSize.addActionListener(this);
00067         toolbar.add(plusSize);
00068         minusSize = new JButton("-");
00069         minusSize.addActionListener(this);
00070         toolbar.add(minusSize);
00071         frame.getContentPane().add(toolbar, BorderLayout.SOUTH);
00072 
00073         frame.addWindowListener(this);
00074 
00075         frame.pack();
00076         frame.setVisible(true);
00077     }
00078 
00079     void addText(String s) {
00080         if (! text.equals("")) text += "\n<div><hr></div>";
00081         text += "<pre>"+s+"</pre>";
00082         if (frame == null) {
00083             init();
00084         } else {
00085             textArea.setText(addFont(text));
00086         }
00087         frame.setVisible(true);
00088     }
00089 
00090     String addFont(String t) {
00091         return "<HEAD><STYLE type=\"text/css\"> pre {font-size:" + size +
00092           "}</STYLE></HEAD><BODY>" + t + "</BODY>";
00093     }
00094     
00095     // WindowListener interface
00096 
00097     public void windowOpened(WindowEvent e) {}
00098     public void windowClosing(WindowEvent e) {
00099         frame.dispose();
00100         frame = null;
00101     }
00102     public void windowClosed(WindowEvent e) {}
00103     public void windowIconified(WindowEvent e) {}
00104     public void windowDeiconified(WindowEvent e) {}
00105     public void windowActivated(WindowEvent e) {}
00106     public void windowDeactivated(WindowEvent e) {}
00107 
00108     // ActionListener interface
00109     public void actionPerformed(ActionEvent e) {
00110         if (e.getSource() == clearButton) {
00111           text = "";
00112             textArea.setText(text);
00113         }
00114         if (e.getSource() == plusSize) {
00115           ++size;
00116           if (size == maxSize) plusSize.setEnabled(false);
00117           minusSize.setEnabled(true);
00118           textArea.setText(addFont(text));
00119         }
00120         if (e.getSource() == minusSize) {
00121           --size;
00122           if (size == minSize) minusSize.setEnabled(false);
00123           plusSize.setEnabled(true);
00124           textArea.setText(addFont(text));
00125         }
00126     }
00127 
00128 }