author | wenzelm |
Fri, 25 Apr 2014 12:51:08 +0200 | |
changeset 56715 | 52125652e82a |
parent 56662 | f373fb77e0a4 |
child 57612 | 990ffb84489b |
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 |
{ |
|
68 |
def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean, |
|
69 |
entry: Entry, index: Int): Component = |
|
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 |
{ |
51534 | 89 |
def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory) |
55877 | 90 |
def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) } |
51534 | 91 |
} |
92 |
||
93 |
private case class Command_Entry(command: Command, timing: Double) extends Entry |
|
94 |
{ |
|
95 |
def print: String = " " + Time.print_seconds(timing) + "s command " + quote(command.name) |
|
51533 | 96 |
def follow(snapshot: Document.Snapshot) |
52980 | 97 |
{ PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) } |
51533 | 98 |
} |
99 |
||
100 |
||
101 |
/* timing view */ |
|
102 |
||
103 |
private val timing_view = new ListView(Nil: List[Entry]) { |
|
104 |
listenTo(mouse.clicks) |
|
105 |
reactions += { |
|
106 |
case MouseClicked(_, point, _, clicks, _) if clicks == 2 => |
|
107 |
val index = peer.locationToIndex(point) |
|
108 |
if (index >= 0) listData(index).follow(PIDE.session.snapshot()) |
|
109 |
} |
|
110 |
} |
|
111 |
timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP) |
|
112 |
timing_view.peer.setVisibleRowCount(0) |
|
113 |
timing_view.selection.intervalMode = ListView.IntervalMode.Single |
|
114 |
timing_view.renderer = new Entry.Renderer |
|
115 |
||
116 |
set_content(new ScrollPane(timing_view)) |
|
117 |
||
118 |
||
119 |
/* timing threshold */ |
|
120 |
||
121 |
private var timing_threshold = PIDE.options.real("jedit_timing_threshold") |
|
122 |
||
51549 | 123 |
private val threshold_tooltip = "Threshold for timing display (seconds)" |
124 |
||
125 |
private val threshold_label = new Label("Threshold: ") { |
|
126 |
tooltip = threshold_tooltip |
|
127 |
} |
|
51533 | 128 |
|
129 |
private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) { |
|
130 |
reactions += { |
|
51538 | 131 |
case _: ValueChanged => |
51533 | 132 |
text match { |
133 |
case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x |
|
134 |
case _ => |
|
135 |
} |
|
136 |
handle_update() |
|
137 |
} |
|
51549 | 138 |
tooltip = threshold_tooltip |
51538 | 139 |
verifier = ((s: String) => |
140 |
s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false }) |
|
51533 | 141 |
} |
142 |
||
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
53177
diff
changeset
|
143 |
private val controls = |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
53177
diff
changeset
|
144 |
new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value) |
51533 | 145 |
add(controls.peer, BorderLayout.NORTH) |
146 |
||
147 |
||
148 |
/* component state -- owned by Swing thread */ |
|
149 |
||
150 |
private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing] |
|
51534 | 151 |
|
152 |
private def make_entries(): List[Entry] = |
|
153 |
{ |
|
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56372
diff
changeset
|
154 |
Swing_Thread.require {} |
51534 | 155 |
|
156 |
val name = |
|
157 |
Document_View(view.getTextArea) match { |
|
158 |
case None => Document.Node.Name.empty |
|
52973 | 159 |
case Some(doc_view) => doc_view.model.node_name |
51534 | 160 |
} |
52888 | 161 |
val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing) |
51534 | 162 |
|
163 |
val theories = |
|
51536 | 164 |
(for ((node_name, node_timing) <- nodes_timing.toList if !node_timing.commands.isEmpty) |
165 |
yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering) |
|
51534 | 166 |
val commands = |
167 |
(for ((command, command_timing) <- timing.commands.toList) |
|
168 |
yield Command_Entry(command, command_timing)).sorted(Entry.Ordering) |
|
169 |
||
51536 | 170 |
theories.flatMap(entry => |
171 |
if (entry.name == name) entry.copy(current = true) :: commands |
|
172 |
else List(entry)) |
|
51534 | 173 |
} |
51533 | 174 |
|
175 |
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) |
|
176 |
{ |
|
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56372
diff
changeset
|
177 |
Swing_Thread.require {} |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
178 |
|
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
179 |
val snapshot = PIDE.session.snapshot() |
51533 | 180 |
|
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
181 |
val iterator = |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
182 |
restriction match { |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
183 |
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
|
184 |
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
|
185 |
} |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
186 |
val nodes_timing1 = |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
187 |
(nodes_timing /: iterator)({ case (timing1, (name, node)) => |
56208 | 188 |
if (PIDE.resources.loaded_theories(name.theory)) timing1 |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
189 |
else { |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
190 |
val node_timing = |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
191 |
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
|
192 |
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
|
193 |
} |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
194 |
}) |
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
195 |
nodes_timing = nodes_timing1 |
51533 | 196 |
|
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52980
diff
changeset
|
197 |
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
|
198 |
if (timing_view.listData.toList != entries) timing_view.listData = entries |
51533 | 199 |
} |
200 |
||
201 |
||
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
202 |
/* main */ |
51533 | 203 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
204 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
205 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
206 |
case changed => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
207 |
Swing_Thread.later { handle_update(Some(changed.nodes)) } |
51533 | 208 |
} |
209 |
||
210 |
override def init() |
|
211 |
{ |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
212 |
PIDE.session.commands_changed += main |
51533 | 213 |
handle_update() |
214 |
} |
|
215 |
||
216 |
override def exit() |
|
217 |
{ |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
218 |
PIDE.session.commands_changed -= main |
51533 | 219 |
} |
220 |
} |