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