src/Tools/jEdit/src/session_dockable.scala
author wenzelm
Mon Jul 04 22:11:32 2011 +0200 (2011-07-04)
changeset 43661 39fdbd814c7f
parent 43606 e1a09c2a6248
child 43721 fad8634cee62
permissions -rw-r--r--
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/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@39734
    13
import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
wenzelm@39638
    14
import scala.swing.event.{ButtonClicked, SelectionChanged}
wenzelm@39593
    15
wenzelm@43520
    16
import java.lang.System
wenzelm@39593
    17
import java.awt.BorderLayout
wenzelm@39697
    18
import javax.swing.border.{BevelBorder, SoftBevelBorder}
wenzelm@39515
    19
wenzelm@39515
    20
import org.gjt.sp.jedit.View
wenzelm@39515
    21
wenzelm@39515
    22
wenzelm@39515
    23
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
wenzelm@39515
    24
{
wenzelm@39591
    25
  /* main tabs */
wenzelm@39591
    26
wenzelm@43661
    27
  private val readme = new HTML_Panel("SansSerif", 14)
wenzelm@43661
    28
  readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
wenzelm@39591
    29
wenzelm@39629
    30
  private val syslog = new TextArea(Isabelle.session.syslog())
wenzelm@39591
    31
  syslog.editable = false
wenzelm@39591
    32
wenzelm@39591
    33
  private val tabs = new TabbedPane {
wenzelm@39591
    34
    pages += new TabbedPane.Page("README", Component.wrap(readme))
wenzelm@39591
    35
    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
wenzelm@39638
    36
wenzelm@39638
    37
    selection.index =
wenzelm@39638
    38
    {
wenzelm@39638
    39
      val index = Isabelle.Int_Property("session-panel.selection", 0)
wenzelm@39638
    40
      if (index >= pages.length) 0 else index
wenzelm@39638
    41
    }
wenzelm@39638
    42
    listenTo(selection)
wenzelm@39638
    43
    reactions += {
wenzelm@39638
    44
      case SelectionChanged(_) =>
wenzelm@39638
    45
        Isabelle.Int_Property("session-panel.selection") = selection.index
wenzelm@39638
    46
    }
wenzelm@39591
    47
  }
wenzelm@39591
    48
wenzelm@39591
    49
  set_content(tabs)
wenzelm@39515
    50
wenzelm@39515
    51
wenzelm@39593
    52
  /* controls */
wenzelm@39593
    53
wenzelm@39635
    54
  val session_phase = new Label(Isabelle.session.phase.toString)
wenzelm@39697
    55
  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
wenzelm@39697
    56
  session_phase.tooltip = "Prover status"
wenzelm@39635
    57
wenzelm@39734
    58
  private val interrupt = new Button("Interrupt") {
wenzelm@39734
    59
    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
wenzelm@39702
    60
  }
wenzelm@39734
    61
  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
wenzelm@39702
    62
wenzelm@39702
    63
  private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
wenzelm@39702
    64
  logic.listenTo(logic.selection)
wenzelm@39702
    65
  logic.reactions += {
wenzelm@39702
    66
    case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
wenzelm@39702
    67
  }
wenzelm@39702
    68
wenzelm@39635
    69
  private val controls =
wenzelm@39734
    70
    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
wenzelm@39593
    71
  add(controls.peer, BorderLayout.NORTH)
wenzelm@39593
    72
wenzelm@39593
    73
wenzelm@39515
    74
  /* main actor */
wenzelm@39515
    75
wenzelm@39515
    76
  private val main_actor = actor {
wenzelm@39515
    77
    loop {
wenzelm@39515
    78
      react {
wenzelm@39589
    79
        case result: Isabelle_Process.Result =>
wenzelm@39625
    80
          if (result.is_syslog)
wenzelm@39625
    81
            Swing_Thread.now {
wenzelm@39629
    82
              val text = Isabelle.session.syslog()
wenzelm@39626
    83
              if (text != syslog.text) {
wenzelm@39626
    84
                syslog.text = text
wenzelm@39626
    85
              }
wenzelm@39625
    86
            }
wenzelm@39589
    87
wenzelm@39701
    88
        case phase: Session.Phase =>
wenzelm@39696
    89
          Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
wenzelm@39635
    90
wenzelm@39515
    91
        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
wenzelm@39515
    92
      }
wenzelm@39515
    93
    }
wenzelm@39515
    94
  }
wenzelm@39515
    95
wenzelm@39635
    96
  override def init() {
wenzelm@39635
    97
    Isabelle.session.raw_messages += main_actor
wenzelm@39635
    98
    Isabelle.session.phase_changed += main_actor
wenzelm@39635
    99
  }
wenzelm@39635
   100
wenzelm@39635
   101
  override def exit() {
wenzelm@39635
   102
    Isabelle.session.raw_messages -= main_actor
wenzelm@39635
   103
    Isabelle.session.phase_changed -= main_actor
wenzelm@39635
   104
  }
wenzelm@39515
   105
}