Thanks Norm. I updated my visualization, so column width is calculated automatically now.
Best regards, Igor воскресенье, 27 декабря 2020 г. в 18:17:56 UTC+1, Norman Megill: > This is great! > > A slight cosmetic issue is that the Ref column sometimes overflows into > the Expression column for long theorem names, e.g. > https://expln.github.io/metamath/asrt/merco1lem18.html > Ideally the Ref column width should automatically be resized to the > longest theorem name. > > I modified metamath.exe to recognize a new $t keyword "htmlexturl" (HTML > external URL) that is now in set.mm on GitHub. Your visualization version > is linked to on each theorem page now (on the us2 server) e.g. > > http://us2.metamath.org/mpeuni/sqrt2irr.html > > NOTE TO EVERYONE: metamath.exe was updated on GitHub to "Version 0.194 > 26-Dec-2020" to recognize the new $t keyword. You will need to update it > locally for "verify markup" to pass with the set.mm change I made, either > from GitHub or http://us2.metamath.org/index.html#mmprog . If you are > using Windows, the 0.194 executable can be retrieved here: > http://us2.metamath.org/metamath/metamath.exe > > Norm > > > On Thursday, December 24, 2020 at 12:49:57 PM UTC-5 [email protected] > wrote: > >> The problem with the “jumping” [-] button is fixed. I also added few more >> features: >> >> 1) Adjustment of column widths: click a “three horizontal lines” button >> at the top right corner of the proof table. Column widths are stored in the >> local storage of the browser, so width adjustment may be done only once and >> it will be applied to all other assertion pages unless local storage is >> turned off. >> >> 2) Highlighting of matching parentheses: hover the mouse over a >> parenthesis to temporarily highlight it or click it to highlight it >> permanently. This feature works only on unexpanded expressions. >> >> Best regards, >> Igor >> >> воскресенье, 20 декабря 2020 г. в 17:46:28 UTC+1, Igor Ieskov: >> >>> Thanks Benoit and Norm! >>> >>> I will try to fix this behaviour of +/- button. (it happens in all >>> browsers) >>> >>> Best regards, >>> Igor >>> >>> воскресенье, 20 декабря 2020 г. в 17:35:35 UTC+1, Norman Megill: >>> >>>> On Sunday, December 20, 2020 at 11:13:33 AM UTC-5 Norman Megill wrote: >>>> >>>>> 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 >>>>> >>>> >>>> s.b. "upper-left" >>>> >>>> >>>>> without moving the mouse, although I'm not sure how hard that is to do. >>>>> >>>>> Norm >>>>> >>>> -- 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/1ffb0e37-c04a-4c81-8ecb-af84536e0d2en%40googlegroups.com.
