src/Tools/jEdit/src/raw_output_dockable.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 46918 1752164d916b
child 49416 1053a564dd25
permissions -rw-r--r--
more explicit indication of swing thread context;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/raw_output_dockable.scala
wenzelm@37065
     2
    Author:     Makarius
wenzelm@37065
     3
wenzelm@37065
     4
Dockable window for raw process output (stdout).
wenzelm@37065
     5
*/
wenzelm@37065
     6
wenzelm@37065
     7
package isabelle.jedit
wenzelm@37065
     8
wenzelm@37065
     9
wenzelm@37065
    10
import isabelle._
wenzelm@37065
    11
wenzelm@43520
    12
import java.lang.System
wenzelm@43520
    13
wenzelm@37065
    14
import scala.actors.Actor._
wenzelm@37067
    15
import scala.swing.{TextArea, ScrollPane}
wenzelm@37065
    16
wenzelm@37065
    17
import org.gjt.sp.jedit.View
wenzelm@37065
    18
wenzelm@37065
    19
wenzelm@37067
    20
class Raw_Output_Dockable(view: View, position: String)
wenzelm@37067
    21
  extends Dockable(view: View, position: String)
wenzelm@37065
    22
{
wenzelm@37067
    23
  private val text_area = new TextArea
wenzelm@37067
    24
  set_content(new ScrollPane(text_area))
wenzelm@37065
    25
wenzelm@37065
    26
wenzelm@37067
    27
  /* main actor */
wenzelm@37065
    28
wenzelm@37067
    29
  private val main_actor = actor {
wenzelm@37065
    30
    loop {
wenzelm@37065
    31
      react {
wenzelm@46772
    32
        case output: Isabelle_Process.Output =>
wenzelm@46772
    33
          if (output.is_stdout || output.is_stderr)
wenzelm@46918
    34
            Swing_Thread.later { text_area.append(XML.content(output.message).mkString) }
wenzelm@37065
    35
wenzelm@37067
    36
        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
wenzelm@37065
    37
      }
wenzelm@37065
    38
    }
wenzelm@37065
    39
  }
wenzelm@37065
    40
wenzelm@44734
    41
  override def init() { Isabelle.session.raw_output_messages += main_actor }
wenzelm@44734
    42
  override def exit() { Isabelle.session.raw_output_messages -= main_actor }
wenzelm@37065
    43
}