[fleche] Auto-check documents on scroll when in lazy mode.

We introduce a new `coq/viewRange` notification, from client to
server, than hints the scheduler about the visible area of the
document.

Combined with the new lazy checking mode, this provides
checking on scroll, a feature inspired from Isabelle
IDE.

CHANGES.md

@@ -130,6 +130,10 @@
    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, #715)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

controller/lsp_core.ml

@@ -411,6 +411,17 @@ let do_cancel ~ofn ~params =
 
 let do_cache_trim () = Nt_cache_trim.notification ()
 
+let do_viewRange params =
+  match List.assoc "range" params |> Lsp.JLang.Diagnostic.Range.of_yojson with
+  | Ok range ->
+    let { Lsp.JLang.Diagnostic.Range.end_ = { line; character }; _ } = range in
+    let message = Format.asprintf "l: %d c:%d" line character in
+    LIO.trace "viewRange" message;
+    let uri = Helpers.get_uri params in
+    Fleche.Theory.Check.set_scheduler_hint ~uri ~point:(line, character);
+    ()
+  | Error err -> LIO.trace "viewRange" ("error in parsing notification: " ^ err)
+
 let do_changeConfiguration params =
   let message = "didChangeReceived" in
   let () = LIO.(logMessage ~lvl:Lvl.Info ~message) in
@@ -496,6 +507,7 @@ let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit =
   | "textDocument/didClose" -> do_close ~ofn params
   | "textDocument/didSave" -> Cache.save_to_disk ()
   (* Specific to coq-lsp *)
+  | "coq/viewRange" -> do_viewRange params
   | "coq/trimCaches" -> do_cache_trim ()
   (* Cancel Request *)
   | "$/cancelRequest" -> do_cancel ~ofn ~params

editor/code/lib/types.ts

@@ -179,3 +179,8 @@ export type PerfMessagePayload = PerfUpdate | PerfReset;
 export interface PerfMessageEvent extends MessageEvent {
   data: PerfMessagePayload;
 }
+
+export interface ViewRangeParams {
+  textDocument: VersionedTextDocumentIdentifier;
+  range: Range;
+}

editor/code/src/client.ts

@@ -14,6 +14,7 @@ import {
   Disposable,
   languages,
   Uri,
+  TextEditorVisibleRangesChangeEvent,
 } from "vscode";
 
 import * as vscode from "vscode";
@@ -37,6 +38,7 @@ import {
   GoalAnswer,
   PpString,
   DocumentPerfParams,
+  ViewRangeParams,
 } from "../lib/types";
 
 import { CoqLspClientConfig, CoqLspServerConfig, CoqSelector } from "./config";
@@ -45,6 +47,7 @@ import { FileProgressManager } from "./progress";
 import { coqPerfData, PerfDataView } from "./perf";
 import { sentenceNext, sentenceBack } from "./edit";
 import { HeatMap, HeatMapConfig } from "./heatmap";
+import { debounce, throttle } from "throttle-debounce";
 
 // Convert perf data to VSCode format
 function toVsCodePerf(
@@ -314,6 +317,28 @@ export function activateCoqLSP(
 
   context.subscriptions.push(goalsHook);
 
+  const viewRangeNotification = new NotificationType<ViewRangeParams>(
+    "coq/viewRange"
+  );
+
+  let viewRangeHook = window.onDidChangeTextEditorVisibleRanges(
+    throttle(400, (evt: TextEditorVisibleRangesChangeEvent) => {
+      if (
+        languages.match(CoqSelector.local, evt.textEditor.document) > 0 &&
+        evt.visibleRanges[0]
+      ) {
+        let uri = evt.textEditor.document.uri.toString();
+        let version = evt.textEditor.document.version;
+        let textDocument = { uri, version };
+        let range = client.code2ProtocolConverter.asRange(evt.visibleRanges[0]);
+        let params: ViewRangeParams = { textDocument, range };
+        client.sendNotification(viewRangeNotification, params);
+      }
+    })
+  );
+
+  context.subscriptions.push(viewRangeHook);
+
   // Heatmap setup
   heatMap = new HeatMap(
     workspace.getConfiguration("coq-lsp").get("heatmap") as HeatMapConfig

etc/doc/PROTOCOL.md

@@ -354,6 +354,18 @@ const coqPerfData : NotificationType<DocumentPerfParams<Range>>
 The `coq/trimCaches` notification from client to server tells the
 server to free memory. It has no parameters.
 
+### Viewport notification
+
+The `coq/viewRange` notification from client to server tells the
+server the visible range of the user.
+
+```typescript
+interface ViewRangeParams {
+  textDocument: VersionedTextDocumentIdentifier;
+  range: Range;
+}
+```
+
 ### Did Change Configuration and Server Configuration parameters
 
 The server will listen to the `workspace/didChangeConfiguration`

fleche/theory.ml

@@ -194,6 +194,8 @@ module Check : sig
 
   val maybe_check :
     io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option
+
+  val set_scheduler_hint : uri:Lang.LUri.File.t -> point:int * int -> unit
 end = struct
   let pending = ref []
 
@@ -214,9 +216,18 @@ end = struct
       | None -> pend_try f tt
       | Some r -> Some r)
 
+  let hint : (int * int) option ref = ref None
+
   let get_check_target pt_requests =
     let target_of_pt_handle (_, (l, c)) = Doc.Target.Position (l, c) in
-    Option.map target_of_pt_handle (List.nth_opt pt_requests 0)
+    match Option.map target_of_pt_handle (List.nth_opt pt_requests 0) with
+    | None ->
+      Option.map
+        (fun (l, c) ->
+          hint := None;
+          Doc.Target.Position (l, c))
+        !hint
+    | Some t -> Some t
 
   (* Notification handling; reply is optional / asynchronous *)
   let check ~io ~token ~uri =
@@ -255,6 +266,12 @@ end = struct
 
   let deschedule ~uri =
     pending := CList.remove Lang.LUri.File.equal uri !pending
+
+  let set_scheduler_hint ~uri ~point =
+    if CList.is_empty !pending then
+      let () = hint := Some point in
+      schedule ~uri (* if the hint is set we wanna override it *)
+    else if not (Option.is_empty !hint) then hint := Some point
 end
 
 let create ~io ~token ~env ~uri ~raw ~version =

fleche/theory.mli

@@ -21,6 +21,8 @@ module Check : sig
       progress and diagnostics notifications using output function [ofn]. *)
   val maybe_check :
     io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option
+
+  val set_scheduler_hint : uri:Lang.LUri.File.t -> point:int * int -> unit
 end
 
 (** Create a document inside a theory *)

lsp/jLang.mli

@@ -21,6 +21,22 @@ end
 
 module Diagnostic : sig
   type t = Lang.Diagnostic.t [@@deriving to_yojson]
+
+  module Point : sig
+    type t =
+      { line : int
+      ; character : int
+      }
+    [@@deriving yojson]
+  end
+
+  module Range : sig
+    type t =
+      { start : Point.t
+      ; end_ : Point.t [@key "end"]
+      }
+    [@@deriving yojson]
+  end
 end
 
 val mk_diagnostics :