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