[helm.git] / helm / software / matita / nlibrary / topology / convert.awk

BEGIN { p = 1; indent = ""; } 
/DOCBEGIN/ { indent = ""; NF = 0; }
/DOCEND/ { indent = "    "; NF = 0; } 
/HIDE/ { p = 0; }
{ if (p == 1) print indent $0; } 
/UNHIDE/ { p = 1; }