That's very much on my roadmap, but I had to start with .mm because I don't believe the code for generating .mmp files exists on the JavaScript platform yet. (Glauco's Yamma doesn't have it yet, and Igor's proof assistant doesn't use them or save any intermediate format I'm aware of).
The ctrl+g of mmj2 is not in yamma, yet (I guess that's the only feature I use in mmj2, that's not going to be in the first "stable" release) But Thierry's metamath-vspa, has a command "Show Proof" that creates the .mmp file (if you want to have a look at his code) Glauco -- 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/64ee4737-03a4-402f-913f-c91808188b4fn%40googlegroups.com.
