+ c.layout();
+ }
+
+ private void updatePausedState()
+ {
+ setPauseText(pauseButton, false);
+ if (exec != null)
+ if (pauseButton.getSelection())
+ exec.unpauseLiveExecution();
+ else
+ exec.pauseLiveExecution();
+ }
+
+ private void updateSpeedFactorFromScale()
+ {
+ double factor = Math.pow(SIM_SPEED_SCALE_STEP_FACTOR, simSpeedScale.getSelection() - SIM_SPEED_SCALE_STEPS);
+ simSpeedInput.setValue(factor);
+ if (exec != null)
+ exec.setSpeedFactor(factor);
+ }
+
+ private void updateSpeedFactorFromInput(double factor)
+ {
+ double factorCheckedFor0;
+ if (factor != 0)
+ factorCheckedFor0 = factor;
+ else
+ {
+ factorCheckedFor0 = Math.pow(10, -simSpeedInput.getPrecision());
+ simSpeedInput.setValue(factorCheckedFor0);
+ }
+ int closestScalePos = (int) Math.round(Math.log(factorCheckedFor0) / SIM_SPEED_SCALE_STEP_FACTOR_LOG + SIM_SPEED_SCALE_STEPS);
+ simSpeedScale.setSelection(Math.min(Math.max(closestScalePos, 0), SIM_SPEED_SCALE_STEPS));
+ if (exec != null)
+ exec.setSpeedFactor(factorCheckedFor0);
+ }