src/Tools/jEdit/src/jedit/session_dockable.scala
author wenzelm
Fri Sep 24 00:00:21 2010 +0200 (2010-09-24)
changeset 39635 5cd8545a070b
parent 39629 08eb2730a8a1
child 39638 4293ce5b07fb
permissions -rw-r--r--
added Session_Dockable.session_phase label;
wenzelm@39515
     1
/*  Title:      Tools/jEdit/src/jedit/session_dockable.scala
wenzelm@39515
     2
    Author:     Makarius
wenzelm@39515
     3
wenzelm@39515
     4
Dockable window for prover session management.
wenzelm@39515
     5
*/
wenzelm@39515
     6
wenzelm@39515
     7
package isabelle.jedit
wenzelm@39515
     8
wenzelm@39515
     9
wenzelm@39515
    10
import isabelle._
wenzelm@39515
    11
wenzelm@39515
    12
import scala.actors.Actor._
wenzelm@39635
    13
import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane,
wenzelm@39635
    14
  Component, Swing}
wenzelm@39593
    15
import scala.swing.event.ButtonClicked
wenzelm@39593
    16
wenzelm@39593
    17
import java.awt.BorderLayout
wenzelm@39515
    18
wenzelm@39515
    19
import org.gjt.sp.jedit.View
wenzelm@39515
    20
wenzelm@39515
    21
wenzelm@39515
    22
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
wenzelm@39515
    23
{
wenzelm@39591
    24
  /* main tabs */
wenzelm@39591
    25
wenzelm@39591
    26
  private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
wenzelm@39591
    27
  readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
wenzelm@39591
    28
wenzelm@39629
    29
  private val syslog = new TextArea(Isabelle.session.syslog())
wenzelm@39591
    30
  syslog.editable = false
wenzelm@39591
    31
wenzelm@39591
    32
  private val tabs = new TabbedPane {
wenzelm@39591
    33
    pages += new TabbedPane.Page("README", Component.wrap(readme))
wenzelm@39591
    34
    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
wenzelm@39591
    35
  }
wenzelm@39591
    36
wenzelm@39591
    37
  set_content(tabs)
wenzelm@39515
    38
wenzelm@39515
    39
wenzelm@39593
    40
  /* controls */
wenzelm@39593
    41
wenzelm@39635
    42
  val session_phase = new Label(Isabelle.session.phase.toString)
wenzelm@39635
    43
  session_phase.border = Swing.EtchedBorder(Swing.Lowered)
wenzelm@39635
    44
  session_phase.tooltip = "Prover process status"
wenzelm@39635
    45
wenzelm@39593
    46
  private val interrupt = new Button("Interrupt") {
wenzelm@39593
    47
    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
wenzelm@39593
    48
  }
wenzelm@39593
    49
  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
wenzelm@39593
    50
wenzelm@39635
    51
  private val controls =
wenzelm@39635
    52
    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt)
wenzelm@39593
    53
  add(controls.peer, BorderLayout.NORTH)
wenzelm@39593
    54
wenzelm@39593
    55
wenzelm@39515
    56
  /* main actor */
wenzelm@39515
    57
wenzelm@39515
    58
  private val main_actor = actor {
wenzelm@39515
    59
    loop {
wenzelm@39515
    60
      react {
wenzelm@39589
    61
        case result: Isabelle_Process.Result =>
wenzelm@39625
    62
          if (result.is_syslog)
wenzelm@39625
    63
            Swing_Thread.now {
wenzelm@39629
    64
              val text = Isabelle.session.syslog()
wenzelm@39626
    65
              if (text != syslog.text) {
wenzelm@39626
    66
                syslog.text = text
wenzelm@39626
    67
              }
wenzelm@39625
    68
            }
wenzelm@39589
    69
wenzelm@39635
    70
        case (_, phase: Session.Phase) =>
wenzelm@39635
    71
          Swing_Thread.now { session_phase.text = phase.toString }
wenzelm@39635
    72
wenzelm@39515
    73
        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
wenzelm@39515
    74
      }
wenzelm@39515
    75
    }
wenzelm@39515
    76
  }
wenzelm@39515
    77
wenzelm@39635
    78
  override def init() {
wenzelm@39635
    79
    Isabelle.session.raw_messages += main_actor
wenzelm@39635
    80
    Isabelle.session.phase_changed += main_actor
wenzelm@39635
    81
  }
wenzelm@39635
    82
wenzelm@39635
    83
  override def exit() {
wenzelm@39635
    84
    Isabelle.session.raw_messages -= main_actor
wenzelm@39635
    85
    Isabelle.session.phase_changed -= main_actor
wenzelm@39635
    86
  }
wenzelm@39515
    87
}