src/Tools/jEdit/src/syslog_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 57612 990ffb84489b
child 66591 6efa351190d0
permissions -rw-r--r--
tuned signature;
wenzelm@48021
     1
/*  Title:      Tools/jEdit/src/syslog_dockable.scala
wenzelm@48021
     2
    Author:     Makarius
wenzelm@48021
     3
wenzelm@48021
     4
Dockable window for syslog.
wenzelm@48021
     5
*/
wenzelm@48021
     6
wenzelm@48021
     7
package isabelle.jedit
wenzelm@48021
     8
wenzelm@48021
     9
wenzelm@48021
    10
import isabelle._
wenzelm@48021
    11
wenzelm@56775
    12
import scala.swing.{TextArea, ScrollPane}
wenzelm@48021
    13
wenzelm@48021
    14
import org.gjt.sp.jedit.View
wenzelm@48021
    15
wenzelm@48021
    16
wenzelm@49559
    17
class Syslog_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@48021
    18
{
wenzelm@48021
    19
  /* GUI components */
wenzelm@48021
    20
wenzelm@48021
    21
  private val syslog = new TextArea()
wenzelm@48021
    22
wenzelm@57612
    23
  private def syslog_delay = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
wenzelm@48021
    24
  {
wenzelm@56775
    25
    val text = PIDE.session.syslog_content()
wenzelm@53177
    26
    if (text != syslog.text) syslog.text = text
wenzelm@48021
    27
  }
wenzelm@48021
    28
wenzelm@56775
    29
  set_content(new ScrollPane(syslog))
wenzelm@48021
    30
wenzelm@48021
    31
wenzelm@56715
    32
  /* main */
wenzelm@48021
    33
wenzelm@56715
    34
  private val main =
wenzelm@56775
    35
    Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() }
wenzelm@48021
    36
wenzelm@48021
    37
  override def init()
wenzelm@48021
    38
  {
wenzelm@56715
    39
    PIDE.session.syslog_messages += main
wenzelm@56775
    40
    syslog_delay.invoke()
wenzelm@48021
    41
  }
wenzelm@48021
    42
wenzelm@48021
    43
  override def exit()
wenzelm@48021
    44
  {
wenzelm@56715
    45
    PIDE.session.syslog_messages -= main
wenzelm@48021
    46
  }
wenzelm@48021
    47
}