1/* Title: Tools/jEdit/src/theories_dockable.scala 2 Author: Makarius 3 4Dockable window for theories managed by prover. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11import isabelle.jedit_base.Dockable 12 13import scala.swing.{Button, TextArea, Label, ListView, Alignment, 14 ScrollPane, Component, CheckBox, BorderPanel} 15import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved} 16 17import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} 18import javax.swing.{JList, BorderFactory, UIManager} 19import javax.swing.border.{BevelBorder, SoftBevelBorder} 20 21import org.gjt.sp.jedit.{View, jEdit} 22 23 24class Theories_Dockable(view: View, position: String) extends Dockable(view, position) 25{ 26 /* status */ 27 28 private val status = new ListView(Nil: List[Document.Node.Name]) { 29 background = 30 { 31 // enforce default value 32 val c = UIManager.getDefaults.getColor("Panel.background") 33 new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) 34 } 35 listenTo(mouse.clicks) 36 listenTo(mouse.moves) 37 reactions += { 38 case MouseClicked(_, point, _, clicks, _) => 39 val index = peer.locationToIndex(point) 40 if (index >= 0) { 41 if (in_checkbox(peer.indexToLocation(index), point)) { 42 if (clicks == 1) Document_Model.node_required(listData(index), toggle = true) 43 } 44 else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) 45 } 46 case MouseMoved(_, point, _) => 47 val index = peer.locationToIndex(point) 48 val index_location = peer.indexToLocation(index) 49 if (index >= 0 && in_checkbox(index_location, point)) 50 tooltip = "Mark as required for continuous checking" 51 else if (index >= 0 && in_label(index_location, point)) { 52 val name = listData(index) 53 val st = overall_node_status(name) 54 tooltip = 55 "theory " + quote(name.theory) + 56 (if (st == Overall_Node_Status.ok) "" else " (" + st + ")") 57 } 58 else tooltip = null 59 } 60 } 61 status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) 62 status.peer.setVisibleRowCount(0) 63 status.selection.intervalMode = ListView.IntervalMode.Single 64 65 set_content(new ScrollPane(status)) 66 67 68 /* controls */ 69 70 def phase_text(phase: Session.Phase): String = "Prover: " + phase.print 71 72 private val session_phase = new Label(phase_text(PIDE.session.phase)) 73 session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) 74 session_phase.tooltip = "Status of prover session" 75 76 private def handle_phase(phase: Session.Phase) 77 { 78 GUI_Thread.require {} 79 session_phase.text = " " + phase_text(phase) + " " 80 } 81 82 private val purge = new Button("Purge") { 83 tooltip = "Restrict document model to theories required for open editor buffers" 84 reactions += { case ButtonClicked(_) => PIDE.editor.purge() } 85 } 86 87 private val continuous_checking = new Isabelle.Continuous_Checking 88 continuous_checking.focusable = false 89 90 private val logic = JEdit_Sessions.logic_selector(PIDE.options, true) 91 92 private val controls = 93 Wrap_Panel(List(purge, continuous_checking, session_phase, logic)) 94 95 add(controls.peer, BorderLayout.NORTH) 96 97 98 /* component state -- owned by GUI thread */ 99 100 private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty 101 private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes() 102 103 private object Overall_Node_Status extends Enumeration 104 { 105 val ok, failed, pending = Value 106 } 107 108 private def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value = 109 nodes_status.get(name) match { 110 case Some(st) if st.consolidated => 111 if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed 112 case _ => Overall_Node_Status.pending 113 } 114 115 private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean = 116 geometry match { 117 case Some((loc, size)) => 118 loc0.x + loc.x <= p.x && p.x < loc0.x + size.width && 119 loc0.y + loc.y <= p.y && p.y < loc0.y + size.height 120 case None => false 121 } 122 123 private def in_checkbox(loc0: Point, p: Point): Boolean = 124 Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p) 125 126 private def in_label(loc0: Point, p: Point): Boolean = 127 Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p) 128 129 130 private object Node_Renderer_Component extends BorderPanel 131 { 132 opaque = true 133 border = BorderFactory.createEmptyBorder(2, 2, 2, 2) 134 135 var node_name = Document.Node.Name.empty 136 137 var checkbox_geometry: Option[(Point, Dimension)] = None 138 val checkbox = new CheckBox { 139 opaque = false 140 override def paintComponent(gfx: Graphics2D) 141 { 142 super.paintComponent(gfx) 143 if (location != null && size != null) 144 checkbox_geometry = Some((location, size)) 145 } 146 } 147 148 var label_geometry: Option[(Point, Dimension)] = None 149 val label = new Label { 150 background = view.getTextArea.getPainter.getBackground 151 foreground = view.getTextArea.getPainter.getForeground 152 opaque = false 153 xAlignment = Alignment.Leading 154 155 override def paintComponent(gfx: Graphics2D) 156 { 157 def paint_segment(x: Int, w: Int, color: Color) 158 { 159 gfx.setColor(color) 160 gfx.fillRect(x, 0, w, size.height) 161 } 162 163 paint_segment(0, size.width, background) 164 nodes_status.get(node_name) match { 165 case Some(st) if st.total > 0 => 166 val segments = 167 List( 168 (st.unprocessed, PIDE.options.color_value("unprocessed1_color")), 169 (st.running, PIDE.options.color_value("running_color")), 170 (st.warned, PIDE.options.color_value("warning_color")), 171 (st.failed, PIDE.options.color_value("error_color")) 172 ).filter(_._1 > 0) 173 174 ((size.width - 2) /: segments)({ case (last, (n, color)) => 175 val w = (n * ((size.width - 4) - segments.length) / st.total) max 4 176 paint_segment(last - w, w, color) 177 last - w - 1 178 }) 179 180 case _ => 181 paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) 182 } 183 super.paintComponent(gfx) 184 185 if (location != null && size != null) 186 label_geometry = Some((location, size)) 187 } 188 } 189 190 def label_border(name: Document.Node.Name) 191 { 192 val status = overall_node_status(name) 193 val color = 194 if (status == Overall_Node_Status.failed) PIDE.options.color_value("error_color") 195 else label.foreground 196 val thickness1 = if (status == Overall_Node_Status.pending) 1 else 2 197 val thickness2 = 3 - thickness1 198 199 label.border = 200 BorderFactory.createCompoundBorder( 201 BorderFactory.createLineBorder(color, thickness1), 202 BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2)) 203 } 204 205 layout(checkbox) = BorderPanel.Position.West 206 layout(label) = BorderPanel.Position.Center 207 } 208 209 private class Node_Renderer extends ListView.Renderer[Document.Node.Name] 210 { 211 def componentFor(list: ListView[_ <: isabelle.Document.Node.Name], isSelected: Boolean, 212 focused: Boolean, name: Document.Node.Name, index: Int): Component = 213 { 214 val component = Node_Renderer_Component 215 component.node_name = name 216 component.checkbox.selected = nodes_required.contains(name) 217 component.label_border(name) 218 component.label.text = name.theory_base_name 219 component 220 } 221 } 222 status.renderer = new Node_Renderer 223 224 private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) 225 { 226 GUI_Thread.require {} 227 228 val snapshot = PIDE.session.snapshot() 229 val nodes = snapshot.version.nodes 230 231 val nodes_status1 = 232 (nodes_status /: (restriction.getOrElse(nodes.domain).iterator))( 233 { case (status, name) => 234 if (PIDE.resources.is_hidden(name) || 235 PIDE.resources.session_base.loaded_theory(name) || 236 nodes(name).is_empty) status 237 else { 238 val st = Protocol.node_status(snapshot.state, snapshot.version, name) 239 status + (name -> st) 240 } 241 }) 242 243 val nodes_status2 = 244 nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_suppressed(_)) 245 246 if (nodes_status != nodes_status2) { 247 nodes_status = nodes_status2 248 status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_)) 249 } 250 } 251 252 253 /* main */ 254 255 private val main = 256 Session.Consumer[Any](getClass.getName) { 257 case phase: Session.Phase => 258 GUI_Thread.later { handle_phase(phase) } 259 260 case _: Session.Global_Options => 261 GUI_Thread.later { 262 continuous_checking.load() 263 logic.load () 264 nodes_required = Document_Model.required_nodes() 265 status.repaint() 266 } 267 268 case changed: Session.Commands_Changed => 269 GUI_Thread.later { handle_update(Some(changed.nodes)) } 270 } 271 272 override def init() 273 { 274 PIDE.session.phase_changed += main 275 PIDE.session.global_options += main 276 PIDE.session.commands_changed += main 277 278 handle_phase(PIDE.session.phase) 279 handle_update() 280 } 281 282 override def exit() 283 { 284 PIDE.session.phase_changed -= main 285 PIDE.session.global_options -= main 286 PIDE.session.commands_changed -= main 287 } 288} 289