src/Tools/jEdit/src/syslog_dockable.scala
author wenzelm
Sat Aug 24 13:32:51 2013 +0200 (2013-08-24)
changeset 53177 dcac8d837b9c
parent 50205 788c8263e634
child 55618 995162143ef4
permissions -rw-r--r--
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
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.actors.Actor._
wenzelm@48021
    13
import scala.swing.TextArea
wenzelm@48021
    14
wenzelm@48021
    15
import org.gjt.sp.jedit.View
wenzelm@48021
    16
wenzelm@48021
    17
wenzelm@49559
    18
class Syslog_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@48021
    19
{
wenzelm@48021
    20
  /* GUI components */
wenzelm@48021
    21
wenzelm@48021
    22
  private val syslog = new TextArea()
wenzelm@48021
    23
wenzelm@48021
    24
  private def update_syslog()
wenzelm@48021
    25
  {
wenzelm@53177
    26
    Swing_Thread.require()
wenzelm@53177
    27
wenzelm@53177
    28
    val text = PIDE.session.current_syslog()
wenzelm@53177
    29
    if (text != syslog.text) syslog.text = text
wenzelm@48021
    30
  }
wenzelm@48021
    31
wenzelm@48021
    32
  set_content(syslog)
wenzelm@48021
    33
wenzelm@48021
    34
wenzelm@48021
    35
  /* main actor */
wenzelm@48021
    36
wenzelm@48021
    37
  private val main_actor = actor {
wenzelm@48021
    38
    loop {
wenzelm@48021
    39
      react {
wenzelm@48021
    40
        case output: Isabelle_Process.Output =>
wenzelm@53177
    41
          if (output.is_syslog) Swing_Thread.later { update_syslog() }
wenzelm@48021
    42
wenzelm@49559
    43
        case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
wenzelm@48021
    44
      }
wenzelm@48021
    45
    }
wenzelm@48021
    46
  }
wenzelm@48021
    47
wenzelm@48021
    48
  override def init()
wenzelm@48021
    49
  {
wenzelm@50205
    50
    PIDE.session.syslog_messages += main_actor
wenzelm@48021
    51
    update_syslog()
wenzelm@48021
    52
  }
wenzelm@48021
    53
wenzelm@48021
    54
  override def exit()
wenzelm@48021
    55
  {
wenzelm@50205
    56
    PIDE.session.syslog_messages -= main_actor
wenzelm@48021
    57
  }
wenzelm@48021
    58
}