#! /bin/bash
# Last edited on 2004-01-20 13:23:34 by stolfi

cmd="${0##*/}"
usage="${cmd} DIR IMG... > MOVIE.gif"

# Reads the images "{IMG}.eps" from directory {DIR}. Converts them to
# images, and turns them into a GIF movie that is written to stdout.

if [ $# -lt 2 ]; then echo "usage: ${usage}"; exit 1; fi

dir="$1"; shift;
imgs=( $* )

temp="/tmp/$$"

# Canvas size in pt:
pgsz=227

# Resolution in dpi:
dpi=200

n=100
frames=( )
for img in ${imgs[@]} ; do 
  frame=${temp}-${n}.ppm
  convert \
    -page "${pgsz}x${pgsz}" \
    -units PixelsPerInch \
    -density "${dpi}x${dpi}" \
    ${dir}/${img}.eps \
    ${frame}
  display -title '%f' ${frame} &
  frames=( ${frames[@]} ${frame} )
  n=$((n + 1))
done

convert ${frames[@]} -delay 50 -loop 20 ${temp}-m.gif
display -delay 1 ${temp}-m.gif
cat ${temp}-m.gif
/bin/rm -f noname.{red,grn,blu} ${temp}-*