#! /bin/csh -f 
# Last edited on 1998-12-27 22:09:22 by stolfi

# Removes HTML formatting from takeshi's file

cat \
  | tr -d '\015' \
  | sed \
     -e 's@ @_@g' \
     -e 's@<FONT [^<>]*>@@g' \
     -e 's@</FONT>@@g' \
     -e 's@<B>[_ ]*\(f[a-z0-9]*\)[,a-z0-9]*[_ ]*</B>@## \1@g' \
     -e 's/</@</g' \
     -e 's/>/>@/g' \
  | tr '@' '\012' \
  | gawk '/<[^>]*$/{printf "%s", $0; next;} /./{print;}' \
  | gawk '/<[^>]*$/{printf "%s", $0; next;} /./{print;}' \
  | sed \
     -e '/<TABLE/,/<\/TABLE/d' \
     -e '/<FONT/d' \
     -e '/FONT>/d' \
     -e '/<HEAD/,/<\/HEAD/d' \
     -e '/<BODY/d' \
     -e '/BODY>/d' \
     -e '/<HTML/d' \
     -e '/HTML>/d' \
     -e 's@<HR [^<>]*>@@g' \
     -e 's/^[ ]*//' \
     -e 's/[ ]*$//' \
     -e 's/^_$//' \
  | egrep -v '^[ ]*$' \
  | html-to-iso