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