code: package wprover;
  
  import gprover.*;
  
  import javax.swing.*;
  import javax.swing.tree.DefaultTreeCellRenderer;
  import javax.swing.tree.TreeCellRenderer;
  import javax.swing.tree.DefaultMutableTreeNode;
  import javax.swing.tree.TreeCellEditor;
  import javax.swing.border.Border;
  import javax.swing.border.LineBorder;
  import java.awt.event.MouseMotionListener;
  import java.awt.event.MouseListener;
  import java.awt.event.MouseEvent;
  import java.awt.event.ActionListener;
  import java.awt.*;
  import java.util.Vector;
  import java.util.EventObject;
  
  /**
   * Created by IntelliJ IDEA.
   * User: yezheng
   * Date: 2006-5-23
   * Time: 13:50:22
   * To change this template use File | Settings | File Templates.
   */
  class vcellRender extends JPanel {
      protected static Border eborder = BorderFactory.createEmptyBorder(1, 1, 1, 1);
      protected static Border gborder = BorderFactory.createLineBorder(Color.GRAY, 1);
  
      protected static DefaultTreeCellRenderer defaultRenderer = new DefaultTreeCellRenderer();
      boolean selected;
      Color backgroundSelectionColor;
      Color backgroundNonSelectionColor;
  
      public vcellRender() {
          this.setBorder(eborder);
          this.setLayout(new BoxLayout(this, BoxLayout.X_AXIS));
          selected = false;
          defaultRenderer.setFont(itemLabel.font1);
          backgroundSelectionColor = defaultRenderer.getBackgroundSelectionColor();
          backgroundNonSelectionColor = defaultRenderer.
                  getBackgroundNonSelectionColor();
      }
  
  
      public void paintComponent(Graphics g) {
          if (selected) {
              g.setColor(backgroundSelectionColor.darker());
              g.drawRect(0, 0, this.getWidth() - 1, this.getHeight() - 1);
          }
          super.paintComponent(g);
      }
  }
                       
  
  class BookCellRenderer extends vcellRender implements TreeCellRenderer {
      Vector renderlist = new Vector();
      Vector renderlist1 = new Vector();
  
      public BookCellRenderer(int n) {
          super();
          for (int i = 1; i <= n; i++) {
              itemLabel lb = new itemLabel(true, false);
              renderlist.add(lb);
          }
          for (int i = 1; i <= n; i++) {
              itemLabel lb = new itemLabel(true, true);
              renderlist1.add(lb);
          }
      }
  
      public void setCellFont(Font f) {
          for (int i = 0; i < renderlist.size(); i++) {
              itemLabel lb = (itemLabel) renderlist.get(i);
              lb.setFont(f);
          }
          Font f1 = new Font(f.getFamily(), f.getStyle(), f.getSize() - 1);
          for (int i = 0; i < renderlist1.size(); i++) {
              itemLabel lb = (itemLabel) renderlist1.get(i);
              lb.setFont(f1);
          }
      }
  
      public void setLabelObject(int index, int t, Object obj) {
          if (obj == null) return;
  
          itemLabel label = null;
          label = (itemLabel) renderlist.get(index);
          label.setUserObject(t, obj);
          this.add(label);
      }
  
      public void setLabelObject1(int index, int t, Object obj) {
          itemLabel label = null;
          label = (itemLabel) renderlist1.get(index);
          label.setUserObject(t, obj);
          this.add(label);
      }
  
      public Component getTreeCellRendererComponent(JTree tree, Object value,
                                                    boolean selected,
                                                    boolean expanded,
                                                    boolean leaf, int row,
                                                    boolean hasFocus) {
          Component returnValue = null;
  
          boolean crsp = false;
  
          if ((value != null) && (value instanceof DefaultMutableTreeNode)) {
  
              DefaultMutableTreeNode node = (DefaultMutableTreeNode) value;
              this.removeAll();
              Object userObject = ((DefaultMutableTreeNode) value).getUserObject();
              vcellRender cell = this;
  
              if (userObject instanceof gr_term) {
                  gr_term gr = (gr_term) userObject;
                  Vector v = gr.getAllxterm();
                  int index = v.size();
                  int k = 0;
                  if (index >= 0) {
                      if (row != 1) {
                          setLabelObject(0, 0, " = ");
                      } else {
                          setLabelObject(0, 0, "    ");
                      }
                      k++;
                      for (int i = 0; i < v.size(); i++) {
                          xterm x = (xterm) v.get(i);
                          setLabelObject(k++, 1, x);
                      }
                  }
                  if (gr.getPTN() == 0) {
                      setLabelObject(k++, 2, gr.el);
                  }
                  if (v.size() == 1) {
                      xterm x = (xterm) v.get(0);
                      if (x.getPV() == 0)
                          setLabelObject(k++, 0, "   Q.E.D. ");
                  }
              } else if (userObject instanceof el_term) {
                  el_term el = (el_term) userObject;
                  Vector v = el.getAllxterm();
                  int k = 0;
                  if (node.getParent() != null) {
                      setLabelObject1(k++, 0, "because");
                  }
                  setLabelObject1(k++, 1, v.get(0));
                  setLabelObject1(k++, 0, " = ");
                  for (int i = 1; i < v.size(); i++) {
                      setLabelObject1(k++, 1, v.get(i));
                  }
                  if (el.getEType() > 0)
                      setLabelObject1(k++, 2, el);
                  if (selected) {
                      setLabelObject1(k++, 5, el);
                  }
              } else if (userObject instanceof dterm) {
              } else if (userObject instanceof cond) {
                  cond c = (cond) userObject;
                  int k = 0;
                  int nt = c.getNo();
                  if (nt != 0 && nt == BookCellEditor.cond_no)
                      crsp = true;
  
                  if (c.getNo() != 0) {
                      setLabelObject(k++, 0, c.getNo() + ". ");
                  }
                  setLabelObject1(k++, 4, userObject);
                  if (c.getNo() != 0 && node.getChildCount() != 0 && c.getRule() > 0) {
                      setLabelObject1(k++, 2, c);
                  } else if (node.getChildCount() == 0) {
                      int n = c.get_conc_type();
                      if (n != 0) {
                          setLabelObject1(k++, 0, "   (by HYP)");
                      } else if (c.getNo() == 0) {
                          setLabelObject1(k++, 0, "   (in GIB)");
                      }
  
                  }
              } else if (userObject instanceof l_list) {
                  l_list ls = (l_list) userObject;
                  setLabelObject(0, 7, ls);
              } else if (userObject instanceof rule) {
                  rule ls = (rule) userObject;
                  setLabelObject(0, 7, ls);
              } else {
                  //cell = null;
                  setLabelObject(0, 9999, userObject);
              }
  
              if (cell != null) {
                  if (selected || crsp) {
                      cell.setBackground(cell.backgroundSelectionColor);
                  } else {
                      cell.setBackground(cell.backgroundNonSelectionColor);
                  }
                  cell.setEnabled(tree.isEnabled());
                  returnValue = cell;
              }
          }
          if (returnValue == null) {
              returnValue = vcellRender.defaultRenderer.
                      getTreeCellRendererComponent(tree, value, selected, expanded, leaf, row, hasFocus);
          }
          return returnValue;
      }
  
   
  }
  
  
  class BookCellEditor extends BasicCellEditor implements MouseListener {
  
      public BookCellEditor(int n) {
          init(n);
  
          for (int i = 0; i < renderlist.size(); i++) {
              itemLabel lb = (itemLabel) renderlist.get(i);
              lb.addMouseListener(this);
          }
          for (int i = 0; i < renderlist1.size(); i++) {
              itemLabel lb = (itemLabel) renderlist1.get(i);
              lb.addMouseListener(this);
          }
      }
  
      public void mouseClicked(MouseEvent e) {
      }
  
      public void mousePressed(MouseEvent e) {
          if (selectLabel != null) {
              selectLabel.setSelected(false);
          }
          selectLabel = (itemLabel) e.getSource();
          selectLabel.setSelected(true);
          cell.repaint();
      }
  
      public void mouseReleased(MouseEvent e) {
      }
  
      public void mouseEntered(MouseEvent e) {
      }
  
      public void mouseExited(MouseEvent e) {
      }
  
  }
  
                   
  class BasicCellEditor extends AbstractCellEditor implements TreeCellEditor {
      public static int cond_no = 0;
  
      Vector renderlist = new Vector();
      Vector renderlist1 = new Vector();
      vcellRender cell = new vcellRender();
      itemLabel selectLabel = null;
  
  
      public void init(int n) {
  
          for (int i = 1; i <= n; i++) {
              itemLabel lb = new itemLabel(false, false);
              lb.setRenderT(false);
  
              renderlist.add(lb);
          }
          for (int i = 1; i <= n; i++) {
              itemLabel lb = new itemLabel(false, true);
              lb.setRenderT(false);
              lb.setFont(itemLabel.font1);
              renderlist1.add(lb);
          }
          cell.setBorder(new LineBorder(cell.backgroundSelectionColor.darker(), 1));
      }
  
      public void setEditorFont(Font f) {
          for (int i = 0; i < renderlist.size(); i++) {
              itemLabel lb = (itemLabel) renderlist.get(i);
              lb.setFont(f);
          }
          Font f1 = new Font(f.getFamily(), f.getStyle(), f.getSize() - 1);
          for (int i = 0; i < renderlist1.size(); i++) {
              itemLabel lb = (itemLabel) renderlist1.get(i);
              lb.setFont(f1);
          }
      }
  
      public void setLabelObject(int index, int t, Object obj) {
          itemLabel label = null;
          label = (itemLabel) renderlist.get(index);
          label.setUserObject(t, obj);
          cell.add(label);
      }
  
      public void setLabelObject1(int index, int t, Object obj) {
          itemLabel label = null;
          label = (itemLabel) renderlist1.get(index);
          label.setUserObject(t, obj);
          cell.add(label);
      }
  
      public void addListenerToAllLabel(MouseListener listener) {
          for (int i = 0; i < renderlist.size(); i++) {
              itemLabel label = (itemLabel) renderlist.get(i);
              label.addMouseListener(listener);
          }
          for (int i = 0; i < renderlist1.size(); i++) {
              itemLabel label = (itemLabel) renderlist1.get(i);
              label.addMouseListener(listener);
          }
      }
  
      public Component getTreeCellEditorComponent(JTree tree, Object value,
                                                  boolean isSelected,
                                                  boolean expanded,
                                                  boolean leaf, int row) {
          Component returnValue = null;
          cond_no = 0;
          if ((value != null) && (value instanceof DefaultMutableTreeNode)) {
              DefaultMutableTreeNode node = (DefaultMutableTreeNode) value;
              cell.removeAll();
              cell.revalidate();
              Object userObject = ((DefaultMutableTreeNode) value).getUserObject();
              vcellRender cell = this.cell;
  
              if (userObject instanceof gr_term) {
                  gr_term gr = (gr_term) userObject;
                  Vector v = gr.getAllxterm();
                  int index = v.size();
                  int k = 0;
                  if (index >= 0) {
                      if (row != 1) {
                          setLabelObject(0, 0, " = ");
                      } else {
                          setLabelObject(0, 0, "    ");
                      }
                      k++;
                      for (int i = 0; i < v.size(); i++) {
                          xterm x = (xterm) v.get(i);
                          setLabelObject(k++, 1, x);
                      }
                  }
                  if (gr.getPTN() == 0) {
                      el_term e = gr.el;
                      if (e.getEType() > 0) {
                          setLabelObject(k++, 2, gr.el);
                          setLabelObject1(k++, 5, gr.el);
                      }
                  }
                  if (v.size() == 1) {
                      xterm x = (xterm) v.get(0);
                      if (x.getPV() == 0)
                          setLabelObject(k++, 0, "   Q.E.D. ");
                  }
              } else if (userObject instanceof el_term) {
                  el_term el = (el_term) userObject;
                  Vector v = el.getAllxterm();
                  int k = 0;
                  if (node.getParent() != null) {
                      setLabelObject1(k++, 0, "because");
                  }
                  setLabelObject1(k++, 1, v.get(0));
                  setLabelObject1(k++, 0, " = ");
                  for (int i = 1; i < v.size(); i++) {
                      setLabelObject1(k++, 1, v.get(i));
                  }
                  if (el.getEType() > 0)
                      setLabelObject1(k++, 2, el);
                  setLabelObject1(k++, 5, el);
  //                if (node.getParent() != null)
  //                    setLabelObject1(k++, 0, " )");
              } else if (userObject instanceof dterm) {
              } else if (userObject instanceof cond) {
                  cond c = (cond) userObject;
                  int k = 0;
                  cond_no = c.getNo();
                  if (c.getNo() != 0) {
                      setLabelObject(k++, 0, c.getNo() + ". ");
                  }
                  setLabelObject1(k++, 4, userObject);
                  if (c.getNo() != 0 && node.getChildCount() != 0 &&
                          c.getRule() >= 0) {
                      if (c.getRule() > 0) {
                          setLabelObject1(k++, 2, c);
                      }
                      setLabelObject1(k++, 5, c);
                  } else if (node.getChildCount() == 0) {
                      int n = c.get_conc_type();
                      if (n != 0) {
                          setLabelObject1(k++, 0, "   (by HYP)");
                      } else if (c.getNo() == 0) {
                          setLabelObject1(k++, 0, "   (in GIB)");
                      }
                  }
              } else {
                  //cell = null;
                  setLabelObject(0, 9999, userObject);
              }
  
              if (cell != null) {
                  cell.setBackground(cell.backgroundSelectionColor);
                  cell.setEnabled(tree.isEnabled());
                  returnValue = cell;
              }
          }
          if (returnValue == null) {
              returnValue = vcellRender.defaultRenderer.
                      getTreeCellRendererComponent(tree,
                              value, isSelected, expanded, leaf, row, true);
          }
          return returnValue;
  
      }
  
  
      public void cancelCellEditing() {
          super.cancelCellEditing();
          cond_no = 0;
      }
  
      public Object getCellEditorValue() {
          return null;
      }
  }
  
  
  class itemLabel extends JLabel {
      public static ImageIcon icon = GExpert.createImageIcon("images/dtree/detail.gif");
      private static ImageIcon icon_bc = GExpert.createImageIcon("images/dtree/because.gif");
  
  
      public static Font font = CMisc.fullFont;
      public static Font font1 = new Font(font.getName(), font.getStyle(), font.getSize() - 1);
      public GExpert gxInstance;
  
  
      boolean isrender = true;
      boolean mouse_inside = false;
      protected boolean iselm = false;
      int type; // 0.Normal text 1. xterm 2.rule.3.el_term,4:cond  , 5: icon.
      private Object userValue;
  
      boolean selected = false;
  
      public int getType() {
          return type;
      }
  
  
      public static int getItemLabelFontSize() {
          return font.getSize();
      }
  
      public Object getUserObject() {
          return userValue;
      }
  
      public itemLabel(boolean r, boolean e) {
          super();
          isrender = r;
          iselm = e;
          if (e) {
              this.setFont(font1);
          } else {
              this.setFont(font);
              this.setForeground(Color.black);
          }
  
          this.addMouseListener(new MouseListener() {
              public void mouseClicked(MouseEvent e) {
              }
  
              public void mousePressed(MouseEvent e) {
                  selected = true;
              }
  
              public void mouseReleased(MouseEvent e) {
              }
  
              public void mouseEntered(MouseEvent e) {
                  mouse_inside = true;
                  if (type == 5) {
                      setCursor(Cursor.getPredefinedCursor(Cursor.HAND_CURSOR));
                  }
                  itemLabel.this.repaint();
              }
  
              public void mouseExited(MouseEvent e) {
                  mouse_inside = false;
                  if (type == 5) {
                      setCursor(Cursor.getDefaultCursor());
                  }
                  itemLabel.this.repaint();
              }
          });
      }
  
  
      public void setRenderT(boolean r) {
          this.isrender = r;
      }
  
      public void setSelected(boolean s) {
          selected = s;
          if (iselm) {
              {
                  if (s) {
                      this.setForeground(Color.black);
                  } else {
                      this.setForeground(Color.black);
                  }
              }
          }
          this.repaint();
      }
  
      public boolean isSelected() {
          return selected;
      }
  
      public void setUserObject(int type, Object obj) {
          this.type = type;
          userValue = obj;
          if (type == 2) {
              if (obj instanceof el_term) {
                  el_term e = (el_term) obj;
                  if (!iselm) {
                      this.setForeground(Color.black);
                  }
                  if (e.etype != 5) {
                      this.setText("  (rule" + e.etype + ")");
                  } else {
                      this.setText("  (addition)");
                  }
              } else if (obj instanceof cond) {
                  cond c = (cond) obj;
                  if (!iselm) {
                      this.setForeground(Color.black);
                  }
                  int r = c.getRule();
                  setText("  (r" + r + ")");
              }
              this.setIcon(null);
          } else if (type == 5) {
              this.setToolTipText("Click to see the detail ");
              this.setIcon(icon);
              this.setText(null);
          } else if (type == 6) {
              cond c = (cond) obj;
              this.setHorizontalTextPosition(JLabel.LEFT);
              this.setIcon(icon);
              this.setText("   DR" + c.getRule());
          } else {
              String s = obj.toString();
              if (type == 0 && s.trim().equals("because")) {
                  this.setIcon(icon_bc);
                  this.setText(null);
              } else {
                  this.setText(s);
                  this.setIcon(null);
              }
          }
      }
  
      public void paint(Graphics g) {
          if (isrender) {
          } else {
  
              if (type == 5) {
                  if (mouse_inside || selected) {
                      g.setColor(Color.pink.brighter());
                      g.fillRect(0, 0, this.getWidth() - 1, this.getHeight() - 1);
                      g.setColor(Color.pink);
                      g.drawRect(0, 0, this.getWidth() - 1, this.getHeight() - 1);
                  }
              } else if (type != 0) {
                  {
                      if (selected) {
                          g.setColor(Color.pink);
                          g.fillRect(0, 0, this.getWidth() - 1,
                                  this.getHeight() - 1);
                      }
                      if (mouse_inside || selected) {
                          g.setColor(Color.pink.darker());
                          g.drawRect(0, 0, this.getWidth() - 1,
                                  this.getHeight() - 1);
                      }
                  }
              }
          }
          super.paint(g);
      }
  }
  