src/Tools/jEdit/src/syslog_dockable.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73987 fc363a3b690a
child 76488 1eed7e1300ed
permissions -rw-r--r--
clarified formatting, for the sake of scala3;

/*  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.options.seconds("editor_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
  }
}