src/Tools/jEdit/src/protocol_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 60074 38a64cc17403
child 66205 e9fa94f43a15
permissions -rw-r--r--
tuned signature;
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@60074
    12
import java.awt.BorderLayout
wenzelm@60074
    13
wenzelm@37067
    14
import scala.swing.{TextArea, ScrollPane}
wenzelm@34318
    15
wenzelm@34318
    16
import org.gjt.sp.jedit.View
wenzelm@34424
    17
wenzelm@34318
    18
wenzelm@37067
    19
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@34760
    20
{
wenzelm@60074
    21
  /* controls */
wenzelm@60074
    22
wenzelm@60074
    23
  private val ml_stats = new Isabelle.ML_Stats
wenzelm@60074
    24
wenzelm@60074
    25
  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats)
wenzelm@60074
    26
wenzelm@60074
    27
wenzelm@60074
    28
  /* text area */
wenzelm@60074
    29
wenzelm@37067
    30
  private val text_area = new TextArea
wenzelm@60074
    31
wenzelm@60074
    32
wenzelm@60074
    33
  /* layout */
wenzelm@60074
    34
wenzelm@37067
    35
  set_content(new ScrollPane(text_area))
wenzelm@60074
    36
  add(controls.peer, BorderLayout.NORTH)
wenzelm@34772
    37
wenzelm@34772
    38
wenzelm@56715
    39
  /* main */
immler@34671
    40
wenzelm@56715
    41
  private val main =
wenzelm@60074
    42
    Session.Consumer[Any](getClass.getName) {
wenzelm@56715
    43
      case input: Prover.Input =>
wenzelm@57612
    44
        GUI_Thread.later { text_area.append(input.toString + "\n\n") }
wenzelm@43721
    45
wenzelm@56715
    46
      case output: Prover.Output =>
wenzelm@57612
    47
        GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
wenzelm@60074
    48
wenzelm@60074
    49
      case _: Session.Global_Options =>
wenzelm@60074
    50
        GUI_Thread.later { ml_stats.load() }
wenzelm@34772
    51
    }
wenzelm@34772
    52
wenzelm@60074
    53
  override def init()
wenzelm@60074
    54
  {
wenzelm@60074
    55
    PIDE.session.all_messages += main
wenzelm@60074
    56
    PIDE.session.global_options += main
wenzelm@60074
    57
  }
wenzelm@60074
    58
wenzelm@60074
    59
  override def exit()
wenzelm@60074
    60
  {
wenzelm@60074
    61
    PIDE.session.all_messages -= main
wenzelm@60074
    62
    PIDE.session.global_options -= main
wenzelm@60074
    63
  }
wenzelm@34318
    64
}