|
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 |
|
12 import scala.actors.Actor._ |
|
13 import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField} |
|
14 import scala.swing.event.{EditDone, MouseClicked} |
|
15 |
|
16 import java.lang.System |
|
17 import java.awt.{BorderLayout, Graphics2D, Insets} |
|
18 import javax.swing.{JList, BorderFactory} |
|
19 import javax.swing.border.{BevelBorder, SoftBevelBorder} |
|
20 |
|
21 import org.gjt.sp.jedit.{View, jEdit} |
|
22 |
|
23 |
|
24 class Timing_Dockable(view: View, position: String) extends Dockable(view, position) |
|
25 { |
|
26 /* entry */ |
|
27 |
|
28 private object Entry |
|
29 { |
|
30 object Ordering extends scala.math.Ordering[Entry] |
|
31 { |
|
32 def compare(entry1: Entry, entry2: Entry): Int = |
|
33 entry2.timing compare entry1.timing |
|
34 } |
|
35 |
|
36 object Renderer_Component extends Label |
|
37 { |
|
38 opaque = false |
|
39 xAlignment = Alignment.Leading |
|
40 border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
|
41 } |
|
42 |
|
43 class Renderer extends ListView.Renderer[Entry] |
|
44 { |
|
45 def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean, |
|
46 entry: Entry, index: Int): Component = |
|
47 { |
|
48 val component = Renderer_Component |
|
49 component.text = Time.print_seconds(entry.timing) + "s " + entry.command.name |
|
50 component |
|
51 } |
|
52 } |
|
53 } |
|
54 |
|
55 private case class Entry(command: Command, timing: Double) |
|
56 { |
|
57 def follow(snapshot: Document.Snapshot) |
|
58 { |
|
59 val node = snapshot.version.nodes(command.node_name) |
|
60 if (node.commands.contains(command)) { |
|
61 val sources = node.commands.iterator.takeWhile(_ != command).map(_.source) |
|
62 val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) |
|
63 Hyperlink(command.node_name.node, line, column).follow(view) |
|
64 } |
|
65 } |
|
66 } |
|
67 |
|
68 |
|
69 /* timing view */ |
|
70 |
|
71 private val timing_view = new ListView(Nil: List[Entry]) { |
|
72 listenTo(mouse.clicks) |
|
73 reactions += { |
|
74 case MouseClicked(_, point, _, clicks, _) if clicks == 2 => |
|
75 val index = peer.locationToIndex(point) |
|
76 if (index >= 0) listData(index).follow(PIDE.session.snapshot()) |
|
77 } |
|
78 } |
|
79 timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP) |
|
80 timing_view.peer.setVisibleRowCount(0) |
|
81 timing_view.selection.intervalMode = ListView.IntervalMode.Single |
|
82 timing_view.renderer = new Entry.Renderer |
|
83 |
|
84 set_content(new ScrollPane(timing_view)) |
|
85 |
|
86 |
|
87 /* timing threshold */ |
|
88 |
|
89 private var timing_threshold = PIDE.options.real("jedit_timing_threshold") |
|
90 |
|
91 private val threshold_label = new Label("Timing threshold: ") |
|
92 |
|
93 private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) { |
|
94 reactions += { |
|
95 case EditDone(_) => |
|
96 text match { |
|
97 case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x |
|
98 case _ => |
|
99 } |
|
100 text = Time.print_seconds(timing_threshold) |
|
101 handle_update() |
|
102 } |
|
103 tooltip = "Threshold for timing display (seconds)" |
|
104 } |
|
105 |
|
106 private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value) |
|
107 add(controls.peer, BorderLayout.NORTH) |
|
108 |
|
109 |
|
110 /* component state -- owned by Swing thread */ |
|
111 |
|
112 private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing] |
|
113 private var current_name = Document.Node.Name.empty |
|
114 private var current_timing = Protocol.empty_node_timing |
|
115 |
|
116 private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) |
|
117 { |
|
118 Swing_Thread.now { |
|
119 val snapshot = PIDE.session.snapshot() |
|
120 |
|
121 val iterator = |
|
122 restriction match { |
|
123 case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name))) |
|
124 case None => snapshot.version.nodes.entries |
|
125 } |
|
126 val nodes_timing1 = |
|
127 (nodes_timing /: iterator)({ case (timing1, (name, node)) => |
|
128 if (PIDE.thy_load.loaded_theories(name.theory)) timing1 |
|
129 else { |
|
130 val node_timing = |
|
131 Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold) |
|
132 timing1 + (name -> node_timing) |
|
133 } |
|
134 }) |
|
135 nodes_timing = nodes_timing1 |
|
136 |
|
137 Document_View(view.getTextArea) match { |
|
138 case Some(doc_view) => |
|
139 val name = doc_view.model.name |
|
140 val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing |
|
141 if (current_name != name || current_timing != timing) { |
|
142 current_name = name |
|
143 current_timing = timing |
|
144 timing_view.listData = |
|
145 timing.commands.toList.map(p => Entry(p._1, p._2)).sorted(Entry.Ordering) |
|
146 } |
|
147 case None => |
|
148 } |
|
149 } |
|
150 } |
|
151 |
|
152 |
|
153 /* main actor */ |
|
154 |
|
155 private val main_actor = actor { |
|
156 loop { |
|
157 react { |
|
158 case changed: Session.Commands_Changed => handle_update(Some(changed.nodes)) |
|
159 |
|
160 case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad) |
|
161 } |
|
162 } |
|
163 } |
|
164 |
|
165 override def init() |
|
166 { |
|
167 PIDE.session.commands_changed += main_actor |
|
168 handle_update() |
|
169 } |
|
170 |
|
171 override def exit() |
|
172 { |
|
173 PIDE.session.commands_changed -= main_actor |
|
174 } |
|
175 } |