Method scroll

basex-core/src/main/java/org/basex/gui/text/TextPanel.java:669–677

Scrolls to the specified position. @param y new vertical position @param align alignment (0: scroll up, 1: jump, 2: scroll down)

(final int y, final int align)

   * @param align alignment (0: scroll up, 1: jump, 2: scroll down)
   */
  private void scroll(final int y, final int align) {
    if(y != -1) {
      final int h = getHeight(), m = y + (rend.fontHeight() << 1) - h, p = scroll.pos();
      if(p < m || p > y) {
        scroll.pos(align == 0 ? y : align == 1 ? y - h / 2 : m);
      }
    }
    rend.repaint();
  }

  /** Last horizontal position. */
  private int lastCol = -1;