Normally, VDM source files are simple text files in whatever default encoding you normally use. But it is sometimes convenient to include VDM sources that are contained in other formats, such as Microsoft .doc and .docx, or the OpenDocument format .odt. This enables a VDM specification to be embedded with a larger descriptive document (perhaps in an appendix). That document can be included directly in a VSCode project rather than extracting and managing the VDM source separately.

VDM VSCode includes support for .doc, .docx, .odt, .tex and .latex files, but other external formats like PDF can be added via extensions.

When a file with a supported format is found in the project, the VDM source is extracted and a separate plain file is created. The name of the extracted file will be <original name>.<dialect>. So for example a document called FMI_Standard.docx would create a plain file called FMI_Standard.docx.vdmsl if the project dialect was VDM-SL. These extracted files are then included in the project build and can be navigated, functions can be launched and debugged etc. The extracted sources will be shown as nested under the original source in the Explorer view, and the extracted source will have a comment at the top saying, Document created from <original source> at <time>. For example:

When the VSCode instance is closed, the extracted files will be deleted, unless they have been modified. Once an extract has been modified, it will not be overwritten and so the changes made are safe. If the changes are subsequently edited back into the external format document, the extract file can be deleted and it will be re-created immediately (or when the project is next opened).

VDMJ allows for an arbitrary format reader to be plugged into the system. The reader have to implement the interface ExternalFormatReader, which requires the reader to produce a char[] that contains the extracted source. An example of a PDF reader can be found in the VDMJ examples project.

The new reader can be plugged in to VDMJ by adding it to the VDMJ property vdmj.parser.external_readers. The extracted source nesting can be configured using the properties explorer.fileNesting.enabled and explorer.fileNesting.patterns.