wenzelm@44162
|
1 |
/* Title: Tools/jEdit/src/session_dockable.scala
|
wenzelm@39784
|
2 |
Author: Makarius
|
wenzelm@39784
|
3 |
|
wenzelm@39784
|
4 |
Dockable window for prover session management.
|
wenzelm@39784
|
5 |
*/
|
wenzelm@39784
|
6 |
|
wenzelm@39784
|
7 |
package isabelle.jedit
|
wenzelm@39784
|
8 |
|
wenzelm@39784
|
9 |
|
wenzelm@39784
|
10 |
import isabelle._
|
wenzelm@39784
|
11 |
|
wenzelm@39784
|
12 |
import scala.actors.Actor._
|
wenzelm@45828
|
13 |
import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
|
wenzelm@45500
|
14 |
ScrollPane, TabbedPane, Component, Swing}
|
wenzelm@39928
|
15 |
import scala.swing.event.{ButtonClicked, SelectionChanged}
|
wenzelm@39857
|
16 |
|
wenzelm@44400
|
17 |
import java.lang.System
|
wenzelm@45851
|
18 |
import java.awt.{BorderLayout, Graphics2D, Insets}
|
wenzelm@45870
|
19 |
import javax.swing.{JList, DefaultListCellRenderer, BorderFactory}
|
wenzelm@39962
|
20 |
import javax.swing.border.{BevelBorder, SoftBevelBorder}
|
wenzelm@39784
|
21 |
|
wenzelm@45737
|
22 |
import org.gjt.sp.jedit.{View, jEdit}
|
wenzelm@39784
|
23 |
|
wenzelm@39784
|
24 |
|
wenzelm@39784
|
25 |
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
|
wenzelm@39784
|
26 |
{
|
wenzelm@39855
|
27 |
/* main tabs */
|
wenzelm@39855
|
28 |
|
wenzelm@44532
|
29 |
private val readme = new HTML_Panel("SansSerif", 14)
|
wenzelm@44532
|
30 |
readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
|
wenzelm@39855
|
31 |
|
wenzelm@45828
|
32 |
val status = new ListView(Nil: List[Document.Node.Name])
|
wenzelm@45500
|
33 |
status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
|
wenzelm@45500
|
34 |
status.selection.intervalMode = ListView.IntervalMode.Single
|
wenzelm@45500
|
35 |
|
wenzelm@39919
|
36 |
private val syslog = new TextArea(Isabelle.session.syslog())
|
wenzelm@39855
|
37 |
|
wenzelm@39855
|
38 |
private val tabs = new TabbedPane {
|
wenzelm@39855
|
39 |
pages += new TabbedPane.Page("README", Component.wrap(readme))
|
wenzelm@45500
|
40 |
pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
|
wenzelm@45500
|
41 |
pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
|
wenzelm@39928
|
42 |
|
wenzelm@39928
|
43 |
selection.index =
|
wenzelm@39928
|
44 |
{
|
wenzelm@39928
|
45 |
val index = Isabelle.Int_Property("session-panel.selection", 0)
|
wenzelm@39928
|
46 |
if (index >= pages.length) 0 else index
|
wenzelm@39928
|
47 |
}
|
wenzelm@39928
|
48 |
listenTo(selection)
|
wenzelm@39928
|
49 |
reactions += {
|
wenzelm@39928
|
50 |
case SelectionChanged(_) =>
|
wenzelm@39928
|
51 |
Isabelle.Int_Property("session-panel.selection") = selection.index
|
wenzelm@39928
|
52 |
}
|
wenzelm@39855
|
53 |
}
|
wenzelm@39855
|
54 |
|
wenzelm@39855
|
55 |
set_content(tabs)
|
wenzelm@39784
|
56 |
|
wenzelm@39784
|
57 |
|
wenzelm@39857
|
58 |
/* controls */
|
wenzelm@39857
|
59 |
|
wenzelm@39925
|
60 |
val session_phase = new Label(Isabelle.session.phase.toString)
|
wenzelm@39962
|
61 |
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
|
wenzelm@39962
|
62 |
session_phase.tooltip = "Prover status"
|
wenzelm@39925
|
63 |
|
wenzelm@45646
|
64 |
private val cancel = new Button("Cancel") {
|
wenzelm@45736
|
65 |
reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
|
wenzelm@45646
|
66 |
}
|
wenzelm@45737
|
67 |
cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
|
wenzelm@45646
|
68 |
|
wenzelm@45647
|
69 |
private val check = new Button("Check") {
|
wenzelm@45736
|
70 |
reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
|
wenzelm@45647
|
71 |
}
|
wenzelm@45737
|
72 |
check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
|
wenzelm@45647
|
73 |
|
wenzelm@39967
|
74 |
private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
|
wenzelm@39967
|
75 |
logic.listenTo(logic.selection)
|
wenzelm@39967
|
76 |
logic.reactions += {
|
wenzelm@39967
|
77 |
case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
|
wenzelm@39967
|
78 |
}
|
wenzelm@39967
|
79 |
|
wenzelm@45646
|
80 |
private val controls =
|
wenzelm@45647
|
81 |
new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
|
wenzelm@39857
|
82 |
add(controls.peer, BorderLayout.NORTH)
|
wenzelm@39857
|
83 |
|
wenzelm@39857
|
84 |
|
wenzelm@45500
|
85 |
/* component state -- owned by Swing thread */
|
wenzelm@45500
|
86 |
|
wenzelm@45738
|
87 |
private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
|
wenzelm@45738
|
88 |
|
wenzelm@45871
|
89 |
private object Node_Renderer_Component extends Label
|
wenzelm@45738
|
90 |
{
|
wenzelm@45871
|
91 |
opaque = false
|
wenzelm@45828
|
92 |
xAlignment = Alignment.Leading
|
wenzelm@45870
|
93 |
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
|
wenzelm@45828
|
94 |
|
wenzelm@45828
|
95 |
var node_name = Document.Node.Name.empty
|
wenzelm@45828
|
96 |
override def paintComponent(gfx: Graphics2D)
|
wenzelm@45738
|
97 |
{
|
wenzelm@45828
|
98 |
nodes_status.get(node_name) match {
|
wenzelm@45738
|
99 |
case Some(st) if st.total > 0 =>
|
wenzelm@45829
|
100 |
val size = peer.getSize()
|
wenzelm@45870
|
101 |
val insets = border.getBorderInsets(this.peer)
|
wenzelm@45829
|
102 |
val w = size.width - insets.left - insets.right
|
wenzelm@45829
|
103 |
val h = size.height - insets.top - insets.bottom
|
wenzelm@45829
|
104 |
var end = size.width - insets.right
|
wenzelm@45738
|
105 |
for {
|
wenzelm@45738
|
106 |
(n, color) <- List(
|
wenzelm@45738
|
107 |
(st.unprocessed, Isabelle_Markup.unprocessed1_color),
|
wenzelm@45739
|
108 |
(st.running, Isabelle_Markup.running_color),
|
wenzelm@45739
|
109 |
(st.failed, Isabelle_Markup.error_color)) }
|
wenzelm@45738
|
110 |
{
|
wenzelm@45738
|
111 |
gfx.setColor(color)
|
wenzelm@45738
|
112 |
val v = (n * w / st.total) max (if (n > 0) 2 else 0)
|
wenzelm@45829
|
113 |
gfx.fillRect(end - v, insets.top, v, h)
|
wenzelm@45738
|
114 |
end -= v
|
wenzelm@45738
|
115 |
}
|
wenzelm@45738
|
116 |
case _ =>
|
wenzelm@45738
|
117 |
}
|
wenzelm@45739
|
118 |
super.paintComponent(gfx)
|
wenzelm@45738
|
119 |
}
|
wenzelm@45738
|
120 |
}
|
wenzelm@45738
|
121 |
|
wenzelm@45871
|
122 |
private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
|
wenzelm@45828
|
123 |
{
|
wenzelm@45871
|
124 |
def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
|
wenzelm@45871
|
125 |
name: Document.Node.Name, index: Int): Component =
|
wenzelm@45828
|
126 |
{
|
wenzelm@45871
|
127 |
val component = Node_Renderer_Component
|
wenzelm@45828
|
128 |
component.node_name = name
|
wenzelm@45870
|
129 |
component.text = name.theory
|
wenzelm@45871
|
130 |
component
|
wenzelm@45828
|
131 |
}
|
wenzelm@45828
|
132 |
}
|
wenzelm@45828
|
133 |
status.renderer = new Node_Renderer
|
wenzelm@45500
|
134 |
|
wenzelm@45506
|
135 |
private def handle_changed(changed_nodes: Set[Document.Node.Name])
|
wenzelm@45500
|
136 |
{
|
wenzelm@45500
|
137 |
Swing_Thread.now {
|
wenzelm@45504
|
138 |
// FIXME correlation to changed_nodes!?
|
wenzelm@45831
|
139 |
val snapshot = Isabelle.session.snapshot()
|
wenzelm@45504
|
140 |
|
wenzelm@45547
|
141 |
var nodes_status1 = nodes_status
|
wenzelm@45547
|
142 |
for {
|
wenzelm@45547
|
143 |
name <- changed_nodes
|
wenzelm@45831
|
144 |
node <- snapshot.version.nodes.get(name)
|
wenzelm@45831
|
145 |
val status = Isar_Document.node_status(snapshot.state, snapshot.version, node)
|
wenzelm@45738
|
146 |
} nodes_status1 += (name -> status)
|
wenzelm@45547
|
147 |
|
wenzelm@45547
|
148 |
if (nodes_status != nodes_status1) {
|
wenzelm@45547
|
149 |
nodes_status = nodes_status1
|
wenzelm@45738
|
150 |
status.listData =
|
wenzelm@45831
|
151 |
snapshot.version.topological_order.filter(
|
wenzelm@45831
|
152 |
(name: Document.Node.Name) => nodes_status.isDefinedAt(name))
|
wenzelm@45500
|
153 |
}
|
wenzelm@45500
|
154 |
}
|
wenzelm@45500
|
155 |
}
|
wenzelm@45500
|
156 |
|
wenzelm@45500
|
157 |
|
wenzelm@39784
|
158 |
/* main actor */
|
wenzelm@39784
|
159 |
|
wenzelm@39784
|
160 |
private val main_actor = actor {
|
wenzelm@39784
|
161 |
loop {
|
wenzelm@39784
|
162 |
react {
|
wenzelm@39853
|
163 |
case result: Isabelle_Process.Result =>
|
wenzelm@39915
|
164 |
if (result.is_syslog)
|
wenzelm@39915
|
165 |
Swing_Thread.now {
|
wenzelm@39919
|
166 |
val text = Isabelle.session.syslog()
|
wenzelm@39916
|
167 |
if (text != syslog.text) {
|
wenzelm@39916
|
168 |
syslog.text = text
|
wenzelm@39916
|
169 |
}
|
wenzelm@39915
|
170 |
}
|
wenzelm@39853
|
171 |
|
wenzelm@39966
|
172 |
case phase: Session.Phase =>
|
wenzelm@39961
|
173 |
Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
|
wenzelm@39925
|
174 |
|
wenzelm@45500
|
175 |
case changed: Session.Commands_Changed => handle_changed(changed.nodes)
|
wenzelm@45500
|
176 |
|
wenzelm@39784
|
177 |
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
|
wenzelm@39784
|
178 |
}
|
wenzelm@39784
|
179 |
}
|
wenzelm@39784
|
180 |
}
|
wenzelm@39784
|
181 |
|
wenzelm@39925
|
182 |
override def init() {
|
wenzelm@45625
|
183 |
Isabelle.session.syslog_messages += main_actor
|
wenzelm@39925
|
184 |
Isabelle.session.phase_changed += main_actor
|
wenzelm@45500
|
185 |
Isabelle.session.commands_changed += main_actor
|
wenzelm@39925
|
186 |
}
|
wenzelm@39925
|
187 |
|
wenzelm@39925
|
188 |
override def exit() {
|
wenzelm@45625
|
189 |
Isabelle.session.syslog_messages -= main_actor
|
wenzelm@39925
|
190 |
Isabelle.session.phase_changed -= main_actor
|
wenzelm@45500
|
191 |
Isabelle.session.commands_changed -= main_actor
|
wenzelm@39925
|
192 |
}
|
wenzelm@39784
|
193 |
}
|