# HG changeset patch # User wenzelm # Date 1375803009 -7200 # Node ID e2d5c3ff5c3f3cd985a0df531b2be7292eb486ca # Parent 91032244e4caded284e4ac844ff3b96b42cf75ab tuned signature; diff -r 91032244e4ca -r e2d5c3ff5c3f src/Tools/jEdit/src/query_operation.scala --- a/src/Tools/jEdit/src/query_operation.scala Mon Aug 05 23:57:29 2013 +0200 +++ b/src/Tools/jEdit/src/query_operation.scala Tue Aug 06 17:30:09 2013 +0200 @@ -34,7 +34,7 @@ private val instance = Document_ID.make().toString - /* status animation */ + /* animation */ private val passive_icon = JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage @@ -43,9 +43,19 @@ JEdit_Lib.load_image_icon(name).getImage) val animation = new Label - val animation_icon = new AnimatedIcon(passive_icon, active_icons.toArray, 10, animation.peer) + private val animation_icon = + new AnimatedIcon(passive_icon, active_icons.toArray, 10, animation.peer) animation.icon = animation_icon + private def animation_rate(rate: Int) + { + animation_icon.stop + if (rate > 0) { + animation_icon.setRate(rate) + animation_icon.start + } + } + /* implicit state -- owned by Swing thread */ @@ -96,7 +106,7 @@ if (!new_output.isEmpty) { current_result = true - animation_icon.stop + animation_rate(0) remove_overlay() PIDE.flush_buffers() } @@ -117,7 +127,7 @@ current_location = None current_query = Nil current_result = false - animation_icon.start + animation_rate(10) snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { case Some(command) => current_location = Some(command)