Example of Asynchronous Linting

Show
1

Dear PM devs and community,

first of all thanks to the developers for CM and PM, the first of which we have extensively used in our project with success for years!

I am posting a small example of an async linter that we have developed. It seems to work well, but it was not so trivial. Hope it is useful to others, and of course suggestions, tips, and review is very welcome.

The code is here jscoq/frontend/classic/js/coq-editor-pm.js at 4b026d515099a25a8430fcd34fa6c624ec40830c · jscoq/jscoq · GitHub

Some notes:

  • It is not clear if it is better to store decorations in the plugin state, or some other structure and then have the prop generate them.
  • It is not clear if we want to stream the diagnostics or not, and the implications are in terms of performance
  • The main problem we found is that due to Decorations taking the document, it is very easy to have a race condition in which the diagnostics will overwrite a user-initiated transaction. We solved that using document versioning, but indeed it seems like maybe we are doing something wrong in the first place?

In particular, in Code example for applying decorations asynchronously - #2 by marijn it is said:

Either drop responses that are outdated, or record mappings in order to be able to map them to the updated document.

We drop responses that are outdated, but I’m curious as how the “record mappings” approach would work.

Cheers

2 Likes
2

Nice, thanks for sharing.

You basically create your decoration set for the old document, but store any transactions that come in during the request in a plugin field, so that you can map your decorations forward to make them align with the current state.

1 Like
3

prosemirror-typerighter has an example of this – for every transaction, we map our decorations, and any other entities that contain position information, through the transaction mapping.

We must also maintain a mapping from the previous to the current version of the document, so when the in-flight requests return matches, we can map the incoming ranges through this mapping to apply them to the new document in the right place.

3 Likes