src/Tools/jEdit/src/syslog_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56775 59f70b89e5fd
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
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@48021
    12
import scala.swing.TextArea
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@48021
    23
  private def update_syslog()
wenzelm@48021
    24
  {
wenzelm@56662
    25
    Swing_Thread.require {}
wenzelm@53177
    26
wenzelm@53177
    27
    val text = PIDE.session.current_syslog()
wenzelm@53177
    28
    if (text != syslog.text) syslog.text = text
wenzelm@48021
    29
  }
wenzelm@48021
    30
wenzelm@48021
    31
  set_content(syslog)
wenzelm@48021
    32
wenzelm@48021
    33
wenzelm@56715
    34
  /* main */
wenzelm@48021
    35
wenzelm@56715
    36
  private val main =
wenzelm@56715
    37
    Session.Consumer[Prover.Output](getClass.getName) {
wenzelm@56715
    38
      case output =>
wenzelm@56715
    39
        if (output.is_syslog) Swing_Thread.later { update_syslog() }
wenzelm@48021
    40
    }
wenzelm@48021
    41
wenzelm@48021
    42
  override def init()
wenzelm@48021
    43
  {
wenzelm@56715
    44
    PIDE.session.syslog_messages += main
wenzelm@48021
    45
    update_syslog()
wenzelm@48021
    46
  }
wenzelm@48021
    47
wenzelm@48021
    48
  override def exit()
wenzelm@48021
    49
  {
wenzelm@56715
    50
    PIDE.session.syslog_messages -= main
wenzelm@48021
    51
  }
wenzelm@48021
    52
}