Romain Tetley
Romain Tetley
Okay I think I know what is going on ! What you are experiencing is a feature of vscode called [sticky scroll](https://devblogs.microsoft.com/visualstudio/sticky-scroll-now-in-preview/). It does not take the decorations into account....
What do you mean by crash ? I get the following error: ``` Anomaly "Uncaught exception Unix.Unix_error(Unix.ENOENT, "create_process", "csdpcert")." Please report at http://coq.inria.fr/bugs/. ``` but the program does not crash...
@thery I am still unable to reproduce. Could you check ?
Closing. Feel free to reopen if this still happens
Hi ! Thanks for reporting ! By close the project I assume you mean the folder ? Or do you mean they still run even after closing vscode ? Also...
While working on #842 I noticed what is happening here. ```idtac``` sends a ```Info``` level feedback which we currently ignore entirely. Turning it on would display all info messages such...
Okay the idea will be to display them in the goal view, but avoid triggering diagnostics, that way we avoid squiggly lines. (See #842)
Should we add a setting to disable Info level messages ? Or is removing them from diagnostics enough ?
Not sure this is a duplicate of #454 as suggested by @Blaisorblade because the phrasing suggests the problem lies in the execution. I will try and reproduce and see. There...
So in fact the language server was sending the full file as "parsed ranges" at each send_highlights call. On such a big file it is indeed problematic. Working on it...