Get latex code from agda listings

extractblocks.py

import re

from pathlib import Path

import os
import sys

tex = [i for i in list(Path("latex/").glob('*.tex'))]
latexTags = []

for i in tex:
  if i.is_file():
    lines = [line.rstrip('\n') for line in open(i, 'r')]
    keep = False
    with open(i, 'w') as outf:
      print("% This file is generated automatically. ", file=outf)
      for line in lines:
        s = re.search('.*latex:(.*)%.*', line, re.IGNORECASE)
        if line.startswith("\\begin{code}") and s:
          print("\\DefineAgdaCode{"+str(s.group(1))+"}{%", file=outf)
          latexTags.append(str(s.group(1)))
          keep = True
          print(line, file=outf)
        else:
          if keep:
            print(line, file=outf)
            if line.startswith("\\end{code}"):
              keep = False
              print("} %end of Agda def.", file=outf)

with open("latex/all-latex-tags.txt", 'w') as outf:
  for tag in sorted(latexTags):
    print("\\AgdaCode{%s}"%(tag), file=outf)