src/Tools/jEdit/src/raw_output_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56385 76acce58aeab
child 57612 990ffb84489b
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
     1 /*  Title:      Tools/jEdit/src/raw_output_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for raw process output (stdout).
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.swing.{TextArea, ScrollPane}
    13 
    14 import org.gjt.sp.jedit.View
    15 
    16 
    17 class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position)
    18 {
    19   private val text_area = new TextArea
    20   set_content(new ScrollPane(text_area))
    21 
    22 
    23   /* main */
    24 
    25   private val main =
    26     Session.Consumer[Prover.Output](getClass.getName) {
    27       case output: Prover.Output =>
    28         Swing_Thread.later {
    29           text_area.append(XML.content(output.message))
    30           if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
    31         }
    32     }
    33 
    34   override def init() { PIDE.session.raw_output_messages += main }
    35   override def exit() { PIDE.session.raw_output_messages -= main }
    36 }