News for hackers. Stuff that matters.
Re:Formalizing Text Editors in Coq by benrbray on Monday June 08, 2020 @06:20PM (#23461457)
Neat! It would be great to have a universally agreed-upon standard for how text editors behave (especially with regard to embedded / structured content, cursor position, etc.) and which operations they should support.

I recently came across ProseMirror [1], which seems to be a fantastic step in this direction. I've been experimenting with using it to build a Markdown editor with better support for math and pre-defined HTML blocks (for e.g. stating theorems, corollaries, etc. in math notes).

[1]: https://prosemirror.net/

Re:Formalizing Text Editors in Coq by edjroot on Monday June 08, 2020 @09:54PM (#23462853)
Indeed, ProseMirror is highly regarded by its code quality, just as its older sibling, CodeMirror. It even raised quite a bit of money on Indiegogo.

Are you planning on open-sourcing your editor? I'd love to use something like this on a project of mine. (I currently use the much less ambitious EasyMDE [1], which is based on CodeMirror.)

[1]: https://github.com/Ionaru/easy-markdown-editor

Re:Formalizing Text Editors in Coq by benrbray on Monday June 08, 2020 @11:46PM (#23463461)
Yes, that's the plan! I've long lamented that editors like Typora and Roam are closed-source, preventing users like me from tweaking them to my specific use-case. So I'm hoping to build something that others can modify if they need to.

My priorities are math support, citations/wikilinks and the ability to define custom document structure (theorems, etc.). I basically want users to be able to specify a ProseMirror schema with CSS to go along with it.

Can I ask about your specific use case? Any features you've been really missing? No promises they'll make it in, but I'm curious :)