LSP Plugin Writers Guide

So a plugin sounds like something to can add to LSP. So the LSP Plugin Writer's Guide explains that?

Basically, yes. A plugin here means an "Analysis Plugin".

This has been mentioned before, in the VDMJ HLD, I think?

Well, that's part of it yes. The idea is that an "analysis" is a separate phase of processing that a VDM specification can be subject to. Some analyses are built-in, like the syntax and type checking; some are written externally and added as plugins in separate jars.

But didn't this have something to do with the class mapping idea in the HLD?

That is true for the main analyses, like syntax, type checking, the interpreter and the PO generator. Those things have specialized AST classes that are mapped from somewhere else (ultimately, from the parser). But an analysis can work with the existing classes.

It might help if you could give me a realistic example?

Okay, so let's say that we have an idea of how to do some sophisticated checking that, say, enables complex VDM expressions to be simplified. That would be a useful thing to have, and it could perhaps provide hints as you were writing a specification.

So you'd package this into a plugin somehow?

Yes.

And it would be an analysis plugin?

Yes, because it's adding some sophisticated checking to your specification. But at the other end of the spectrum, an analysis plugin could just do a spell check of the variables or make recommendations about style.

Okay, so how does this fit with class mapping?

*Well, a sophisticated analysis is much more likely to want its own specialized classes, mapped from somewhere else. A simple spell checker would not need to do that.