[code] Show server status using LanguageStatusItem

We show server checking status and toolchain version using the new
`LanguageStatusItem` UI. It is also possible to control using this UI
whether the server is in continuous or lazy mode. Some more changes:

- Added a new command to toggle the mode.
- Show `coq-lsp` version info.

More information about what the server is doing should be possible if
the users want! (For example, we should show memory use, etc...)

Author: ejgallego

CHANGES.md

@@ -1,11 +1,6 @@
 # unreleased
 ------------
 
- - Added new heatmap feature allowing timing data to be seen in the
-   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
-   comamnd. Can be configured to show memory usage. Colors and
-   granularity are configurable. (@Alizter and @ejgallego, #686,
-   grants #681).
  - 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
@@ -132,19 +127,25 @@
    #697)
  - Always dispose UI elements. This should improve some strange
    behaviors on extension restart (@ejgallego, #708)
- - Support Coq meta-commands (Reset, Reset Initial, Back) They are
-   actually pretty useful to hint the incremental engine to ignore
-   changes in some part of the document (@ejgallego, #709)
+ - [code] Added new heatmap feature allowing timing data to be seen in
+   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
+   comamnd. Can be configured to show memory usage. Colors and
+   granularity are configurable. (@Alizter and @ejgallego, #686,
+   grants #681).
+ - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
+   They are actually pretty useful to hint the incremental engine to
+   ignore changes in some part of the document (@ejgallego, #709)
  - JSON-RPC library now supports all kind of incoming messages
    (@ejgallego, #713)
- - New `coq/viewRange` notification, from client to server, than hints
-   the scheduler for the visible area of the document; combined with
-   the new lazy checking mode, this provides checking on scroll, a
-   feature inspired from Isabelle IDE (@ejgallego, #717)
- - Have VSCode wait for full LSP client shutdown on server
+ - [code/server] New `coq/viewRange` notification, from client to
+   server, than hints the scheduler for the visible area of the
+   document; combined with the new lazy checking mode, this provides
+   checking on scroll, a feature inspired from Isabelle IDE
+   (@ejgallego, #717)
+ - [code] Have VSCode wait for full LSP client shutdown on server
    restart. This fixes some bugs on extension restart (finally!)
    (@ejgallego, #719)
- - Center the view if cursor goes out of scope in
+ - [code] Center the view if cursor goes out of scope in
    `sentenceNext/sentencePrevious` (@ejgallego, #718)
  - Switch Flèche range encoding to protocol native, this means UTF-16
    code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
@@ -154,7 +155,7 @@
    user navigates proofs (@Alidra @ejgallego, #722, #725)
  - `fcc`: new option `--diags_level` to control whether Coq's notice
    and info messages appear as diagnostics
- - Display the continous/on-request checking mode in the status bar,
+ - [code] Display the continous/on-request checking mode in the status bar,
    allow to change it by clicking on it (@ejgallego, #721)
  - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
    #611)
@@ -173,6 +174,10 @@
  - [petanque] Return extra premise information: file name, position,
    raw_text, using the above support for reading .glob files
    (@ejgallego, #735)
+ - [code] Display server status using the `LanguageStatusItem`
+   facility, for now we display version and checking status
+   information (moved from #721), and we also allow to toggle the
+   checking mode from there (@ejgallego, #728)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

README.md

@@ -39,6 +39,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
 
 - [🎁 Features](#-features)
   - [⏩ Incremental Compilation and Continuous Document Checking](#-incremental-compilation-and-continuous-document-checking)
+  - [👁 On-demand, Follow The Viewport Document Checking](#-on-demand-follow-the-viewport-document-checking)
   - [🧠 Smart, Cache-Aware Error Recovery](#-smart-cache-aware-error-recovery)
   - [🥅 Whole-Document Goal Display](#-whole-document-goal-display)
   - [🗒️ Markdown Support](#️-markdown-support)
@@ -89,6 +90,14 @@ restart your proof session where you left it at the last time.
 Incremental support is undergoing refinement, if `coq-lsp` rechecks when it
 should not, please file a bug!
 
+### 👁 On-demand, Follow The Viewport Document Checking
+
+`coq-lsp` does also support on-demand checking. Two modes are available: follow
+the cursor, or follow the viewport; the modes can be toggled using the Language
+Status Item in Code's bottom right corner:
+
+<img alt="On-demand checking" height="572px" src="etc/img/on_demand.gif"/>
+
 ### 🧠 Smart, Cache-Aware Error Recovery
 
 `coq-lsp` won't stop checking on errors, but supports (and encourages) working

compiler/output.ml

@@ -9,7 +9,6 @@ let pp_diags fmt dl =
 (* We will use this when we set eager diagnotics to true *)
 let diagnostics ~uri:_ ~version:_ _diags = ()
 let fileProgress ~uri:_ ~version:_ _progress = ()
-let perfData ~uri:_ ~version:_ _perf = ()
 
 (* We print trace and messages, and perfData summary *)
 module Fcc_verbose = struct
@@ -24,26 +23,30 @@ module Fcc_verbose = struct
   let perfData ~uri:_ ~version:_ { Fleche.Perf.summary; _ } =
     Format.(eprintf "[perfdata]@\n@[%s@]@\n%!" summary)
 
+  let serverVersion _ = ()
+  let serverStatus _ = ()
+
   let cb =
-    Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+    Fleche.Io.CallBack.
+      { trace
+      ; message
+      ; diagnostics
+      ; fileProgress
+      ; perfData
+      ; serverVersion
+      ; serverStatus
+      }
 end
 
 (* We print trace, messages *)
 module Fcc_normal = struct
   let trace _ ?extra:_ _ = ()
-  let message = Fcc_verbose.message
-  let perfData = Fcc_verbose.perfData
-
-  let cb =
-    Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+  let cb = { Fcc_verbose.cb with trace }
 end
 
 module Fcc_quiet = struct
-  let trace _ ?extra:_ _ = ()
   let message ~lvl:_ ~message:_ = ()
-
-  let cb =
-    Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+  let cb = { Fcc_normal.cb with message }
 end
 
 let set_callbacks (display : Args.Display.t) =

controller/coq_lsp.ml

@@ -49,35 +49,52 @@ let rec process_queue ~delay ~io ~ofn ~state : unit =
   | Some (Cont state) -> process_queue ~delay ~io ~ofn ~state
 
 let concise_cb ofn =
+  let send_notification nt =
+    Lsp.Base.Message.(Notification nt |> to_yojson) |> ofn
+  in
+  let diagnostics ~uri ~version diags =
+    if List.length diags > 0 then
+      Lsp.JLang.mk_diagnostics ~uri ~version diags |> send_notification
+  in
   Fleche.Io.CallBack.
     { trace = (fun _hdr ?extra:_ _msg -> ())
     ; message = (fun ~lvl:_ ~message:_ -> ())
-    ; diagnostics =
-        (fun ~uri ~version diags ->
-          if List.length diags > 0 then
-            Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
+    ; diagnostics
     ; fileProgress = (fun ~uri:_ ~version:_ _progress -> ())
     ; perfData = (fun ~uri:_ ~version:_ _perf -> ())
+    ; serverVersion = (fun _ -> ())
+    ; serverStatus = (fun _ -> ())
     }
 
 (* Main loop *)
 let lsp_cb ofn =
+  let send_notification nt =
+    Lsp.Base.Message.(Notification nt |> to_yojson) |> ofn
+  in
+  let trace = LIO.trace in
   let message ~lvl ~message =
     let lvl = Fleche.Io.Level.to_int lvl in
     LIO.logMessageInt ~lvl ~message
   in
+  let diagnostics ~uri ~version diags =
+    Lsp.JLang.mk_diagnostics ~uri ~version diags |> send_notification
+  in
+  let fileProgress ~uri ~version progress =
+    Lsp.JFleche.mk_progress ~uri ~version progress |> send_notification
+  in
+  let perfData ~uri ~version perf =
+    Lsp.JFleche.mk_perf ~uri ~version perf |> send_notification
+  in
+  let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> send_notification in
+  let serverStatus st = Lsp.JFleche.mk_serverStatus st |> send_notification in
   Fleche.Io.CallBack.
-    { trace = LIO.trace
+    { trace
     ; message
-    ; diagnostics =
-        (fun ~uri ~version diags ->
-          Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
-    ; fileProgress =
-        (fun ~uri ~version progress ->
-          Lsp.JFleche.mk_progress ~uri ~version progress |> ofn)
-    ; perfData =
-        (fun ~uri ~version perf ->
-          Lsp.JFleche.mk_perf ~uri ~version perf |> ofn)
+    ; diagnostics
+    ; fileProgress
+    ; perfData
+    ; serverVersion
+    ; serverStatus
     }
 
 let coq_init ~debug =
@@ -116,7 +133,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
   let json_fn = LIO.send_json Format.std_formatter in
 
   let ofn response =
-    let response = Lsp.Base.Response.to_yojson response in
+    let response = Lsp.Base.Message.to_yojson response in
     LIO.send_json Format.std_formatter response
   in