bos@149: #!/usr/bin/env python
bos@149: 
bos@149: import os
bos@149: import sys
bos@149: import re
bos@149: 
bos@149: unicode_re = re.compile(r'&#x00([0-7][0-9a-f]);', re.I)
bos@149: fancyvrb_re = re.compile(r'id="fancyvrb\d+"', re.I)
bos@149: 
bos@149: tmpsuffix = '.tmp.' + str(os.getpid())
bos@149: 
bos@149: def fix_ascii(m):
bos@149:     return chr(int(m.group(1), 16))
bos@149: 
bos@149: for name in sys.argv[1:]:
bos@149:     tmpname = name + tmpsuffix
bos@149:     ofp = file(tmpname, 'w')
bos@149:     for line in file(name):
bos@149:         line = unicode_re.sub(fix_ascii, line)
bos@149:         line = fancyvrb_re.sub('id="fancyvrb"', line)
bos@149:         ofp.write(line)
bos@149:     ofp.close()
bos@149:     os.rename(tmpname, name)