13 lines
343 B
Awk
Executable file
13 lines
343 B
Awk
Executable file
#!/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;
|
|
}
|