#! /usr/bin/gawk -f
# Last edited on 1999-07-11 14:54:30 by stolfi

BEGIN {
  abort = -1;
  if (dir == "") { error("must define \"dir\""); }
  omitcmt = 1;
  file = "";
}

(abort >= 0) { exit abort; }

/^[#][#] *<f[0-9]+[rv][0-9]*>/ {
  match($0, /<f[0-9]+[rv][0-9]*>/);
  fnum = substr($0, RSTART+1, RLENGTH-2);
  file = (dir "/" fnum);
  print file > "/dev/stderr";
  omitcmt = 0;
  next;
}

/^[#][#]/ {
  print $0 > "/dev/stderr";
  omitcmt = 0;
  next;
}

/^[#] Last edited/ { next; }

/^[#] *Description:/ { omitcmt = 1; next; }

/^[#] *Comments:/ { omitcmt = 1; next; }

/^[#] *References:/ { omitcmt = 1; next; }

/^[#]/ { 
  if (omitcmt) { next; } 
}

// { 
  if (file == "") { next; }
  print $0 > file; 
  next;
}


function error(msg)
{
  printf "line %d: %s\n", NR, msg > "/dev/stderr";
  abort = 1; exit 1;
}