src/Tools/jEdit/src/process_indicator.scala
author wenzelm
Thu, 20 Feb 2014 16:00:37 +0100
changeset 55620 19dffae33cde
parent 52934 bfb6873df88e
child 56666 229309cbc508
permissions -rw-r--r--
cumulate/select wrt. precise elements guard; tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    28
  private val animation = new ImageIcon(passive_icon) {
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    29
    private var current_frame = 0
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    30
    private val timer =
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    31
      new Timer(0, new ActionListener {
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    32
        override def actionPerformed(e: ActionEvent) {
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    33
          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
    34
          setImage(active_icons(current_frame))
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    35
          label.repaint
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    36
        }
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
    timer.setRepeats(true)
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    39
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    40
    def update(rate: Int)
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    41
    {
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    42
      if (rate == 0) {
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    43
        setImage(passive_icon)
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    44
        timer.stop
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    45
        label.repaint
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    46
      }
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    47
      else {
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    48
        val delay = 1000 / rate
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    49
        timer.setInitialDelay(delay)
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    50
        timer.setDelay(delay)
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    51
        timer.restart
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    52
      }
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
  label.icon = animation
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    56
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    57
  def component: Component = label
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    58
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    59
  def update(tip: String, rate: Int)
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    60
  {
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    61
    label.tooltip = tip
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    62
    animation.update(rate)
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
}
bfb6873df88e separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
wenzelm
parents:
diff changeset
    65