Hi there, Just to clarify, this second server is different from the 'metamath-web <https://github.com/tirix/metamath-web>' I was mentioning two weeks ago in another post <https://groups.google.com/g/metamath/c/oOHiy3i-cRw/m/YGd5-DhiDAAJ>, and which provides the pages at http://metamath.tirix.org:3030/ <http://metamath.tirix.org:3030/mpests/toc>.
This shows how easy it is now to write a small server which when using the metamath-knife library as a starting point! The functionalities covered are slightly different, but both can be completed fairly easily. I think Mario put an emphasis on reproducing the same functionality as Norm's original pages, while I took some liberties with the formatting, and added the "structured typesetting" as a display option. Mario, there's another project I'd like to start based on metamath-knife, that would be an LSP server similar to what you've been doing for MM0, which would allow to turn Visual Studio into a tool for viewing and editing not just Metamath source files, but maybe also Metamath proof files - that would certainly be a lofty goal! What I have is really just the scaffolding, but I'll start to share it here <https://github.com/tirix/metamath-vspa>. Could we join forces for that one? Is anyone else interested? _ Thierry On 30/01/2022 15:43, Mario Carneiro wrote:
Hi All, I just wanted to share some metamath-knife progress: The https://github.com/digama0/mm-web-rs experimental metamath web site clone is now able to draw complete theorem pages, including the step list, forward references and axioms used, comment markup, dummy variable and allowed substitution hints, basically everything visible on the page, all powered by the metamath-knife API. Furthermore, as a result of the switch to a rust backend it is now quite simple to add a web server, so now you can run "mm-web-rs server" and it will serve pages like http://localhost:8080/mpeuni/pnt.html as you would expect from a static server. Mario -- 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/CAFXXJStpvP5oC7QvwxroZbEdZHEfcSzAB4e2EVf7Coo-S0XZgw%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAFXXJStpvP5oC7QvwxroZbEdZHEfcSzAB4e2EVf7Coo-S0XZgw%40mail.gmail.com?utm_medium=email&utm_source=footer>.
-- 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/5de715c8-5330-a618-b906-83b298963842%40gmx.net.
