diff --git a/filter_sage.sed b/filter_sage.sed index f883f3a95c36425b39c8cdd0991d57034e45c912..7b59fe38d26df073cc2e11d9b0194d08a268ffd8 100755 --- a/filter_sage.sed +++ b/filter_sage.sed @@ -1,11 +1,23 @@ #!/usr/bin/sed -f -0,/^\\begin{sagesilent}/d -/^\\end{sagesilent}/,/^\\begin{sagesilent}/{ - s/.*\\sage{\(.*\)}.*/# RENDERED TO LATEX: \1 #/ +0,/^\\begin{sagesilent}/b nonsage +/^\\end{sagesilent}/,/^\\begin{sagesilent}/b nonsage + +1 { +:nonsage + s/.*\\sage{\(.*\)}.*/# RENDERED TO LATEX: \1/p + t end + s/.*\\section{\(.*\)}.*/## SECTION \1 ##/ T skip; h;s/\S/#/g;H;G;a p + b end :skip + s/.*\\subsection{\(.*\)}.*/# SUB SECTION \1 #/ + T end; + h;s/\S/#/g;H;g;a + p + b end +:end d }