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