src/Tools/jEdit/src/jedit/session_dockable.scala
author wenzelm
Wed Sep 22 15:01:34 2010 +0200 (2010-09-22)
changeset 39589 5b81b8df1dde
parent 39516 8a70e91650a6
child 39591 a43a723753e6
permissions -rw-r--r--
Session_Dockable: basic syslog output;
wenzelm@39515
     1
/*  Title:      Tools/jEdit/src/jedit/session_dockable.scala
wenzelm@39515
     2
    Author:     Makarius
wenzelm@39515
     3
wenzelm@39515
     4
Dockable window for prover session management.
wenzelm@39515
     5
*/
wenzelm@39515
     6
wenzelm@39515
     7
package isabelle.jedit
wenzelm@39515
     8
wenzelm@39515
     9
wenzelm@39515
    10
import isabelle._
wenzelm@39515
    11
wenzelm@39515
    12
import scala.actors.Actor._
wenzelm@39515
    13
import scala.swing.{TextArea, ScrollPane}
wenzelm@39515
    14
wenzelm@39515
    15
import org.gjt.sp.jedit.View
wenzelm@39515
    16
wenzelm@39515
    17
wenzelm@39515
    18
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
wenzelm@39515
    19
{
wenzelm@39589
    20
  private val text_area = new TextArea
wenzelm@39516
    21
  text_area.editable = false
wenzelm@39515
    22
  set_content(new ScrollPane(text_area))
wenzelm@39515
    23
wenzelm@39515
    24
wenzelm@39515
    25
  /* main actor */
wenzelm@39515
    26
wenzelm@39515
    27
  private val main_actor = actor {
wenzelm@39515
    28
    loop {
wenzelm@39515
    29
      react {
wenzelm@39589
    30
        case result: Isabelle_Process.Result =>
wenzelm@39589
    31
          if (result.is_init || result.is_exit || result.is_system)
wenzelm@39589
    32
            Swing_Thread.now { text_area.append(XML.content(result.message).mkString + "\n") }
wenzelm@39589
    33
wenzelm@39515
    34
        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
wenzelm@39515
    35
      }
wenzelm@39515
    36
    }
wenzelm@39515
    37
  }
wenzelm@39515
    38
wenzelm@39589
    39
  override def init() { Isabelle.session.raw_messages += main_actor }
wenzelm@39589
    40
  override def exit() { Isabelle.session.raw_messages -= main_actor }
wenzelm@39515
    41
}