src/Tools/jEdit/src/session_dockable.scala
author wenzelm
Sat, 20 Aug 2011 20:24:12 +0200
changeset 44335 156be0e43336
parent 44297 b3bd26fd22d3
child 44609 6ec4a5eb2fc0
permissions -rw-r--r--
discontinued "Interrupt", which could disturb administrative tasks of the document model;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 39736
diff changeset
     1
/*  Title:      Tools/jEdit/src/session_dockable.scala
39515
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._
39734
47f5a8c92666 moved "auto-start" to options panel;
wenzelm
parents: 39702
diff changeset
    13
import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
39638
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    14
import scala.swing.event.{ButtonClicked, SelectionChanged}
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    15
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43282
diff changeset
    16
import java.lang.System
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    17
import java.awt.BorderLayout
39697
d54242927fb1 tuned border;
wenzelm
parents: 39696
diff changeset
    18
import javax.swing.border.{BevelBorder, SoftBevelBorder}
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    19
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    20
import org.gjt.sp.jedit.View
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    21
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    22
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    23
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    24
{
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39589
diff changeset
    25
  /* main tabs */
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39589
diff changeset
    26
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43606
diff changeset
    27
  private val readme = new HTML_Panel("SansSerif", 14)
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43606
diff changeset
    28
  readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39589
diff changeset
    29
39629
08eb2730a8a1 tuned signature;
wenzelm
parents: 39626
diff changeset
    30
  private val syslog = new TextArea(Isabelle.session.syslog())
39591
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))
39638
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    35
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    36
    selection.index =
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    37
    {
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    38
      val index = Isabelle.Int_Property("session-panel.selection", 0)
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    39
      if (index >= pages.length) 0 else index
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    40
    }
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    41
    listenTo(selection)
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    42
    reactions += {
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    43
      case SelectionChanged(_) =>
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    44
        Isabelle.Int_Property("session-panel.selection") = selection.index
4293ce5b07fb persistent session-panel.selection;
wenzelm
parents: 39635
diff changeset
    45
    }
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39589
diff changeset
    46
  }
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39589
diff changeset
    47
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39589
diff changeset
    48
  set_content(tabs)
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    49
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    50
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    51
  /* controls */
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    52
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    53
  val session_phase = new Label(Isabelle.session.phase.toString)
39697
d54242927fb1 tuned border;
wenzelm
parents: 39696
diff changeset
    54
  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
d54242927fb1 tuned border;
wenzelm
parents: 39696
diff changeset
    55
  session_phase.tooltip = "Prover status"
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    56
39702
d7c256cb2797 Session_Dockable: more startup controls;
wenzelm
parents: 39701
diff changeset
    57
  private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
d7c256cb2797 Session_Dockable: more startup controls;
wenzelm
parents: 39701
diff changeset
    58
  logic.listenTo(logic.selection)
d7c256cb2797 Session_Dockable: more startup controls;
wenzelm
parents: 39701
diff changeset
    59
  logic.reactions += {
d7c256cb2797 Session_Dockable: more startup controls;
wenzelm
parents: 39701
diff changeset
    60
    case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
d7c256cb2797 Session_Dockable: more startup controls;
wenzelm
parents: 39701
diff changeset
    61
  }
d7c256cb2797 Session_Dockable: more startup controls;
wenzelm
parents: 39701
diff changeset
    62
44335
156be0e43336 discontinued "Interrupt", which could disturb administrative tasks of the document model;
wenzelm
parents: 44297
diff changeset
    63
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    64
  add(controls.peer, BorderLayout.NORTH)
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    65
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    66
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    67
  /* main actor */
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    68
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    69
  private val main_actor = actor {
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    70
    loop {
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    71
      react {
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43661
diff changeset
    72
        case input: Isabelle_Process.Input =>
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43661
diff changeset
    73
39589
5b81b8df1dde Session_Dockable: basic syslog output;
wenzelm
parents: 39516
diff changeset
    74
        case result: Isabelle_Process.Result =>
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
    75
          if (result.is_syslog)
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
    76
            Swing_Thread.now {
39629
08eb2730a8a1 tuned signature;
wenzelm
parents: 39626
diff changeset
    77
              val text = Isabelle.session.syslog()
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
    78
              if (text != syslog.text) {
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
    79
                syslog.text = text
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
    80
              }
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
    81
            }
39589
5b81b8df1dde Session_Dockable: basic syslog output;
wenzelm
parents: 39516
diff changeset
    82
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39697
diff changeset
    83
        case phase: Session.Phase =>
39696
f4da0428dc78 more informative Session.Phase;
wenzelm
parents: 39638
diff changeset
    84
          Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    85
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    86
        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    87
      }
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    88
    }
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    89
  }
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    90
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    91
  override def init() {
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    92
    Isabelle.session.raw_messages += main_actor
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    93
    Isabelle.session.phase_changed += main_actor
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    94
  }
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    95
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    96
  override def exit() {
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    97
    Isabelle.session.raw_messages -= main_actor
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    98
    Isabelle.session.phase_changed -= main_actor
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    99
  }
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   100
}