author | wenzelm |
Thu, 04 Mar 2021 15:41:46 +0100 | |
changeset 73359 | d8a0e996614b |
parent 73358 | 78aa7846e91f |
child 73361 | ef8c9b3d5355 |
permissions | -rw-r--r-- |
51533 | 1 |
/* Title: Tools/jEdit/src/timing_dockable.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Dockable window for timing information. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
66206
diff
changeset
|
11 |
import isabelle.jedit_base.Dockable |
51533 | 12 |
|
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
53177
diff
changeset
|
13 |
import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField} |
51538 | 14 |
import scala.swing.event.{MouseClicked, ValueChanged} |
51533 | 15 |
|
51536 | 16 |
import java.awt.{BorderLayout, Graphics2D, Insets, Color} |
51533 | 17 |
import javax.swing.{JList, BorderFactory} |
18 |
import javax.swing.border.{BevelBorder, SoftBevelBorder} |
|
19 |
||
20 |
import org.gjt.sp.jedit.{View, jEdit} |
|
21 |
||
22 |
||
23 |
class Timing_Dockable(view: View, position: String) extends Dockable(view, position) |
|
24 |
{ |
|
25 |
/* entry */ |
|
26 |
||
27 |
private object Entry |
|
28 |
{ |
|
29 |
object Ordering extends scala.math.Ordering[Entry] |
|
30 |
{ |
|
31 |
def compare(entry1: Entry, entry2: Entry): Int = |
|
32 |
entry2.timing compare entry1.timing |
|
33 |
} |
|
34 |
||
35 |
object Renderer_Component extends Label |
|
36 |
{ |
|
37 |
opaque = false |
|
38 |
xAlignment = Alignment.Leading |
|
39 |
border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
|
51536 | 40 |
|
41 |
var entry: Entry = null |
|
73340 | 42 |
override def paintComponent(gfx: Graphics2D): Unit = |
51536 | 43 |
{ |
73340 | 44 |
def paint_rectangle(color: Color): Unit = |
51536 | 45 |
{ |
46 |
val size = peer.getSize() |
|
47 |
val insets = border.getBorderInsets(peer) |
|
48 |
val x = insets.left |
|
49 |
val y = insets.top |
|
50 |
val w = size.width - x - insets.right |
|
51 |
val h = size.height - y - insets.bottom |
|
52 |
gfx.setColor(color) |
|
53 |
gfx.fillRect(x, y, w, h) |
|
54 |
} |
|
55 |
||
56 |
entry match { |
|
57 |
case theory_entry: Theory_Entry if theory_entry.current => |
|
58 |
paint_rectangle(view.getTextArea.getPainter.getSelectionColor) |
|
59 |
case _: Command_Entry => |
|
60 |
paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor) |
|
61 |
case _ => |
|
62 |
} |
|
63 |
super.paintComponent(gfx) |
|
64 |
} |
|
51533 | 65 |
} |
66 |
||
67 |
class Renderer extends ListView.Renderer[Entry] |
|
68 |
{ |
|
66191 | 69 |
def componentFor(list: ListView[_ <: Timing_Dockable.this.Entry], |
64442 | 70 |
isSelected: Boolean, focused: Boolean, entry: Entry, index: Int): Component = |
51533 | 71 |
{ |
72 |
val component = Renderer_Component |
|
51536 | 73 |
component.entry = entry |
51534 | 74 |
component.text = entry.print |
51533 | 75 |
component |
76 |
} |
|
77 |
} |
|
78 |
} |
|
79 |
||
51534 | 80 |
private abstract class Entry |
81 |
{ |
|
82 |
def timing: Double |
|
83 |
def print: String |
|
73340 | 84 |
def follow(snapshot: Document.Snapshot): Unit |
51534 | 85 |
} |
86 |
||
51536 | 87 |
private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean) |
88 |
extends Entry |
|
51533 | 89 |
{ |
59735 | 90 |
def print: String = |
91 |
Time.print_seconds(timing) + "s theory " + quote(name.theory) |
|
73340 | 92 |
def follow(snapshot: Document.Snapshot): Unit = |
93 |
PIDE.editor.goto_file(true, view, name.node) |
|
51534 | 94 |
} |
95 |
||
96 |
private case class Command_Entry(command: Command, timing: Double) extends Entry |
|
97 |
{ |
|
59735 | 98 |
def print: String = |
99 |
" " + Time.print_seconds(timing) + "s command " + quote(command.span.name) |
|
73340 | 100 |
def follow(snapshot: Document.Snapshot): Unit = |
101 |
PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) |
|
51533 | 102 |
} |
103 |
||
104 |
||
105 |
/* timing view */ |
|
106 |
||
107 |
private val timing_view = new ListView(Nil: List[Entry]) { |
|
108 |
listenTo(mouse.clicks) |
|
109 |
reactions += { |
|
110 |
case MouseClicked(_, point, _, clicks, _) if clicks == 2 => |
|
111 |
val index = peer.locationToIndex(point) |
|
112 |
if (index >= 0) listData(index).follow(PIDE.session.snapshot()) |
|
113 |
} |
|
114 |
} |
|
115 |
timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP) |
|
116 |
timing_view.peer.setVisibleRowCount(0) |
|
117 |
timing_view.selection.intervalMode = ListView.IntervalMode.Single |
|
118 |
timing_view.renderer = new Entry.Renderer |
|
119 |
||
120 |
set_content(new ScrollPane(timing_view)) |
|
121 |
||
122 |
||
123 |
/* timing threshold */ |
|
124 |
||
125 |
private var timing_threshold = PIDE.options.real("jedit_timing_threshold") |
|
126 |
||
51549 | 127 |
private val threshold_tooltip = "Threshold for timing display (seconds)" |
128 |
||
129 |
private val threshold_label = new Label("Threshold: ") { |
|
130 |
tooltip = threshold_tooltip |
|
131 |
} |
|
51533 | 132 |
|
133 |
private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) { |
|
134 |
reactions += { |
|
51538 | 135 |
case _: ValueChanged => |
51533 | 136 |
text match { |
63805 | 137 |
case Value.Double(x) if x >= 0.0 => timing_threshold = x |
51533 | 138 |
case _ => |
139 |
} |
|
140 |
handle_update() |
|
141 |
} |
|
51549 | 142 |
tooltip = threshold_tooltip |
51538 | 143 |
verifier = ((s: String) => |
63805 | 144 |
s match { case Value.Double(x) => x >= 0.0 case _ => false }) |
51533 | 145 |
} |
146 |
||
66206 | 147 |
private val controls = Wrap_Panel(List(threshold_label, threshold_value)) |
148 |
||
51533 | 149 |
add(controls.peer, BorderLayout.NORTH) |
150 |
||
151 |
||
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
152 |
/* component state -- owned by GUI thread */ |
51533 | 153 |
|
69863 | 154 |
private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing] |
51534 | 155 |
|
156 |
private def make_entries(): List[Entry] = |
|
157 |
{ |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
158 |
GUI_Thread.require {} |
51534 | 159 |
|
160 |
val name = |
|
64882 | 161 |
Document_View.get(view.getTextArea) match { |
51534 | 162 |
case None => Document.Node.Name.empty |
52973 | 163 |
case Some(doc_view) => doc_view.model.node_name |
51534 | 164 |
} |
69863 | 165 |
val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty) |
51534 | 166 |
|
167 |
val theories = |
|
69863 | 168 |
(for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty) |
51536 | 169 |
yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering) |
51534 | 170 |
val commands = |
69863 | 171 |
(for ((command, command_timing) <- timing.command_timings.toList) |
51534 | 172 |
yield Command_Entry(command, command_timing)).sorted(Entry.Ordering) |
173 |
||
51536 | 174 |
theories.flatMap(entry => |
175 |
if (entry.name == name) entry.copy(current = true) :: commands |
|
176 |
else List(entry)) |
|
51534 | 177 |
} |
51533 | 178 |
|
73340 | 179 |
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None): Unit = |
51533 | 180 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
181 |
GUI_Thread.require {} |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
182 |
|
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
183 |
val snapshot = PIDE.session.snapshot() |
51533 | 184 |
|
73358 | 185 |
val nodes_timing1 = |
186 |
(restriction match { |
|
72823 | 187 |
case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name))) |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56208
diff
changeset
|
188 |
case None => snapshot.version.nodes.iterator |
73359 | 189 |
}).foldLeft(nodes_timing) { |
190 |
case (timing1, (name, node)) => |
|
73358 | 191 |
if (PIDE.resources.session_base.loaded_theory(name)) timing1 |
192 |
else { |
|
193 |
val node_timing = |
|
194 |
Document_Status.Overall_Timing.make( |
|
195 |
snapshot.state, snapshot.version, node.commands, threshold = timing_threshold) |
|
196 |
timing1 + (name -> node_timing) |
|
197 |
} |
|
73359 | 198 |
} |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
199 |
nodes_timing = nodes_timing1 |
51533 | 200 |
|
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
201 |
val entries = make_entries() |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
202 |
if (timing_view.listData.toList != entries) timing_view.listData = entries |
51533 | 203 |
} |
204 |
||
205 |
||
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
206 |
/* main */ |
51533 | 207 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
208 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
209 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
210 |
case changed => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
211 |
GUI_Thread.later { handle_update(Some(changed.nodes)) } |
51533 | 212 |
} |
213 |
||
73340 | 214 |
override def init(): Unit = |
51533 | 215 |
{ |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
216 |
PIDE.session.commands_changed += main |
51533 | 217 |
handle_update() |
218 |
} |
|
219 |
||
73340 | 220 |
override def exit(): Unit = |
51533 | 221 |
{ |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
222 |
PIDE.session.commands_changed -= main |
51533 | 223 |
} |
224 |
} |