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