#!/usr/bin/awk -f

/^@{/ { protect=1; print "%    \\begin{macrocode}"; next }
/^}@/ { protect=0; print "%    \\end{macrocode}"; next }
/^#{/ { protect=1; next }
/^}#/ { protect=0; next }
{ if (protect) { print; next }
  sub(/~.*/,"",$0);
  gsub(/!{/,"\\iffalse",$0);
  gsub(/}!/,"\\fi",$0);
  if (!match($0, /^[[:blank:]]*$/)) print "%" $0;
}