Using the Kate Editor

VDMJ should theoretically be accessible from any IDE or editor environment that supports the Language Server Protocol. One such environment is the Kate editor.

Configuring Kate to use VDMJ for VDM-SL, VDM++ and VDM-RT requires the following steps:

• Under Settings > Configure Kate..., go to the "Plugins" section and make sure the "LSP Client" plugin is enabled. If this is not available, look at your OS distribution for how to install it.
• On the "LSP Client" section, under the "Client Settings" tab, set the options as follows:
• On the "Open/Save" section, under the "Modes & Filetypes" tab, use the "New" button to create a new Filetype called "VDM-SL" in the Section "Sources"; use the default indentation mode; set the file extensions to *.vdmsl.
• Similarly, add new Filetypes for Sources/VDM++ and Sources/VDM-RT, using *.vdmpp and *.vdmrt as their file extensions, respectively.
• Set the three new Filetypes' highlighting modes to different values, that are currently unused in the "LSPClient" section's "Default Server Settings". I suggest trying Sources/Zonnon, Sources/xHarbour and Sources/FSharp. This is explained below!!
• In the "LSP Client" section, under "User Server Settings", add the following JSON:

{
    "servers": {
        "vdmsl": {
            "command": ["bash", "kate-lsp.sh", "-Dlsp.log.level=all", "-Dlsp.log.filename=kate.log", "-vdmsl"],
            "root": "",
            "url": "https://github.com/nickbattle/vdmj/lsp",
            "highlightingModeRegex": "^Zonnon$"
        },
        "vdmpp": {
            "command": ["bash", "kate-lsp.sh", "-Dlsp.log.level=all", "-Dlsp.log.filename=kate.log", "-vdmpp"],
            "root": "",
            "url": "https://github.com/nickbattle/vdmj/lsp",
            "highlightingModeRegex": "^xHarbour$"
        },
        "vdmrt": {
            "command": ["bash", "kate-lsp.sh", "-Dlsp.log.level=all", "-Dlsp.log.filename=kate.log", "-vdmrt"],
            "root": "",
            "url": "https://github.com/nickbattle/vdmj/lsp",
            "highlightingModeRegex": "^FSharp$"
        }
    }
}

• Note that the highlightingModeRegex field is a regex that matches the highlighting mode that we selected for the Filetypes. This is a limitation of Kate, which cannot easily add new languages, even though you can add new Filetypes. As a compromise, they have arranged to use the highlighting mode as a link between the Filetype/extension pattern and a given LSP server configuration. Unfortunately that means that the selected highlighting mode has to be unique in the LSP server configuration, and is also used to highlight keywords. The highlighting for Zonnon, xHarbour and FSharp is not ideal. You can try using a different highlight mode, but remember to change the JSON patterns to match, and make sure all VDM dialects use different, unused highlightingModeRegex's.
• Note also kate-lsp.sh must be on your $PATH. It is released under <git>/lsp/src/main/scripts and links to jars in the Maven repository.
• If you're using Windows, or don't have access to bash, you can use Java directly as follows (for "-vdmsl"):

"command": ["java", "-Xmx3000m", "-Xss1m", "-Dlsp.log.filename=kate.log", "-Dlsp.log.level=all", "-cp", "<path to>/vdmj-4.5.0.jar:<path to>/annotations-4.5.0.jar:<path to>/lsp-4.5.0.jar:<path to>/stdlib-4.5.0.jar", "lsp.LSPServerStdio", "-vdmsl"],

• You can omit the -Dlsp.log.* settings, which write LSP diagnostics to a file in the current folder. But this is very useful to start with, if there are problems!
• The kate-lsp.sh script can be passed a -P option, to select high precision. If you are using Windows, change all the jars in the "command" to use the "-P" versions.
• It is a good idea to completely restart Kate, if you change anything in its configuration.

Kate has a similar concept of "project" to VSCode, meaning an arbitrary folder that you open which contains a number of source files, all of the same dialect. So to start Kate with VDMJ, make sure all of your VDM source files are within one root folder (subfolders are allowed), and then use "Open Folder" in the editor to get started. You should be able to see on-the-fly syntax and type checking errors (LSP Client > Switch to Diagnostics Tab) as well as some navigation features . Look on the "LSP Client" menu for options and settings. You can open an individual file, but the LSP server still collects all of the files in the hierarchy in that case, starting from the current working directory (ie. where you started Kate).