Apparently, it is quite easy to write plugins for intellij idea. I just tried and one day later, I had written lexers and primary parsers for the mm0 and mmu files, with JFlex and GrammarKit (and thanks to mario's answers and the experience gained by writting home made parsers for mm0/mmu),
A few minutes ago, I just pushed accidently my prototype plugin to https://github.com/Lakedaemon/mm0-kotlin-tooling I did not push the plugin to the market place yet though (because it misses lots of functionnalities, I'll do that later when it is ready) So, I'll probably be able to develop and distribute a fully feature plugin adding mm0 and mmu support to intellij idea (which has a free community version), with the usual intellisense goodness added to it. This should be a nice alternative to vs-code. There is an issue that must be addressed though : Intellij idea refuses to open set.mm.mmu outside of raw mode (no syntax highlighting/advanced features) because it is much too big (at 450MB). Which is quite understandable. But that means that people will have to break mmu (and mm0) files into smaller parts to be able to work with them confortably. There is an "import file.mm0;" statement at the top of https://github.com/digama0/mm0/blob/master/examples/string.mm0 that could mitigate the issue, by allowing to split files in smaller parts and to reassemble them when veryfing. BUT the fact that these statements aren't in the mm0 grammar should render vscode and intellij idea unable to work with these files (because parsing these files that hold an invalid statement will fail). So,it would be nice to have a solution that allows : - reusing mm0/mmu files (like modules) - limit their length/split them - agregate them Mario recently published a tool that can agregate files with "import at their top". But that doesn't fix the issue for intellij idea Maybee, a solution would be to stip the mm0 files from the import statement and have a third filetype (.mmerge) that holds a structured document telling how to build big mm0/mmu files from smaller parts Best regards, Olivier -- 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/588c3eac-492c-4bb8-9241-bbc77d999e92%40googlegroups.com.
