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/4edaf64a-0e61-4498-b0f8-cb5ecf613dd4n%40googlegroups.com.
