src/Tools/jEdit/src/jedit/session_dockable.scala
author wenzelm
Thu Sep 23 14:39:29 2010 +0200 (2010-09-23)
changeset 39625 fb0c851e4f9d
parent 39593 1a34187f0b97
child 39626 a5d0bcfb95a3
permissions -rw-r--r--
tuned prover message categorization;
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@39593
    13
import scala.swing.{FlowPanel, Button, TextArea, ScrollPane, TabbedPane, Component}
wenzelm@39593
    14
import scala.swing.event.ButtonClicked
wenzelm@39593
    15
wenzelm@39593
    16
import java.awt.BorderLayout
wenzelm@39515
    17
wenzelm@39515
    18
import org.gjt.sp.jedit.View
wenzelm@39515
    19
wenzelm@39515
    20
wenzelm@39515
    21
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
wenzelm@39515
    22
{
wenzelm@39591
    23
  /* main tabs */
wenzelm@39591
    24
wenzelm@39591
    25
  private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
wenzelm@39591
    26
  readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
wenzelm@39591
    27
wenzelm@39591
    28
  private val syslog = new TextArea
wenzelm@39591
    29
  syslog.editable = false
wenzelm@39591
    30
wenzelm@39591
    31
  private val tabs = new TabbedPane {
wenzelm@39591
    32
    pages += new TabbedPane.Page("README", Component.wrap(readme))
wenzelm@39591
    33
    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
wenzelm@39591
    34
  }
wenzelm@39591
    35
wenzelm@39591
    36
  set_content(tabs)
wenzelm@39515
    37
wenzelm@39515
    38
wenzelm@39593
    39
  /* controls */
wenzelm@39593
    40
wenzelm@39593
    41
  private val interrupt = new Button("Interrupt") {
wenzelm@39593
    42
    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
wenzelm@39593
    43
  }
wenzelm@39593
    44
  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
wenzelm@39593
    45
wenzelm@39593
    46
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(interrupt)
wenzelm@39593
    47
  add(controls.peer, BorderLayout.NORTH)
wenzelm@39593
    48
wenzelm@39593
    49
wenzelm@39515
    50
  /* main actor */
wenzelm@39515
    51
wenzelm@39515
    52
  private val main_actor = actor {
wenzelm@39515
    53
    loop {
wenzelm@39515
    54
      react {
wenzelm@39589
    55
        case result: Isabelle_Process.Result =>
wenzelm@39625
    56
          if (result.is_syslog)
wenzelm@39625
    57
            Swing_Thread.now {
wenzelm@39625
    58
              syslog.append(XML.content(result.message).mkString + "\n")
wenzelm@39625
    59
            }
wenzelm@39589
    60
wenzelm@39515
    61
        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
wenzelm@39515
    62
      }
wenzelm@39515
    63
    }
wenzelm@39515
    64
  }
wenzelm@39515
    65
wenzelm@39589
    66
  override def init() { Isabelle.session.raw_messages += main_actor }
wenzelm@39589
    67
  override def exit() { Isabelle.session.raw_messages -= main_actor }
wenzelm@39515
    68
}