Hi David,
At least, there was one that let you expand/contract proof steps, which one was that?
The viewer you're talking about is probably this one: http://metamath.tirix.org/geoisum1.html There are two things in there: First, this is also MathML, but this time generated not using Rust-based metamath-knife, but the good old C based metamath-exe. The code for that is still living in a PR: https://github.com/metamath/metamath-exe/pull/9 (Actually the code was available way before that, but Norm did not feel he was ready to open a GitHub repository at the time I wrote it) Unfortunately this was not merged at the time and Wolf and Mario started major clean up and refactoring. I see Mario has made some work but in the mean time there are new conflicts to solve. Also I tried to stick to the coding style I saw, which has now changed, so it probably does not live up to the rest of the code anymore. Second, the JS library which does the expand/contract is actually independent and could be used on the "classic" Metamath pages, IIRC. It is available here: https://github.com/tirix/mm-web-ui I'll answer to the other comments about the tool in a separated post! BR, _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7bcd8661-91d0-4feb-75fd-f7f52f4ba49d%40gmx.net.
