#! /usr/bin/gawk -f
# Last edited on 1999-01-29 18:34:12 by stolfi

BEGIN {
  abort = -1;
  usage = "cleanup-page-descr [-v indent=NUM] < INFILE > OUTFILE";
  if (indent == "") { indent = 3; }
  #
  # Reads a page description file in EVMT format
  # (a bunch of "#" comments).
  # Discards (complaining) non-"#" lines.
  # Discards leading and trailing blank lines.
  # Moves the "Last edited on" line to the end, adds one if missing.
  lastEdit = "";
  discardBlanks = 1;
  nBlanks = 0;
  split("", nsec);
  split("", nlin);
}

(abort >= 0) { exit abort; }

/^[#][#]/ {
  if(! match($0, /^[#][#] *[<]f[0-9][0-9]*[rv]*[0-9]*[>] *[{][$].*[}] *$/))
    { error("bad format of ##-line"); }
  match($0, /[<]f[0-9][0-9]*[rv]*[0-9]*[>]/);
  print; 
  next;
}
  
/^ *$/ { next; }

/^[^#]/ { error("not an #-line"); }

/^[#] *Last edited on/{
  lastEdit = $0; next;
}

/^[#] *$/{
  if (! discardBlanks) { nBlanks++; }
  next;
}

/^[#]/ {
  while (nBlanks > 0) { print "#"; nBlanks--; }
  if(! match($0, /^[#][ ]*/)) { error("duh?"); }
  if (RLENGTH < indent+1) { warning("not enough indentation"); }
  print; discardBlanks=0; next;
}

END {
  print "#";
  if (lastEdit != "") 
    { print lastEdit; }
  else
    { print "# Last edited on DATE TIME by USER"; }
}

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

function warning(msg) {
  printf "line %d: (warning) %s\n", NR, msg >> "/dev/stderr"; 
}