Maxime Dénès

[experiment] Separate parsing execution

11

This is an experimental branch, not to be merged directly.

"Source mangling" should not be done in place

6

The script responsible for building the html documentation currently "mangles" the source files in place, without warning. Not only is this dangerous (can destroy an unsaved change), but the transformation...

This PR makes VsCoq use Coq's document manager (https://github.com/coq/coq/pull/12461) instead of adapting the CoqIDE protocol. This is very much work in progress.

Manual testing on large developments

3

Play a bit with the extension on CompCert and Mathcomp, for example.

Add testing

1

Unit tests for the extension: https://code.visualstudio.com/api/working-with-extensions/testing-extension https://mochajs.org/ Unit tests for ML OUnit or nothing? End-to-end tests: https://github.com/ocaml/ocaml-lsp/tree/master/ocaml-lsp-server/test/e2e

Simultaneous publication of VsCoq versions

1

Study how we can make the document manager version and the legacy version of VsCoq coexist on the marketplace without being too confusing for users e.g. with older versions of...