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;
     1 /*  Title:      Tools/jEdit/src/syslog_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for syslog.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.actors.Actor._
    13 import scala.swing.TextArea
    14 
    15 import org.gjt.sp.jedit.View
    16 
    17 
    18 class Syslog_Dockable(view: View, position: String) extends Dockable(view, position)
    19 {
    20   /* GUI components */
    21 
    22   private val syslog = new TextArea()
    23 
    24   private def update_syslog()
    25   {
    26     Swing_Thread.require()
    27 
    28     val text = PIDE.session.current_syslog()
    29     if (text != syslog.text) syslog.text = text
    30   }
    31 
    32   set_content(syslog)
    33 
    34 
    35   /* main actor */
    36 
    37   private val main_actor = actor {
    38     loop {
    39       react {
    40         case output: Isabelle_Process.Output =>
    41           if (output.is_syslog) Swing_Thread.later { update_syslog() }
    42 
    43         case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
    44       }
    45     }
    46   }
    47 
    48   override def init()
    49   {
    50     PIDE.session.syslog_messages += main_actor
    51     update_syslog()
    52   }
    53 
    54   override def exit()
    55   {
    56     PIDE.session.syslog_messages -= main_actor
    57   }
    58 }