diff --git a/CHANGES.md b/CHANGES.md index 71e7c3f57..88122cf95 100644 --- a/CHANGES.md +++ b/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 ----------------------------- diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 1cbf27145..aa593abb0 100644 --- a/controller/lsp_core.ml +++ b/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 diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index f4165b36c..f5065a9b3 100644 --- a/editor/code/lib/types.ts +++ b/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; +} diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index ecf292e90..0e436a21e 100644 --- a/editor/code/src/client.ts +++ b/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( + "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 diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index 1b933a801..c3e303b41 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -354,6 +354,18 @@ const coqPerfData : NotificationType> 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` diff --git a/fleche/theory.ml b/fleche/theory.ml index 29f4f8276..2c25f7ef7 100644 --- a/fleche/theory.ml +++ b/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 = diff --git a/fleche/theory.mli b/fleche/theory.mli index 33bbb8964..e20c2cf78 100644 --- a/fleche/theory.mli +++ b/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 *) diff --git a/lsp/jLang.mli b/lsp/jLang.mli index 0ddf3d1ac..73f2df3a1 100644 --- a/lsp/jLang.mli +++ b/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 :