src/Tools/jEdit/src/protocol_dockable.scala
changeset 43282 5d294220ca43
parent 39588 507fcf86e1e0
child 43520 cec9b95fa35d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Jun 08 17:42:07 2011 +0200
     1.3 @@ -0,0 +1,39 @@
     1.4 +/*  Title:      Tools/jEdit/src/protocol_dockable.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Dockable window for protocol messages.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +import scala.actors.Actor._
    1.16 +import scala.swing.{TextArea, ScrollPane}
    1.17 +
    1.18 +import org.gjt.sp.jedit.View
    1.19 +
    1.20 +
    1.21 +class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
    1.22 +{
    1.23 +  private val text_area = new TextArea
    1.24 +  set_content(new ScrollPane(text_area))
    1.25 +
    1.26 +
    1.27 +  /* main actor */
    1.28 +
    1.29 +  private val main_actor = actor {
    1.30 +    loop {
    1.31 +      react {
    1.32 +        case result: Isabelle_Process.Result =>
    1.33 +          Swing_Thread.now { text_area.append(result.message.toString + "\n") }
    1.34 +
    1.35 +        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    1.36 +      }
    1.37 +    }
    1.38 +  }
    1.39 +
    1.40 +  override def init() { Isabelle.session.raw_messages += main_actor }
    1.41 +  override def exit() { Isabelle.session.raw_messages -= main_actor }
    1.42 +}