When this becomes stable, I can add a link to your version on each theorem page of the main site, like the link that now says "Structured version" for Thierry's pages. This will let you have direct control over your content. (To start with, your base URL would be hard-coded in metamath.exe, but later I can add a keyword to the $t statement in set.mm so the URL can be maintained there.)
I don't know your long term plans, but I'll mention that personally (although I may be in the minority) I don't mind the ASCII notation in the proofs. It shows a beginner the direct relationship to the set.mm source and allows easy copy/paste. The user can also see the direct relationship between the ASCII and the Unicode rendering by switching between your page and the standard page, without having to consult set.mm or the awkward "ASCII Symbol Equivalents" page. BTW although of course it's not as convenient as your pages, some people might not know that metamath.exe can show the substitutions made in a step: MM> show proof 2p2e4 /detailed_step 18 Proof step 18: eqtr4i.1=oveq2i $p |- ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ) This step assigns source "oveq2i" ($p) to target "eqtr4i.1" ($e). The source assertion requires the hypotheses "cA" ($f, step 13), "cB" ($f, step 14), "cC" ($f, step 15), "cF" ($f, step 16), and "oveq1i.1" ($e, step 17). The parent assertion of the target hypothesis is "eqtr4i" ($p, step 47). The source assertion before substitution was: oveq2i $p |- ( C F A ) = ( C F B ) The following substitutions were made to the source assertion: Variable Substituted with C 2 F + A 2 B ( 1 + 1 ) The target hypothesis before substitution was: eqtr4i.1 $e |- A = B The following substitutions were made to the target hypothesis: Variable Substituted with A ( 2 + 2 ) B ( 2 + ( 1 + 1 ) ) Norm On Tuesday, December 8, 2020 at 9:27:57 AM UTC-5 igori...@gmail.com wrote: > Norm, Jim, thanks for your feedback! > > I updated the proof visualisation - all steps are collapsed by default and > a [+] button will expand selected node. Examples: > http://metamath.d4-e5.de/v2/data/2p/2e/2p2e4.html > http://metamath.d4-e5.de/v2/data/sq/rt/2i/sqrt2irr.html > http://metamath.d4-e5.de/index.html > > Also offline version may be found here > https://drive.google.com/drive/folders/1na2UM270rsCd85BQCmaJJSnak8HywfL8?usp=sharing > (its > size is 500M when unarchived). > > At the moment, step numbers in my proof visualisation don't correspond to > step numbers on http://us.metamath.org in many cases. This is because of > duplicate steps in my visualisation. I will fix this. > > Best regards, > Igor > > вторник, 1 декабря 2020 г. в 03:22:00 UTC+1, kin...@panix.com: > >> On 11/30/20 6:03 PM, Paul Chapman wrote: >> >> > I may be getting too old/lazy to code. Thirty years ago I’d’ve written >> > a knockout replacement for mmj2. ;) >> >> Haha I'll let you be the judge of whether you are too old/lazy to code. >> >> But if you are just disinclined to shave all the yaks required to get a >> smalltalk compatible with that experiment running again, hey that >> strikes me as quite understandable quite aside from age. Quite a saga. >> >> >> -- 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/d8062893-cdad-41fd-b348-33445386c408n%40googlegroups.com.