Most are done during crafting Agda REPL.
It is a semi-persistent data structure backed by CM's rope structure. Introduction.
Similar to Vim's concept of folding. Useful when the language is indent-sensitive but you do not have a language service in hand.
A hack to gather candidates of the same label and allows one to navigate it like a grid.
Allow one to bake syntax highlighting, autocompletions, etc. into the field.
A bullet-proof setup to ensure that the text can never contain newline characters.
Only highlight active lines if all selection is empty.
Comment:
- My original plan was to "stop highlighting that line if it contains a non-empty selection", but there was no easy way to instruct
highlightActiveLine
extension to do so.- I wanted to use a state field, but the
provide
requires a facet which does not make sense in my scenerio.