Generating Documentation

The VS Code extension for IPL includes a built-in documentation creation system, which can be accessed via a dedicated VSCode command. Simply running the command Ipl:Generate Documentation on an IPL file will produce a document in HTML format containing detailed information on the various IPL entities defined in the model, including messages, enumeration types, and repeating groups. The documentation generation process is fully automatic by default, but it can optionally be customized via user-defined Markdown files specifying the desided structure and format of the generated documents.

The following sections explain how to generate documentation via the VS Code extension for IPL, and how to use Markdown files to customize the generation process.

Visual Studio Code extension

To access the document generation functionality from VS Code, please make sure to

• install the Imandra CLI
• install the latest IPL VS Code Plugin
• be registered with an Imandra account

Documentation can be generated by opening an IPL file and invoking the VS Code command Ipl:Generate Documentation. Upon successfull completion, a documentation page in HTML format will be saved in the same location and with the same file name of the source IPL file. Note that this process will not succeed if

• the IPL model contains errors, or
• there is no internet connection, or
• the user is not authenticated into their Imandra account

Authentication

The documentation generation command is only available to authenticated users. The IPL extension will guide the user through authentication if they have not logged in yet; however, a valid Imandra account and a working installation of the Imandra CLI are prerequisites.

If the VS Code command Ipl:Generate Documentation is invoked on an unauthenticated machine, the extension will instruct the user to log in:

Upon clicking "Proceed", a login page will open in a new browser window. After successfully logging in, the browser page will show an authentication code, which must be copied and pasted into the following text box back in VS Code.

After entering the authentication code, the extension will ask to select the computing zone.

After this last step, the user will be authenticated and the IPL extension will proceed to generate documentation.

Formatting documentation with Markdown

By default, the IPL extension formats the output HTML file automatically, following a standard document structure that lists all messages, fields, enumeration types, and repeating groups defined in the IPL model. Documentation generated using this standard format is highly detailed and thus likely to be sufficient for most use cases, however it is possible to intruct the extension to use a custom format instead.

The IPL extension supports full customization of the documentation generation process via Markdown. This feature allows the user to provide a Markdown file with their own content and formatting, which will be used to render the final HTML documentation file. The extension supports a custom version of Markdown that allows to insert in-document references to IPL entities (like messages and enumeration types) that get automatically rendered into rich documentation for those entities. This enables the user to write content to the desired level of detail, leaving the generation of complex data-based lists and tables to IPL.

To use Markdown formatting to drive the documentation generation process, simply add a Markdown file in the same location of the IPL model. The Markdown file should have the same file name as the IPL file, but with .md extension.

When invoking the command Ipl:Generate Documentation, the extension will look for a matching Markdown file in the same location of the target IPL file and, if present, use it to render documentation.

See Markdown formatting for details on the Markdown syntax supported by the extension.

Markdown formatting

The Markdown format supported by the Ipl:Generate Documentation command is a subset of v0.30 of the CommonMark standard, augmented with special code blocks that can be used to insert references to various entities from the IPL model (such as messages and enumeration types) and automatically generate richly-formatted documentation for them. Thus, one can use Markdown formatting to manually specify the textual content and overall structure of the document, while leaving detailed technical documentation to the automated process.

To make template editing easier, the VS Code extension provides an additional command Ipl:Generate Markdown template that automatically creates a Markdown file complete with all the templating constructs that are needed to generate the IPL model’s default HTML documentation, exactly as you would get from running Ipl:Generate Documentation without templates. This Markdown file can then be used to learn how the templating syntax works, and apply custom modifications to the HTML docs, without the need to draft a full template from scratch.

Supported Markdown constructs