CJ Bell

don't load if doc is viewed in diff-mode

1

when a coq script is shown in diff view * do not apply highlights * do not load proof-view

vscode truncates output buffer, so give option to display as a file

error: term "X" has type "Y" when it is expected to have type "Z": provide a way to quickly see the difference between "Y" and "Z".

feature: when a sentence-state is invalidated by editing the document, do not immediately rewind the STM state. Instead: 1. mark the state as invalidated 2. highlight invalidated states to the...

chords: support multiple chords keybindings (blocked by Microsoft/vscode#6966, but there may be a way to hack it?)

1. get a testing framework in place 2. implement some basic tests ... adopt practice of adding new tests for each closed bug (regression) and new feature.

Feature -- "open coqtop here": runs coqtop interactively, optionally adds the commands up to the given point, and provides a terminal for the user to interact with coqtop.