Skip to content

Commit

Permalink
Update documentation for Dafny server
Browse files Browse the repository at this point in the history
  • Loading branch information
keyboardDrummer committed Jan 5, 2024
1 parent 880ba3f commit eea182e
Showing 1 changed file with 1 addition and 3 deletions.
4 changes: 1 addition & 3 deletions docs/DafnyRef/VSCodeIDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ the position of the parse or resolution error.

## 14.3. The Dafny Server {#sec-old-dafny-server}

Before Dafny [implemented](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyLanguageServer) the official [Language Server Protocol](https://microsoft.github.io/language-server-protocol/), it implemented its own protocol for [Emacs](https://github.com/boogie-org/boogie-friends), which resulted in a project called [DafnyServer](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyServer).
Before Dafny [implemented](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyLanguageServer) the official [Language Server Protocol](https://microsoft.github.io/language-server-protocol/), it implemented its own protocol for [Emacs](https://github.com/boogie-org/boogie-friends), which resulted in a project called [DafnyServer](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyServer). While the latest Dafny releases still contain a working DafnyServer binary, this component has been feature frozen since 2022, and it may not support features that were added to Dafny after that time. We do not recommend using it.

The Dafny Server has [integration tests](https://github.com/dafny-lang/dafny/tree/master/Test/server) that serve as the basis of the documentation.

Expand Down Expand Up @@ -156,5 +156,3 @@ btoa(JSON.stringify({

Thus to decode such output, you'd manually use `JSON.parse(atob(payload))`.

The Dafny Server is still supported, but we recommend using the [Language Server](https://github.com/dafny-lang/dafny/tree/master/Source/DafnyLanguageServer) instead. It is supported in [VSCode](https://marketplace.visualstudio.com/items?itemName=dafny-lang.ide-vscode) only. The Language Server also provides features such as ghost highlighting or symbol hovering.

0 comments on commit eea182e

Please sign in to comment.