lib 1001094 // JavaLayer 1.0.1

import javazoom.jl.player.*;

static void playMp3_javaSound(File mp3) ctex {
  FileInputStream fis = new FileInputStream(mp3);
  Player player = new Player(fis);
  player.play();
  repeat with ms sleep 10 {
    if (player.isComplete()) break;
  }
  player.close();
  fis.close();
}

Began life as a copy of #1001267