wenzelm@51314
|
1 |
/* Title: Tools/jEdit/src/theories_dockable.scala
|
wenzelm@39784
|
2 |
Author: Makarius
|
wenzelm@39784
|
3 |
|
wenzelm@51314
|
4 |
Dockable window for theories managed by prover.
|
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@54848
|
13 |
import scala.swing.{Button, TextArea, Label, ListView, Alignment,
|
wenzelm@53952
|
14 |
ScrollPane, Component, CheckBox, BorderPanel}
|
wenzelm@54852
|
15 |
import scala.swing.event.{MouseClicked, MouseMoved}
|
wenzelm@39857
|
16 |
|
wenzelm@44400
|
17 |
import java.lang.System
|
wenzelm@54315
|
18 |
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
|
wenzelm@48484
|
19 |
import javax.swing.{JList, BorderFactory}
|
wenzelm@53939
|
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@51314
|
25 |
class Theories_Dockable(view: View, position: String) extends Dockable(view, position)
|
wenzelm@39784
|
26 |
{
|
wenzelm@49036
|
27 |
/* status */
|
wenzelm@39855
|
28 |
|
wenzelm@49036
|
29 |
private val status = new ListView(Nil: List[Document.Node.Name]) {
|
wenzelm@45872
|
30 |
listenTo(mouse.clicks)
|
wenzelm@53954
|
31 |
listenTo(mouse.moves)
|
wenzelm@45872
|
32 |
reactions += {
|
wenzelm@53953
|
33 |
case MouseClicked(_, point, _, clicks, _) =>
|
wenzelm@45872
|
34 |
val index = peer.locationToIndex(point)
|
wenzelm@53954
|
35 |
if (index >= 0) {
|
wenzelm@53954
|
36 |
if (in_checkbox(peer.indexToLocation(index), point)) {
|
wenzelm@53954
|
37 |
if (clicks == 1) {
|
wenzelm@53954
|
38 |
for {
|
wenzelm@53954
|
39 |
buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
|
wenzelm@53954
|
40 |
model <- PIDE.document_model(buffer)
|
wenzelm@53954
|
41 |
} model.node_required = !model.node_required
|
wenzelm@53954
|
42 |
}
|
wenzelm@53953
|
43 |
}
|
wenzelm@54117
|
44 |
else if (clicks == 2) PIDE.editor.goto(view, listData(index).node)
|
wenzelm@53953
|
45 |
}
|
wenzelm@53954
|
46 |
case MouseMoved(_, point, _) =>
|
wenzelm@53954
|
47 |
val index = peer.locationToIndex(point)
|
wenzelm@53954
|
48 |
if (index >= 0 && in_checkbox(peer.indexToLocation(index), point))
|
wenzelm@53954
|
49 |
tooltip = "Mark as required for continuous checking"
|
wenzelm@53954
|
50 |
else
|
wenzelm@53954
|
51 |
tooltip = null
|
wenzelm@45872
|
52 |
}
|
wenzelm@45872
|
53 |
}
|
wenzelm@51265
|
54 |
status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
|
wenzelm@51265
|
55 |
status.peer.setVisibleRowCount(0)
|
wenzelm@45500
|
56 |
status.selection.intervalMode = ListView.IntervalMode.Single
|
wenzelm@45500
|
57 |
|
wenzelm@50053
|
58 |
set_content(new ScrollPane(status))
|
wenzelm@39784
|
59 |
|
wenzelm@39784
|
60 |
|
wenzelm@39857
|
61 |
/* controls */
|
wenzelm@39857
|
62 |
|
wenzelm@51314
|
63 |
def phase_text(phase: Session.Phase): String =
|
wenzelm@51314
|
64 |
"Prover: " + Library.lowercase(phase.toString)
|
wenzelm@51314
|
65 |
|
wenzelm@51314
|
66 |
private val session_phase = new Label(phase_text(PIDE.session.phase))
|
wenzelm@39962
|
67 |
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
|
wenzelm@51314
|
68 |
session_phase.tooltip = "Status of prover session"
|
wenzelm@39925
|
69 |
|
wenzelm@49033
|
70 |
private def handle_phase(phase: Session.Phase)
|
wenzelm@49033
|
71 |
{
|
wenzelm@54314
|
72 |
Swing_Thread.require()
|
wenzelm@54314
|
73 |
session_phase.text = " " + phase_text(phase) + " "
|
wenzelm@49033
|
74 |
}
|
wenzelm@49033
|
75 |
|
wenzelm@54852
|
76 |
private val continuous_checking = new Isabelle.Continuous_Checking
|
wenzelm@55301
|
77 |
continuous_checking.focusable = false
|
wenzelm@45647
|
78 |
|
wenzelm@50261
|
79 |
private val logic = Isabelle_Logic.logic_selector(true)
|
wenzelm@39967
|
80 |
|
wenzelm@45646
|
81 |
private val controls =
|
wenzelm@54848
|
82 |
new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic)
|
wenzelm@39857
|
83 |
add(controls.peer, BorderLayout.NORTH)
|
wenzelm@39857
|
84 |
|
wenzelm@39857
|
85 |
|
wenzelm@45500
|
86 |
/* component state -- owned by Swing thread */
|
wenzelm@45500
|
87 |
|
wenzelm@46587
|
88 |
private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
|
wenzelm@53952
|
89 |
private var nodes_required: Set[Document.Node.Name] = Set.empty
|
wenzelm@45738
|
90 |
|
wenzelm@53952
|
91 |
private def update_nodes_required()
|
wenzelm@53952
|
92 |
{
|
wenzelm@53952
|
93 |
nodes_required = Set.empty
|
wenzelm@53952
|
94 |
for {
|
wenzelm@53952
|
95 |
buffer <- JEdit_Lib.jedit_buffers
|
wenzelm@53952
|
96 |
model <- PIDE.document_model(buffer)
|
wenzelm@53952
|
97 |
if model.node_required
|
wenzelm@54110
|
98 |
} nodes_required += model.node_name
|
wenzelm@53952
|
99 |
}
|
wenzelm@53997
|
100 |
update_nodes_required()
|
wenzelm@53952
|
101 |
|
wenzelm@53954
|
102 |
private def in_checkbox(loc0: Point, p: Point): Boolean =
|
wenzelm@53954
|
103 |
Node_Renderer_Component != null &&
|
wenzelm@53954
|
104 |
(Node_Renderer_Component.checkbox_geometry match {
|
wenzelm@53954
|
105 |
case Some((loc, size)) =>
|
wenzelm@53954
|
106 |
loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
|
wenzelm@53954
|
107 |
loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
|
wenzelm@53954
|
108 |
case None => false
|
wenzelm@53954
|
109 |
})
|
wenzelm@53954
|
110 |
|
wenzelm@53952
|
111 |
private object Node_Renderer_Component extends BorderPanel
|
wenzelm@45738
|
112 |
{
|
wenzelm@45871
|
113 |
opaque = false
|
wenzelm@54313
|
114 |
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
|
wenzelm@45828
|
115 |
|
wenzelm@45828
|
116 |
var node_name = Document.Node.Name.empty
|
wenzelm@53953
|
117 |
|
wenzelm@53953
|
118 |
var checkbox_geometry: Option[(Point, Dimension)] = None
|
wenzelm@53953
|
119 |
val checkbox = new CheckBox {
|
wenzelm@53956
|
120 |
opaque = false
|
wenzelm@53953
|
121 |
override def paintComponent(gfx: Graphics2D)
|
wenzelm@53953
|
122 |
{
|
wenzelm@53953
|
123 |
super.paintComponent(gfx)
|
wenzelm@53953
|
124 |
if (location != null && size != null)
|
wenzelm@53953
|
125 |
checkbox_geometry = Some((location, size))
|
wenzelm@53953
|
126 |
}
|
wenzelm@53953
|
127 |
}
|
wenzelm@53946
|
128 |
|
wenzelm@53952
|
129 |
val label = new Label {
|
wenzelm@53952
|
130 |
opaque = false
|
wenzelm@54313
|
131 |
border = BorderFactory.createEmptyBorder()
|
wenzelm@53952
|
132 |
xAlignment = Alignment.Leading
|
wenzelm@51915
|
133 |
|
wenzelm@53952
|
134 |
override def paintComponent(gfx: Graphics2D)
|
wenzelm@53952
|
135 |
{
|
wenzelm@54315
|
136 |
def paint_segment(x: Int, w: Int, color: Color)
|
wenzelm@54315
|
137 |
{
|
wenzelm@54315
|
138 |
gfx.setColor(color)
|
wenzelm@54315
|
139 |
gfx.fillRect(x, 0, w, size.height)
|
wenzelm@54315
|
140 |
}
|
wenzelm@53952
|
141 |
|
wenzelm@53952
|
142 |
nodes_status.get(node_name) match {
|
wenzelm@53952
|
143 |
case Some(st) if st.total > 0 =>
|
wenzelm@54315
|
144 |
val segments =
|
wenzelm@54315
|
145 |
List(
|
wenzelm@54315
|
146 |
(st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
|
wenzelm@54315
|
147 |
(st.running, PIDE.options.color_value("running_color")),
|
wenzelm@54315
|
148 |
(st.warned, PIDE.options.color_value("warning_color")),
|
wenzelm@54315
|
149 |
(st.failed, PIDE.options.color_value("error_color"))
|
wenzelm@54315
|
150 |
).filter(_._1 > 0)
|
wenzelm@53952
|
151 |
|
wenzelm@54315
|
152 |
(size.width /: segments)({ case (last, (n, color)) =>
|
wenzelm@54315
|
153 |
val w = (n * (size.width - segments.length) / st.total) max 4
|
wenzelm@54315
|
154 |
paint_segment(last - w, w, color)
|
wenzelm@54315
|
155 |
last - w - 1
|
wenzelm@54315
|
156 |
})
|
wenzelm@54315
|
157 |
|
wenzelm@53952
|
158 |
case _ =>
|
wenzelm@54315
|
159 |
paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
|
wenzelm@53952
|
160 |
}
|
wenzelm@53952
|
161 |
super.paintComponent(gfx)
|
wenzelm@45738
|
162 |
}
|
wenzelm@45738
|
163 |
}
|
wenzelm@53952
|
164 |
|
wenzelm@53953
|
165 |
layout(checkbox) = BorderPanel.Position.West
|
wenzelm@53952
|
166 |
layout(label) = BorderPanel.Position.Center
|
wenzelm@45738
|
167 |
}
|
wenzelm@45738
|
168 |
|
wenzelm@45871
|
169 |
private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
|
wenzelm@45828
|
170 |
{
|
wenzelm@45871
|
171 |
def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
|
wenzelm@45871
|
172 |
name: Document.Node.Name, index: Int): Component =
|
wenzelm@45828
|
173 |
{
|
wenzelm@45871
|
174 |
val component = Node_Renderer_Component
|
wenzelm@45828
|
175 |
component.node_name = name
|
wenzelm@53953
|
176 |
component.checkbox.selected = nodes_required.contains(name)
|
wenzelm@53952
|
177 |
component.label.text = name.theory
|
wenzelm@45871
|
178 |
component
|
wenzelm@45828
|
179 |
}
|
wenzelm@45828
|
180 |
}
|
wenzelm@45828
|
181 |
status.renderer = new Node_Renderer
|
wenzelm@45500
|
182 |
|
wenzelm@45882
|
183 |
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
|
wenzelm@45500
|
184 |
{
|
wenzelm@54314
|
185 |
Swing_Thread.require()
|
wenzelm@45504
|
186 |
|
wenzelm@54314
|
187 |
val snapshot = PIDE.session.snapshot()
|
wenzelm@45547
|
188 |
|
wenzelm@54314
|
189 |
val iterator =
|
wenzelm@55904
|
190 |
(restriction match {
|
wenzelm@54314
|
191 |
case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
|
wenzelm@54314
|
192 |
case None => snapshot.version.nodes.entries
|
wenzelm@55904
|
193 |
}).filter(_._1.is_theory)
|
wenzelm@54314
|
194 |
val nodes_status1 =
|
wenzelm@54314
|
195 |
(nodes_status /: iterator)({ case (status, (name, node)) =>
|
wenzelm@54314
|
196 |
if (PIDE.thy_load.loaded_theories(name.theory)) status
|
wenzelm@54314
|
197 |
else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
|
wenzelm@54314
|
198 |
|
wenzelm@54314
|
199 |
if (nodes_status != nodes_status1) {
|
wenzelm@54314
|
200 |
nodes_status = nodes_status1
|
wenzelm@54314
|
201 |
status.listData =
|
wenzelm@54314
|
202 |
snapshot.version.nodes.topological_order.filter(
|
wenzelm@54314
|
203 |
(name: Document.Node.Name) => nodes_status.isDefinedAt(name))
|
wenzelm@45500
|
204 |
}
|
wenzelm@45500
|
205 |
}
|
wenzelm@45500
|
206 |
|
wenzelm@45500
|
207 |
|
wenzelm@39784
|
208 |
/* main actor */
|
wenzelm@39784
|
209 |
|
wenzelm@39784
|
210 |
private val main_actor = actor {
|
wenzelm@39784
|
211 |
loop {
|
wenzelm@39784
|
212 |
react {
|
wenzelm@54314
|
213 |
case phase: Session.Phase =>
|
wenzelm@54314
|
214 |
Swing_Thread.later { handle_phase(phase) }
|
wenzelm@39925
|
215 |
|
wenzelm@53896
|
216 |
case _: Session.Global_Options =>
|
wenzelm@53896
|
217 |
Swing_Thread.later {
|
wenzelm@53944
|
218 |
continuous_checking.load()
|
wenzelm@53896
|
219 |
logic.load ()
|
wenzelm@53952
|
220 |
update_nodes_required()
|
wenzelm@53952
|
221 |
status.repaint()
|
wenzelm@53896
|
222 |
}
|
wenzelm@50262
|
223 |
|
wenzelm@54314
|
224 |
case changed: Session.Commands_Changed =>
|
wenzelm@54314
|
225 |
Swing_Thread.later { handle_update(Some(changed.nodes)) }
|
wenzelm@45500
|
226 |
|
wenzelm@51314
|
227 |
case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
|
wenzelm@39784
|
228 |
}
|
wenzelm@39784
|
229 |
}
|
wenzelm@39784
|
230 |
}
|
wenzelm@39784
|
231 |
|
wenzelm@49033
|
232 |
override def init()
|
wenzelm@49033
|
233 |
{
|
wenzelm@54314
|
234 |
PIDE.session.phase_changed += main_actor
|
wenzelm@51220
|
235 |
PIDE.session.global_options += main_actor
|
wenzelm@54314
|
236 |
PIDE.session.commands_changed += main_actor
|
wenzelm@54314
|
237 |
|
wenzelm@54314
|
238 |
handle_phase(PIDE.session.phase)
|
wenzelm@54314
|
239 |
handle_update()
|
wenzelm@39925
|
240 |
}
|
wenzelm@39925
|
241 |
|
wenzelm@49033
|
242 |
override def exit()
|
wenzelm@49033
|
243 |
{
|
wenzelm@51220
|
244 |
PIDE.session.phase_changed -= main_actor
|
wenzelm@51220
|
245 |
PIDE.session.global_options -= main_actor
|
wenzelm@51220
|
246 |
PIDE.session.commands_changed -= main_actor
|
wenzelm@39925
|
247 |
}
|
wenzelm@39784
|
248 |
}
|