display time numerically on tracker line when dragging

jkboyce · Jan 28, 2022 · 8b46eff · 8b46eff
1 parent 15a90b9
commit 8b46eff
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/source/jugglinglab/core/EditLadderDiagram.java b/source/jugglinglab/core/EditLadderDiagram.java
@@ -397,6 +397,7 @@ else if (my > (height-border_top))
                     gui_state = STATE_INACTIVE;
                     if (animator != null)
                         animator.setPaused(anim_paused);
+                    repaint();
                     break;
                 case STATE_POPUP:
                     break;
@@ -1858,6 +1859,10 @@ protected void paintComponent(Graphics gr) {
         // draw the tracker line showing the time
         gr.setColor(Color.red);
         gr.drawLine(0, tracker_y, width, tracker_y);
+        if (gui_state == STATE_MOVING_TRACKER) {
+            gr.drawString(JLFunc.toStringRounded(sim_time, 2) + " s",
+                        width / 2 - 18, tracker_y - 5);
+        }
     }
 
 /*