Hi Gilad,


I've run into a bizarre and annoying bug in Java Swing, and so far
failed to find a workaround. Following is a program that demonstrates
the bug. I'd be grateful if you could pass this on to someone
appropriate, or let me know who I should contact. Many thanks, -- P


-----------------------------------------------------------------------
Philip Wadler ###@###.###
Bell Labs, Lucent Technologies http://www.cs.bell-labs.com/~wadler
600 Mountain Ave, room 2T-402 office: +1 908 582 4004
Murray Hill, NJ 07974-0636 fax: +1 908 582 5857
USA home: +1 908 626 9252
-----------------------------------------------------------------------


/*


Scroll Bug
Philip Wadler, 8 April 98


This program demonstrates a bug in scrolling with JDK 1.2.1 Swing. It
displays a JList on the left, and a stack of JTextArea on the right.
Clicking an entry in the JList selects the corresponding JTextArea,
and should scroll it to be visible. However, sometimes it exhibits
bizarre behavior: it scrolls to the wrong place, or it scrolls to the
right place and then immediately leaps to some other place.


*/


import java.awt.*;
import java.awt.event.*;
import javax.swing.*;
import javax.swing.event.*;


class ScrollBug {


  protected final int SIZE = 50;


  protected final JSplitPane splitPane;


  protected final JList list;
  protected final JPanel vbox;


  protected final JScrollPane listScroll;
  protected final JScrollPane vboxScroll;


  protected final String[] strings;
  protected final JTextArea[] texts;


  public ScrollBug() {


    strings = new String[SIZE];
    texts = new JTextArea[SIZE];
    for (int i=0; i<SIZE; i++) {
      strings[i] = "list "+i;
      JTextArea text = new JTextArea();
      text.setText("text "+i);
      texts[i] = text;
    }


    list = new JList(strings);
    list.addListSelectionListener(new ListSelectionListener() {
      public void valueChanged(ListSelectionEvent e) {
        if (e.getValueIsAdjusting()) return;
        int i = list.getSelectedIndex();
        JTextArea text = texts[i];
        Rectangle r = text.getBounds();
        System.out.println("select: "+i+", scroll to: "+r);
        text.selectAll();
        text.scrollRectToVisible(r);
      }
    });


    vbox = new JPanel();
    vbox.setLayout(new BoxLayout(vbox, BoxLayout.Y_AXIS));
    for (int i=0; i<SIZE; i++) { vbox.add(texts[i]); }


    listScroll = new JScrollPane(list);
    vboxScroll = new JScrollPane(vbox);
    // listScroll.setMinimumSize(new Dimension(100, 100));
    // vboxScroll.setMinimumSize(new Dimension(100, 100));


    splitPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT);
    splitPane.setLeftComponent(listScroll);
    splitPane.setRightComponent(vboxScroll);
    splitPane.setPreferredSize(new Dimension(250, 250));
    splitPane.setDividerLocation(120);
  }


  public void scrollVisible (JComponent c) {
  }


  // ListSelectionListener
  // main
  public static void main(String s[]) {


    ScrollBug scrollbug = new ScrollBug();


    JFrame frame = new JFrame();
    frame.addWindowListener(new WindowAdapter() {
      public void windowClosing(WindowEvent e) {System.exit(0);}
    });
    frame.getContentPane().add(scrollbug.splitPane);
    frame.pack();
    frame.setVisible(true);
  }


}