How to make as simple as tool which would make some simple operation over HTML (e.g., headings numbering)? If I would use htmllib.py, I would have to build HTMLformatter or I am wrong and it is easy? Thanks Matthew