Method setDocument

src/main/java/gate/gui/LogArea.java:349–354

Overridden to fetch new start and end Positions when the document is changed.

(Document d)

   * changed.
   */
  @Override
  public void setDocument(Document d) {
    super.setDocument(d);
    startPos = d.getStartPosition();
    endPos = d.getEndPosition();
  }

  @Override
  public void setStyledDocument(StyledDocument d) {