[Metamath] Re: mm-web-rs server support

2024-02-07 Thread Mario Carneiro
It requires some changes to the mmrecent.html CSS, so for now a copy is hosted at https://github.com/digama0/mm-web-rs/blob/master/mmrecent.raw.html . The pages generated by mm-web-rs are significantly different under the hood, making use of modern HTML5, although it's still dressed up in the web

[Metamath] Re: mm-web-rs server support

2024-02-07 Thread Mario Carneiro
mm-web-rs now supports generation of the auxiliary pages: mmtheorems.html, mmrecent.html, mmtheoremsall.html, mmdefinitions.html, and mmascii.html, which was the last remaining piece to completely replace metamath-exe web site generation functionality. The next step is to add it to the website

[Metamath] Re: searching for theorem manually in Metamath lamp/

2024-02-07 Thread Marshall Stoner
Thank you. This works. On Tuesday, February 6, 2024 at 1:32:21 AM UTC-5 igori...@gmail.com wrote: > If I correctly understand the issue, then a feature similar to what you > described already exists in Metamath-lamp. In order to change a > justification, you may do the following: > >1.