src/Tools/jEdit/src/protocol_dockable.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 56715 52125652e82a
child 60074 38a64cc17403
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/protocol_dockable.scala
wenzelm@36760
     2
    Author:     Makarius
wenzelm@36760
     3
wenzelm@37067
     4
Dockable window for protocol messages.
wenzelm@36760
     5
*/
wenzelm@34408
     6
wenzelm@34318
     7
package isabelle.jedit
wenzelm@34318
     8
wenzelm@34318
     9
wenzelm@36015
    10
import isabelle._
wenzelm@36015
    11
wenzelm@37067
    12
import scala.swing.{TextArea, ScrollPane}
wenzelm@34318
    13
wenzelm@34318
    14
import org.gjt.sp.jedit.View
wenzelm@34424
    15
wenzelm@34318
    16
wenzelm@37067
    17
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@34760
    18
{
wenzelm@37067
    19
  private val text_area = new TextArea
wenzelm@37067
    20
  set_content(new ScrollPane(text_area))
wenzelm@34772
    21
wenzelm@34772
    22
wenzelm@56715
    23
  /* main */
immler@34671
    24
wenzelm@56715
    25
  private val main =
wenzelm@56715
    26
    Session.Consumer[Prover.Message](getClass.getName) {
wenzelm@56715
    27
      case input: Prover.Input =>
wenzelm@57612
    28
        GUI_Thread.later { text_area.append(input.toString + "\n\n") }
wenzelm@43721
    29
wenzelm@56715
    30
      case output: Prover.Output =>
wenzelm@57612
    31
        GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
wenzelm@34772
    32
    }
wenzelm@34772
    33
wenzelm@56715
    34
  override def init() { PIDE.session.all_messages += main }
wenzelm@56715
    35
  override def exit() { PIDE.session.all_messages -= main }
wenzelm@34318
    36
}