I like this very much. I think I will add a variable to the $t statement in set.mm so your base URL can be maintained there, instead of being hard-coded in metamath.exe. (And Thierry's structured version also, which is currently hard-coded.) Give me a week or so.
An observation (in Chrome 87.0.4280.88 at least): when the [+] box is clicked, the [-] box sometimes appears in the lower-left corner of the expanded table cell and other times in the upper-left corner. E.g. step 34 of sqrtirr shows a lower-left [-] and step 35 shows an upper-right [-]. Ideally the [-] would remain at the same position as the corresponding [+] so we can open and close an expansion without moving the mouse, although I'm not sure how hard that is to do. Norm On Saturday, December 19, 2020 at 3:05:07 PM UTC-5 igori... wrote: > Hello Norm, > > I’ve prepared a final version of my proof visualizations which you may add > links to on the main site. URLs of pages have a form of > https://expln.github.io/metamath/asrt/label.html Where “label” should be > replaced with the actual label of an assertion. (“asrt” stands for > “assertion” and it is a constant part of the URL) For example: > https://expln.github.io/metamath/asrt/sqrt2irr.html > > I spent some time investigating if I can implement unicode representation > but it appeared complicated because each symbol is represented as raw html > code. And it is not trivial to embed it into SVG visualization. > > Please let me know if everything is ok and you can add links to this > version. > > Best regards, > Igor > >> >>>>> -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fc65c4f8-2217-4df5-8455-90c944801c07n%40googlegroups.com.
