saver_mplayer, saver_mpv: make video file list configurable.

Also, always run the player with a playlist of 256 videos; this strikes a
balance between having too many pauses between videos while not eating
too much memory in the player.

Replaces pull request #56.