src/Tools/jEdit/src/raw_output_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 57612 990ffb84489b
child 66591 6efa351190d0
permissions -rw-r--r--
tuned signature;
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@37067
    12
import scala.swing.{TextArea, ScrollPane}
wenzelm@37065
    13
wenzelm@37065
    14
import org.gjt.sp.jedit.View
wenzelm@37065
    15
wenzelm@37065
    16
wenzelm@49559
    17
class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@37065
    18
{
wenzelm@37067
    19
  private val text_area = new TextArea
wenzelm@37067
    20
  set_content(new ScrollPane(text_area))
wenzelm@37065
    21
wenzelm@37065
    22
wenzelm@56715
    23
  /* main */
wenzelm@37065
    24
wenzelm@56715
    25
  private val main =
wenzelm@56715
    26
    Session.Consumer[Prover.Output](getClass.getName) {
wenzelm@56715
    27
      case output: Prover.Output =>
wenzelm@57612
    28
        GUI_Thread.later {
wenzelm@56715
    29
          text_area.append(XML.content(output.message))
wenzelm@56715
    30
          if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
wenzelm@56715
    31
        }
wenzelm@56715
    32
    }
wenzelm@37065
    33
wenzelm@56715
    34
  override def init() { PIDE.session.raw_output_messages += main }
wenzelm@56715
    35
  override def exit() { PIDE.session.raw_output_messages -= main }
wenzelm@37065
    36
}