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