[hover] New option show_loc_info_on_hover to display parsing debug …

…info.

The previous flag was fixed in code, which is way less flexible.

This also fixes a bug in 0.1.8, where the option was left on by mistake.

CHANGES.md

@@ -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
 -------------------------------
 

controller/rq_hover.ml

@@ -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"
@@ -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

editor/code/package.json

@@ -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."
           }
         }
       },

editor/code/src/config.ts

@@ -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 {
@@ -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,
     };
   }
 }

fleche/config.ml

@@ -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]
@@ -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