Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[hover] New option show_loc_info_on_hover to display parsing debug info. #588

Merged
merged 1 commit into from
Oct 25, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,11 @@
# unreleased
-----------

- new option `show_loc_info_on_hover` that will display parsing debug
information on hover; previous flag was fixed in code, which is way
less flexible. This also fixes the option being on in 0.1.8 by
mistake (@ejgallego, #588)

# coq-lsp 0.1.8: Trick-or-treat
-------------------------------

Expand Down
5 changes: 2 additions & 3 deletions controller/rq_hover.ml
Original file line number Diff line number Diff line change
Expand Up @@ -173,8 +173,6 @@ module type HoverProvider = sig
end

module Loc_info : HoverProvider = struct
let enabled = true

let h ~contents:_ ~point:_ ~node =
match node with
| None -> "no node here"
Expand All @@ -183,7 +181,8 @@ module Loc_info : HoverProvider = struct
Format.asprintf "%a" Lang.Range.pp range

let h ~contents ~point ~node =
if enabled then Some (h ~contents ~point ~node) else None
if !Config.v.show_loc_info_on_hover then Some (h ~contents ~point ~node)
else None

let h = Handler.MaybeNode h
end
Expand Down
12 changes: 9 additions & 3 deletions editor/code/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -150,11 +150,17 @@
"type": "number",
"default": 150,
"description": "Maximum number of errors per file, after that, coq-lsp will stop checking the file."
},
"coq-lsp.show_stats_on_hover": {
}
}
},
{
"title": "Hover",
"type": "object",
"properties": {
"coq-lsp.show_loc_info_on_hover": {
"type": "boolean",
"default": false,
"description": "Show timing and memory stats for a sentence on hover."
"description": "Show parsing information for a sentence on hover."
}
}
},
Expand Down
2 changes: 2 additions & 0 deletions editor/code/src/config.ts
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ export interface CoqLspServerConfig {
max_errors: number;
pp_type: 0 | 1 | 2;
show_stats_on_hover: boolean;
show_loc_info_on_hover: boolean;
}

export namespace CoqLspServerConfig {
Expand All @@ -31,6 +32,7 @@ export namespace CoqLspServerConfig {
max_errors: wsConfig.max_errors,
pp_type: wsConfig.pp_type,
show_stats_on_hover: wsConfig.show_stats_on_hover,
show_loc_info_on_hover: wsConfig.show_loc_info_on_hover,
};
}
}
Expand Down
3 changes: 3 additions & 0 deletions fleche/config.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@ type t =
(** Pretty-printing type in Info Panel Request, 0 = string; 1 = Pp.t; 2
= Coq Layout Engine *)
; show_stats_on_hover : bool [@default false] (** Show stats on hover *)
; show_loc_info_on_hover : bool [@default false]
(** Show loc info on hover *)
; pp_json : bool [@default false]
(** Whether to pretty print the protocol JSON on the wire *)
; send_perf_data : bool [@default true]
Expand All @@ -62,6 +64,7 @@ let default =
; max_errors = 150
; pp_type = 0
; show_stats_on_hover = false
; show_loc_info_on_hover = false
; verbosity = 2
; pp_json = false
; send_perf_data = true
Expand Down
Loading