Skip to content

Commit

Permalink
release: Update extension
Browse files Browse the repository at this point in the history
  • Loading branch information
famoser committed Mar 3, 2024
1 parent 51fd0dc commit 838d35f
Show file tree
Hide file tree
Showing 6 changed files with 18 additions and 7 deletions.
5 changes: 5 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,10 @@
# Changelog

## v1.6.0

Add language configuration, TextMate grammar and semantic tokens.


## v1.5.0

Add hover.
Expand Down
8 changes: 7 additions & 1 deletion CONTRIBUTE.md
Original file line number Diff line number Diff line change
Expand Up @@ -41,10 +41,16 @@ The architecture is inspired by an article series by [tomassetti](https://tomass

The language server first lexes and parses the ProVerif code. Both the lexer as well as the parser are specified in Antl3r grammar, as this has good tool support to generate corresponding TypeScript code. The lexer is written by hand. The parser is transpiled from ProVerif's original `pitparser.mly` file using a python script called `pitparser-transpile-g4.py`.

Then, the language server builds up the symbol table. To do this, relevant grammar rules have to implemented manually. For most this should be done; some more obscure are however not done yet. As long as not all rules are implemented, navigation might fail or be wrong.
Then, the language server builds up the symbol table. To do this, relevant grammar rules have to implemented manually. For most rules this should be done; some more obscure rules are however not implemented. As long as not all rules are implemented, navigation might fail or be wrong.

Lastly, the language server waits for the user to click on an identifier, and then picks the closest element in the symbol table.

## How it works: Syntax highlighting

Syntax highlighting works primarily over the TextMate grammar in [./syntaxes/pv.tmLanguage.json](./syntaxes/pv.tmLanguage.json). As TextMate works quite differently to antlr, the rules are translated by hand. Details of the rules have been ommitted, to save on complexity. The primary task of the antlr grammar is to identify keywords, operators and types.

While the TextMate grammar is fast, it is unable to precisely color. For example, some expressions allow both variables as well as functions to be referenced, which cannot be easily expressed in the grammar. For this, the language server implements semantic tokens: It scans the whole file, and returns a list of tokens it recognises as functions, variables and parameters. VSCode then adjusts the colors appropriately.

## Publish

Process:
Expand Down
4 changes: 2 additions & 2 deletions package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
"author": "ProVerif",
"icon": "img/icon.png",
"license": "MIT",
"version": "1.5.0",
"version": "1.6.0",
"repository": {
"type": "git",
"url": "https://github.com/ProVerif/vscode-proverif-language-service"
Expand Down
4 changes: 2 additions & 2 deletions server/package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion server/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
"name": "vscode-proverif-server",
"description": "Language support for the ProVerif language - server",
"author": "ProVerif",
"version": "1.5.0",
"version": "1.6.0",
"license": "MIT",
"engines": {
"node": "*"
Expand Down

0 comments on commit 838d35f

Please sign in to comment.