author | wenzelm |
Wed, 23 Apr 2014 11:40:42 +0200 | |
changeset 56666 | 229309cbc508 |
parent 52934 | bfb6873df88e |
child 73340 | 0ffcad1f6130 |
permissions | -rw-r--r-- |
52934
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/process_indicator.scala |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
3 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
4 |
Process indicator with animated icon. |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
6 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
8 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
9 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
11 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
12 |
import java.awt.Image |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
13 |
import java.awt.event.{ActionListener, ActionEvent} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
14 |
import javax.swing.{ImageIcon, Timer} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
15 |
import scala.swing.{Label, Component} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
16 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
17 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
18 |
class Process_Indicator |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
19 |
{ |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
20 |
private val label = new Label |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
21 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
22 |
private val passive_icon = |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
23 |
JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
24 |
private val active_icons = |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
25 |
space_explode(':', PIDE.options.string("process_active_icons")).map(name => |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
26 |
JEdit_Lib.load_image_icon(name).getImage) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
27 |
|
56666
229309cbc508
avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents:
52934
diff
changeset
|
28 |
private class Animation extends ImageIcon(passive_icon) |
229309cbc508
avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents:
52934
diff
changeset
|
29 |
{ |
52934
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
30 |
private var current_frame = 0 |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
31 |
private val timer = |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
32 |
new Timer(0, new ActionListener { |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
33 |
override def actionPerformed(e: ActionEvent) { |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
34 |
current_frame = (current_frame + 1) % active_icons.length |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
35 |
setImage(active_icons(current_frame)) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
36 |
label.repaint |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
37 |
} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
38 |
}) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
39 |
timer.setRepeats(true) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
40 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
41 |
def update(rate: Int) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
42 |
{ |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
43 |
if (rate == 0) { |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
44 |
setImage(passive_icon) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
45 |
timer.stop |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
46 |
label.repaint |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
47 |
} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
48 |
else { |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
49 |
val delay = 1000 / rate |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
50 |
timer.setInitialDelay(delay) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
51 |
timer.setDelay(delay) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
52 |
timer.restart |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
53 |
} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
54 |
} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
55 |
} |
56666
229309cbc508
avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents:
52934
diff
changeset
|
56 |
|
229309cbc508
avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents:
52934
diff
changeset
|
57 |
private val animation = new Animation |
52934
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
58 |
label.icon = animation |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
59 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
60 |
def component: Component = label |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
61 |
|
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
62 |
def update(tip: String, rate: Int) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
63 |
{ |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
64 |
label.tooltip = tip |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
65 |
animation.update(rate) |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
66 |
} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
67 |
} |
bfb6873df88e
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff
changeset
|
68 |