feature to print html with show trace?

[Stefan Allan]

It might be useful to have a way to print html files for the immediate dependencies of a statement, similar to how the 'show trace_back /tree /depth <n>' command works.  For example along with the proofs of ~syl one could have the proofs of ~a1i and ~mpd, and then proofs of their dependencies, etc. I'm thinking if say you wanted to print out pages of metamath proofs for a course you could do this for several statements, varying the depth parameter to the desired level of detail. However I've tried different syntax and I don't think metamath will do this. Would this be a desirable feature?

Very sorry to hear about Norm's passing.... I never met him in person but he was always there ready to answer even silly questions, and helpful in teaching me concepts whenever I hit a stumbling block. A very good soul. RIP.