Using the neovim Editor

Language server setup

Both vim and neovim can detect the various VDM file types out of the box. Furthermore, the nvim-lspconfig plugin allows you to quickly configure neovim's native LSP client for VDMJ's language server. As long as VDMJ is in your local Maven repository, this is as easy as adding

require'lspconfig'.vdmj.setup{}

to your init.lua file. You can find all the available options in the documentation of nvim-lspconfig.

Debugger support

VDMJ provides a DAP server, which can be used within (neo)vim by configuring a DAP client plugin, such as nvim-dap or vimspector. Here we will show you how to do the former, and we will assume that you are using the LSP configuration provided by nvim-lspconfig.

First of all, you need to enable the DAP server by adding the debugger_port option to your LSP configuration, such as:

require'lspconfig'.vdmj.setup{
  options = {
    debugger_port = 0,
  },
}

Negative values disable the DAP server, a 0 value enables it on a random port, while positive values enable it on a fixed port and represent the port number on which the server will listen. In particular, this means that if a positive value is given, only one instance of the server can be active at any given time.

You can then configure an adapter for VDMJ's DAP server and enable it for the file types you wish to support, i.e. vdmsl for VDM-SL, vdmpp for VDM++, or vdmrt for VDM-RT.

local dap = require 'dap'

local filter_vdmj = function(table)
  return table.name == "vdmj"
end

dap.adapters.vdm = function(callback)
  local vdmj_clients = vim.tbl_filter(filter_vdmj, vim.lsp.get_active_clients())
  callback({
    type = 'server',
    host = '127.0.0.1',
    -- fetch DAP port number from the first active VDMJ language server
    port = vdmj_clients[1].server_capabilities.experimental.dapServer.port,
  })
end

dap.configurations.vdmsl = {{
  type = 'vdm',  -- adapter name
  request = 'launch',
  name = 'Launch VDM Debug',
  noDebug = false,
}}

Many thanks to Alessandro Pezzoni ([email protected]) for contributing this page.