13 import java.awt.event.{ActionListener, ActionEvent} |
13 import java.awt.event.{ActionListener, ActionEvent} |
14 import javax.swing.{ImageIcon, Timer} |
14 import javax.swing.{ImageIcon, Timer} |
15 import scala.swing.{Label, Component} |
15 import scala.swing.{Label, Component} |
16 |
16 |
17 |
17 |
18 class Process_Indicator |
18 class Process_Indicator { |
19 { |
|
20 private val label = new Label |
19 private val label = new Label |
21 |
20 |
22 private val passive_icon = |
21 private val passive_icon = |
23 JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage |
22 JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage |
24 private val active_icons = |
23 private val active_icons = |
25 space_explode(':', PIDE.options.string("process_active_icons")).map(name => |
24 space_explode(':', PIDE.options.string("process_active_icons")).map(name => |
26 JEdit_Lib.load_image_icon(name).getImage) |
25 JEdit_Lib.load_image_icon(name).getImage) |
27 |
26 |
28 private class Animation extends ImageIcon(passive_icon) |
27 private class Animation extends ImageIcon(passive_icon) { |
29 { |
|
30 private var current_frame = 0 |
28 private var current_frame = 0 |
31 private val timer = |
29 private val timer = |
32 new Timer(0, new ActionListener { |
30 new Timer(0, new ActionListener { |
33 override def actionPerformed(e: ActionEvent): Unit = |
31 override def actionPerformed(e: ActionEvent): Unit = { |
34 { |
|
35 current_frame = (current_frame + 1) % active_icons.length |
32 current_frame = (current_frame + 1) % active_icons.length |
36 setImage(active_icons(current_frame)) |
33 setImage(active_icons(current_frame)) |
37 label.repaint() |
34 label.repaint() |
38 } |
35 } |
39 }) |
36 }) |
40 timer.setRepeats(true) |
37 timer.setRepeats(true) |
41 |
38 |
42 def update(rate: Int): Unit = |
39 def update(rate: Int): Unit = { |
43 { |
|
44 if (rate == 0) { |
40 if (rate == 0) { |
45 setImage(passive_icon) |
41 setImage(passive_icon) |
46 timer.stop |
42 timer.stop |
47 label.repaint() |
43 label.repaint() |
48 } |
44 } |
58 private val animation = new Animation |
54 private val animation = new Animation |
59 label.icon = animation |
55 label.icon = animation |
60 |
56 |
61 def component: Component = label |
57 def component: Component = label |
62 |
58 |
63 def update(tip: String, rate: Int): Unit = |
59 def update(tip: String, rate: Int): Unit = { |
64 { |
|
65 label.tooltip = tip |
60 label.tooltip = tip |
66 animation.update(rate) |
61 animation.update(rate) |
67 } |
62 } |
68 } |
63 } |
69 |
64 |