src/Tools/jEdit/src/protocol_dockable.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 46918 1752164d916b
child 50205 788c8263e634
permissions -rw-r--r--
more explicit indication of swing thread context;
     1 /*  Title:      Tools/jEdit/src/protocol_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for protocol messages.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.lang.System
    13 
    14 import scala.actors.Actor._
    15 import scala.swing.{TextArea, ScrollPane}
    16 
    17 import org.gjt.sp.jedit.View
    18 
    19 
    20 class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
    21 {
    22   private val text_area = new TextArea
    23   set_content(new ScrollPane(text_area))
    24 
    25 
    26   /* main actor */
    27 
    28   private val main_actor = actor {
    29     loop {
    30       react {
    31         case input: Isabelle_Process.Input =>
    32           Swing_Thread.later { text_area.append(input.toString + "\n") }
    33 
    34         case output: Isabelle_Process.Output =>
    35           Swing_Thread.later { text_area.append(output.message.toString + "\n") }
    36 
    37         case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    38       }
    39     }
    40   }
    41 
    42   override def init() { Isabelle.session.all_messages += main_actor }
    43   override def exit() { Isabelle.session.all_messages -= main_actor }
    44 }