#! /bin/csh -f
# Last edited on 2000-07-10 08:01:50 by stolfi

set usage = "$0 [-v VAR=VALUE]... PAGES"

# Makes an index for the colorized files pages-html/PAGE.html
# where PAGE is each of the PAGES

set vars = ( )

while ( ( $#argv > 0 ) && ( "x$1" =~ x-* ) )
  if ( ( $#argv >= 2 ) && ( "x$1" == "x-v" ) ) then
    set vars = ( ${vars} "$1" "$2" ); shift; shift
  else
    echo "usage: ${usage}"; exit 1
  endif
end

set user = "${USER}"
set date = "`date +'%Y-%m-%d %H:%M:%S'`"

set hdir = "pages-html"
set ifile = "${hdir}/index.html"

/bin/rm -f ${ifile}

set secs = ( $* ) 

cat page-index-header.html \
  | replace-html-vars \
      ${vars} \
      -v user="${user}" -v date="${date}" \
  > ${ifile}

echo "<pre>" >> ${ifile}
describe-word-equivalence ${vars} >> ${ifile}
echo "</pre>" >> ${ifile}

echo 

foreach sec ( ${secs} ) 
  echo "<h3>${sec}<h3>" >> ${ifile}
  echo "<b><tt>" >> ${ifile}
  foreach fnum ( `cat sections-fnums/${sec}.fnums` )
    echo '[<a href="'"${fnum}.html"'">'"${fnum}"'</a>] ' >> ${ifile}
  end
  echo "</tt></b>" >> ${ifile}
end

cat page-trailer.html \
  | replace-html-vars \
      ${vars} \
      -v user="${user}" -v date="${date}" \
  >> ${ifile}