src/Tools/jEdit/src/protocol_dockable.scala
author wenzelm
Wed Jun 08 17:42:07 2011 +0200 (2011-06-08)
changeset 43282 5d294220ca43
parent 39588 src/Tools/jEdit/src/jedit/protocol_dockable.scala@507fcf86e1e0
child 43520 cec9b95fa35d
permissions -rw-r--r--
moved sources -- eliminated Netbeans artifact of jedit package directory;
     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 scala.actors.Actor._
    13 import scala.swing.{TextArea, ScrollPane}
    14 
    15 import org.gjt.sp.jedit.View
    16 
    17 
    18 class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
    19 {
    20   private val text_area = new TextArea
    21   set_content(new ScrollPane(text_area))
    22 
    23 
    24   /* main actor */
    25 
    26   private val main_actor = actor {
    27     loop {
    28       react {
    29         case result: Isabelle_Process.Result =>
    30           Swing_Thread.now { text_area.append(result.message.toString + "\n") }
    31 
    32         case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    33       }
    34     }
    35   }
    36 
    37   override def init() { Isabelle.session.raw_messages += main_actor }
    38   override def exit() { Isabelle.session.raw_messages -= main_actor }
    39 }