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