src/Tools/jEdit/src/raw_output_dockable.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 44297 b3bd26fd22d3
child 44734 7313e2db3d39
permissions -rw-r--r--
propagate editor perspective through document model;
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@43721
    32
        case input: Isabelle_Process.Input =>
wenzelm@43721
    33
wenzelm@37065
    34
        case result: Isabelle_Process.Result =>
wenzelm@39588
    35
          if (result.is_stdout)
wenzelm@39588
    36
            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
wenzelm@37065
    37
wenzelm@37067
    38
        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
wenzelm@37065
    39
      }
wenzelm@37065
    40
    }
wenzelm@37065
    41
  }
wenzelm@37065
    42
wenzelm@39588
    43
  override def init() { Isabelle.session.raw_messages += main_actor }
wenzelm@39588
    44
  override def exit() { Isabelle.session.raw_messages -= main_actor }
wenzelm@37065
    45
}