src/Tools/jEdit/src/syslog_dockable.scala
author wenzelm
Sun Nov 25 20:59:32 2012 +0100 (2012-11-25)
changeset 50205 788c8263e634
parent 49559 c3a6e110679b
child 53177 dcac8d837b9c
permissions -rw-r--r--
renamed main plugin object to PIDE;
     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.later {
    27       val text = PIDE.session.current_syslog()
    28       if (text != syslog.text) syslog.text = text
    29     }
    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) 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 }