VDM model files are meant to be changed in the Editor area.

Syntax Highlighting

The syntax highlighting is implemented using TextMate grammars located in the syntaxes folder. Currently only highlighting of VDM keywords is provided by the extension, but the long term goal is to have more context-aware syntax highlighting.

If you come from Overture and like that, all keywords have the same colour, this can be achieved by changing your VS Code color theme. If you want one that looks a lot like Overture/Eclipse try the theme "Eclipse Classic Light".

Syntax and Type Checking

Syntax checking is carried out continuously as source files are changed (even before the files are saved). Whenever files are saved, assuming there are no syntax errors, a full type check of the entire VDM model is performed. All errors appear in the Problems view, which can be opened via the View menu, or by typing (CTRL-SHIFT-M).

Snippets

VS Code snippets can be particularly useful when you are new to writing VDM models. If you press CTRL+space after typing the first few characters of a snippet name, VS Code may offer a proposal. For example, if you type fun followed by CTRL+space, the IDE will propose the use of an implicit or explicit function template. If you select a template using the cursor keys, a further CTRL+space will display the content of the snippet. Note that the editor may also offer symbols to insert, based on the content of your specification. Symbol completions have an "abc" icon, whereas code snippets have a box icon.

The IDE includes several templates: cases, quantifications, functions (explicit/implicit), operations (explicit/implicit) and many more. The use of templates makes it much easier for users to create models, even if they are not deeply familiar with the VDM syntax. However, note that these completions are not context sensitive, so you can be offered completions that are not legal at the given position in the source.

Smart Navigation

Multiple actions exist for navigating to the definition of a given identifier in a specification: Ctrl + click, the right-click context menu or pressing F12 while hovering on the identifier. If you press F12 twice, the editor will highlight all occurrences of the symbol (or if there is only one, it will navigate to it). Occurrences can also be shown via SHIFT-F12.

Outline Navigation

An outline view of the currently open file can be enabled by right-clicking on the Explorer view title and ticking Outline. This shows the current module or class, and within that the function/operation/type etc. definitions. Clicking on a definition will navigate to that definition's source in the editor window. A "breadcrumb" view is also presented along the top of the editor window, showing the project, file, module, definition that is currently highlighted. This can also be used to navigate around your project or workspace.

Code Completion

A limit level of code completion is available in the extension, where the available classes, types, operations, etc. is presented when typing in the editor. Since VDMJ does not have an incremental compiler we are only able to refresh the available completion items on save. This also means that as soon as you start typing the completion items are somewhat outdated and we are left to "guessing" about what would fit at different locations. In the future, it would be nice to have an incremental compiler, which will enable even better code completion, but that is not on the development schedule for now.