ott-vscode

Provides syntax highlighting and inline error reporting for the Ott semantics tool.

Features

Syntax Highlighting

The emphasis is on visually distinguishing the meta-language from the language being modeled. As a result, the files end up quite colorful.

I've optimized this for the One Dark Pro theme, but it should look okay with any theme. Some classes might not get distinguished if your theme doesn't define colors for enough scopes, though.

I'm no expert when it comes to visual design, so pull-requests are welcome with regards to the color choices.

Build-on-Save and Inline Error Reporting

When you save your file, it will be run with ott and any errors will be reported inline.

By default, ott is run with no arguments. However, if the first line of your file contains a magic comment of the form:

% !Ott args = "ARGS"

Then, Ott will be run with whatever args are given. This is useful for re-generating LaTeX or proof-assistant code automatically when you save.

Post-processors

If there are one or more magic comments of the form:

% !Ott postprocess = "COMMAND"

then on saving, after ott has finished, the given command(s) will be run. This is useful for building LaTeX into a PDF file, or for automatically running scripts over generated proof-assistant code.

Requirements

The command ott must be installed and on your $PATH.

Syntax highlighting recognizes some languages within the hom blocks, if you have a language pack installed for that language. Reccomended packages to allow this are:

• VSCoq or Coq
• Isabelle
• LaTeX Workshop or LaTeX Language Support

Extension Settings

None so far.

Known Issues

• No option to specify ott binary location
• Check-on-save always on, should be optional
• Not all errors have location (requires changes to Ott to fix)
• Error parsing is hacky, so some errors may not be reported

Future features

• [ ] Source-code formatting
• [ ] Inline unicode replacement, something like prettify-symbols-mode.

Contributing

Contributions are welcome and encouraged! Feel free to leave any issues or submit pull requests. Alternately, if you would like to collaborate, I will happily add collaborators to the repo.

Release Notes

[ 0.0.6 ]

• Fix regression in parse "no parse" errors
• Add parsing for "no conclusion" errors
• Internal warnings are now marked as Information, not Warning

[ 0.0.5 ]

• postprocess uses exec, not spawn

[ 0.0.4 ]

• Error parsing for bad contextrules
• Add "postprocess" option for magic comments

[ 0.0.3 ]

• Remove ansi-strip dependency
• Add output from Ott binary to "Output" pane

[ 0.0.2 ]

• Improved and cleaner error parsing
• Add back brackets to surrounding pairs, remove single quotes (messes up with prime variables)
• Logo and screenshot added

[ 0.0.1 ]

• Initial release