src/Tools/jEdit/src/syslog_dockable.scala
author wenzelm
Fri, 15 Nov 2024 13:31:36 +0100
changeset 81448 9b2e13b3ee43
parent 76610 6e2383488a55
permissions -rw-r--r--
more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);

/*  Title:      Tools/jEdit/src/syslog_dockable.scala
    Author:     Makarius

Dockable window for syslog.
*/

package isabelle.jedit


import isabelle._

import scala.swing.{TextArea, ScrollPane}

import org.gjt.sp.jedit.View


class Syslog_Dockable(view: View, position: String) extends Dockable(view, position) {
  /* GUI components */

  private val syslog = new TextArea()

  private def syslog_delay =
    Delay.first(PIDE.session.update_delay, gui = true) {
      val text = PIDE.session.syslog.content()
      if (text != syslog.text) syslog.text = text
    }

  set_content(new ScrollPane(syslog))


  /* main */

  private val main =
    Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() }

  override def init(): Unit = {
    PIDE.session.syslog_messages += main
    syslog_delay.invoke()
  }

  override def exit(): Unit = {
    PIDE.session.syslog_messages -= main
  }
}