1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 09 12:29:15 2013 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 09 13:37:51 2013 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4    "src/plugin.scala"
     1.5    "src/pretty_text_area.scala"
     1.6    "src/pretty_tooltip.scala"
     1.7 +  "src/process_indicator.scala"
     1.8    "src/protocol_dockable.scala"
     1.9    "src/query_operation.scala"
    1.10    "src/raw_output_dockable.scala"

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/jEdit/src/process_indicator.scala	Fri Aug 09 13:37:51 2013 +0200
     2.3 @@ -0,0 +1,65 @@
     2.4 +/*  Title:      Tools/jEdit/src/process_indicator.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Process indicator with animated icon.
     2.8 +*/
     2.9 +
    2.10 +package isabelle.jedit
    2.11 +
    2.12 +
    2.13 +import isabelle._
    2.14 +
    2.15 +import java.awt.Image
    2.16 +import java.awt.event.{ActionListener, ActionEvent}
    2.17 +import javax.swing.{ImageIcon, Timer}
    2.18 +import scala.swing.{Label, Component}
    2.19 +
    2.20 +
    2.21 +class Process_Indicator
    2.22 +{
    2.23 +  private val label = new Label
    2.24 +
    2.25 +  private val passive_icon =
    2.26 +    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
    2.27 +  private val active_icons =
    2.28 +    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
    2.29 +      JEdit_Lib.load_image_icon(name).getImage)
    2.30 +
    2.31 +  private val animation = new ImageIcon(passive_icon) {
    2.32 +    private var current_frame = 0
    2.33 +    private val timer =
    2.34 +      new Timer(0, new ActionListener {
    2.35 +        override def actionPerformed(e: ActionEvent) {
    2.36 +          current_frame = (current_frame + 1) % active_icons.length
    2.37 +          setImage(active_icons(current_frame))
    2.38 +          label.repaint
    2.39 +        }
    2.40 +      })
    2.41 +    timer.setRepeats(true)
    2.42 +
    2.43 +    def update(rate: Int)
    2.44 +    {
    2.45 +      if (rate == 0) {
    2.46 +        setImage(passive_icon)
    2.47 +        timer.stop
    2.48 +        label.repaint
    2.49 +      }
    2.50 +      else {
    2.51 +        val delay = 1000 / rate
    2.52 +        timer.setInitialDelay(delay)
    2.53 +        timer.setDelay(delay)
    2.54 +        timer.restart
    2.55 +      }
    2.56 +    }
    2.57 +  }
    2.58 +  label.icon = animation
    2.59 +
    2.60 +  def component: Component = label
    2.61 +
    2.62 +  def update(tip: String, rate: Int)
    2.63 +  {
    2.64 +    label.tooltip = tip
    2.65 +    animation.update(rate)
    2.66 +  }
    2.67 +}
    2.68 +

     3.1 --- a/src/Tools/jEdit/src/query_operation.scala	Fri Aug 09 12:29:15 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/query_operation.scala	Fri Aug 09 13:37:51 2013 +0200
     3.3 @@ -11,10 +11,9 @@
     3.4  import isabelle._
     3.5  
     3.6  import scala.actors.Actor._
     3.7 -import scala.swing.Label
     3.8 +import scala.swing.Component
     3.9  
    3.10  import org.gjt.sp.jedit.View
    3.11 -import org.gjt.sp.jedit.gui.AnimatedIcon
    3.12  
    3.13  
    3.14  object Query_Operation
    3.15 @@ -72,34 +71,20 @@
    3.16    }
    3.17  
    3.18  
    3.19 -  /* animation */
    3.20 +  /* process indicator */
    3.21  
    3.22 -  val animation = new Label
    3.23 +  private val process_indicator = new Process_Indicator
    3.24 +  val animation: Component = process_indicator.component
    3.25  
    3.26 -  private val passive_icon =
    3.27 -    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
    3.28 -  private val active_icons =
    3.29 -    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
    3.30 -      JEdit_Lib.load_image_icon(name).getImage)
    3.31 -
    3.32 -  private val animation_icon =
    3.33 -    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
    3.34 -  animation.icon = animation_icon
    3.35 -
    3.36 -  private def animation_update()
    3.37 +  private def update_process_indicator()
    3.38    {
    3.39 -    animation_icon.stop
    3.40      current_status match {
    3.41        case Status.WAITING =>
    3.42 -        animation.tooltip = "Waiting for evaluation of query context ..."
    3.43 -        animation_icon.setRate(5)
    3.44 -        animation_icon.start
    3.45 +        process_indicator.update("Waiting for evaluation of query context ...", 5)
    3.46        case Status.RUNNING =>
    3.47 -        animation.tooltip = "Running query operation ..."
    3.48 -        animation_icon.setRate(15)
    3.49 -        animation_icon.start
    3.50 +        process_indicator.update("Running query operation ...", 15)
    3.51        case Status.FINISHED =>
    3.52 -        animation.tooltip = null
    3.53 +        process_indicator.update(null, 0)
    3.54      }
    3.55    }
    3.56  
    3.57 @@ -173,7 +158,7 @@
    3.58          }
    3.59          if (current_status != new_status) {
    3.60            current_status = new_status
    3.61 -          animation_update()
    3.62 +          update_process_indicator()
    3.63            if (new_status == Status.FINISHED) {
    3.64              remove_overlay()
    3.65              PIDE.flush_buffers()
    3.66 @@ -207,7 +192,7 @@
    3.67              doc_view.model.insert_overlay(command, operation_name, instance :: query)
    3.68            case None =>
    3.69          }
    3.70 -        animation_update()
    3.71 +        update_process_indicator()
    3.72          PIDE.flush_buffers()
    3.73        case None =>
    3.74      }