src/Tools/jEdit/src/session_dockable.scala
changeset 43282 5d294220ca43
parent 39736 e19cece7d18a
child 43520 cec9b95fa35d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Jun 08 17:42:07 2011 +0200
     1.3 @@ -0,0 +1,104 @@
     1.4 +/*  Title:      Tools/jEdit/src/session_dockable.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Dockable window for prover session management.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +import scala.actors.Actor._
    1.16 +import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
    1.17 +import scala.swing.event.{ButtonClicked, SelectionChanged}
    1.18 +
    1.19 +import java.awt.BorderLayout
    1.20 +import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.21 +
    1.22 +import org.gjt.sp.jedit.View
    1.23 +
    1.24 +
    1.25 +class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
    1.26 +{
    1.27 +  /* main tabs */
    1.28 +
    1.29 +  private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
    1.30 +  readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
    1.31 +
    1.32 +  private val syslog = new TextArea(Isabelle.session.syslog())
    1.33 +  syslog.editable = false
    1.34 +
    1.35 +  private val tabs = new TabbedPane {
    1.36 +    pages += new TabbedPane.Page("README", Component.wrap(readme))
    1.37 +    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
    1.38 +
    1.39 +    selection.index =
    1.40 +    {
    1.41 +      val index = Isabelle.Int_Property("session-panel.selection", 0)
    1.42 +      if (index >= pages.length) 0 else index
    1.43 +    }
    1.44 +    listenTo(selection)
    1.45 +    reactions += {
    1.46 +      case SelectionChanged(_) =>
    1.47 +        Isabelle.Int_Property("session-panel.selection") = selection.index
    1.48 +    }
    1.49 +  }
    1.50 +
    1.51 +  set_content(tabs)
    1.52 +
    1.53 +
    1.54 +  /* controls */
    1.55 +
    1.56 +  val session_phase = new Label(Isabelle.session.phase.toString)
    1.57 +  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
    1.58 +  session_phase.tooltip = "Prover status"
    1.59 +
    1.60 +  private val interrupt = new Button("Interrupt") {
    1.61 +    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
    1.62 +  }
    1.63 +  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
    1.64 +
    1.65 +  private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
    1.66 +  logic.listenTo(logic.selection)
    1.67 +  logic.reactions += {
    1.68 +    case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
    1.69 +  }
    1.70 +
    1.71 +  private val controls =
    1.72 +    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
    1.73 +  add(controls.peer, BorderLayout.NORTH)
    1.74 +
    1.75 +
    1.76 +  /* main actor */
    1.77 +
    1.78 +  private val main_actor = actor {
    1.79 +    loop {
    1.80 +      react {
    1.81 +        case result: Isabelle_Process.Result =>
    1.82 +          if (result.is_syslog)
    1.83 +            Swing_Thread.now {
    1.84 +              val text = Isabelle.session.syslog()
    1.85 +              if (text != syslog.text) {
    1.86 +                syslog.text = text
    1.87 +              }
    1.88 +            }
    1.89 +
    1.90 +        case phase: Session.Phase =>
    1.91 +          Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
    1.92 +
    1.93 +        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
    1.94 +      }
    1.95 +    }
    1.96 +  }
    1.97 +
    1.98 +  override def init() {
    1.99 +    Isabelle.session.raw_messages += main_actor
   1.100 +    Isabelle.session.phase_changed += main_actor
   1.101 +  }
   1.102 +
   1.103 +  override def exit() {
   1.104 +    Isabelle.session.raw_messages -= main_actor
   1.105 +    Isabelle.session.phase_changed -= main_actor
   1.106 +  }
   1.107 +}