Skip to content

Commit

Permalink
[lsp] Remove noop --std argument.
Browse files Browse the repository at this point in the history
This argument was introduced very long time ago in the Lambdapi
implementation as we were not fully LSP compliant, but now we are.

The argument itself has been disabled since a long time, and it
misleading now; moreover we put it as default in `package.json`!!!
  • Loading branch information
ejgallego committed Jan 21, 2023
1 parent c0dda9e commit 02e1697
Show file tree
Hide file tree
Showing 4 changed files with 12 additions and 9 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@
- The info view is now script enabled and does client-side
rendering. It is also now bundled with esbuild as part of the build
process (@artagnon, @ejgallego, #171)
- The no-op `--std` argument to the `coq-lsp` binary has been
removed, beware of your setup in the extension settings
(@ejgallego, #208)

# coq-lsp 0.1.3: Event
----------------------
Expand Down
7 changes: 4 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -204,9 +204,10 @@ Studio Code.

### Emacs

You can use this mode with [eglot](https://joaotavora.github.io/eglot/) with
`$path_to_server --std`. Note that `--std` is needed otherwise eglot may choke
due to extra messages.
You can use this mode with [eglot](https://joaotavora.github.io/eglot/).

Note that `eglot` used to choke due to extra notifications that `coq-lsp` may
send, please open an issue if that's the case.

### Roadmap

Expand Down
7 changes: 4 additions & 3 deletions controller/coq_lsp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -490,7 +490,8 @@ let coq_init ~fb_queue ~bt =
let load_plugin = Coq.Loader.plugin_handler None in
Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin })

let lsp_main bt std coqlib vo_load_path ml_include_path =
let lsp_main bt coqlib vo_load_path ml_include_path =
let std = false in
LSP.std_protocol := std;

(* We output to stdout *)
Expand Down Expand Up @@ -552,7 +553,7 @@ let lsp_main bt std coqlib vo_load_path ml_include_path =
(* Arguments handling *)
open Cmdliner

let std =
let _std =
let doc = "Restrict to standard LSP protocol" in
Arg.(value & flag & info [ "std" ] ~doc)

Expand Down Expand Up @@ -620,7 +621,7 @@ let lsp_cmd : unit Cmd.t =
Cmd.(
v
(Cmd.info "coq-lsp" ~version:Version.server ~doc ~man)
Term.(const lsp_main $ bt $ std $ coqlib $ vo_load_path $ ml_include_path))
Term.(const lsp_main $ bt $ coqlib $ vo_load_path $ ml_include_path))

let main () =
let ecode = Cmd.eval lsp_cmd in
Expand Down
4 changes: 1 addition & 3 deletions editor/code/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -99,9 +99,7 @@
"items": {
"type": "string"
},
"default": [
"--std"
],
"default": [ ],
"description": "Arguments to the coq-lsp server"
},
"coq-lsp.eager_diagnostics": {
Expand Down

0 comments on commit 02e1697

Please sign in to comment.