TODO.md

Basic Functionality

• Track highlights per document
• Edit causes editAt event as necessary
• Allow whitespace and comment editing of interpreted text
• Edit_at when editing an interpreted proof (and not whitespace)
• Go to point
• Clear all highlights upon reset
• show Goal and Hyps
• interrupt computation
• set coq options
• support queries
• status bar (ready vs working)
• parse bullets
• forward messages to extension
• display Check messages, etc.
• quotes in comments must be correctly matched
• quotes in comments must be correctly matched for syntax highlighting
• handle _CoqProject
• syntax coloring (not as a separate package)
• lazy load coqtop
• show info messages in own output buffer
• command: finish computation
• gutter icons for each edit position
• move cursor with stepForward, etc.

Future Features

• universal RPC
• Autocompletion
• Ltac debugging
• Substitution
• Symbols (subst. for text)
• Show fancy window pane for goal and hyps, etc.
• Find references
• Find definition
• Peek definition
• Set options