src/Tools/jEdit/src/process_indicator.scala
changeset 75393 87ebf5a50283
parent 73367 77ef8bef0593
child 75811 74d6d09e1a36
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
    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