package forester
A tool for tending mathematical forests
Install
dune-project
Dependency
Authors
Maintainers
Sources
5.0.tar.gz
md5=24f4aed96a8b8af33aba13fba66f1b37
sha512=d36b896aca11858bb4a00fc704c16cc27a1f197bdb3e479d6132fd70f70d67d7158096285cb0b6fb00db14417f0f822cc27fe65d82f0971e42378fd8271ce573
doc/src/forester.language_server/Publish.ml.html
Source file Publish.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
(* * SPDX-FileCopyrightText: 2024 The Forester Project Contributors AND The RedPRL Development Team * * SPDX-License-Identifier: GPL-3.0-or-later OR Apache-2.0 WITH LLVM-exception * *) open Forester_prelude open Forester_core open Forester_compiler open struct module L = Lsp.Types module Lsp_Diagnostic = Lsp.Types.Diagnostic module Broadcast = Lsp.Server_notification module RPC = Jsonrpc end type diagnostic = Reporter.Message.t Asai.Diagnostic.t type table = (Lsp.Uri.t, diagnostic list) Hashtbl.t let send packet = let server = Lsp_state.get () in LspEio.send server.lsp_io packet let (uri : L.DocumentUri.t) (message : Asai.Diagnostic.loctext) : L.DiagnosticRelatedInformation.t = let range = Lsp_shims.Loc.lsp_range_of_range message.loc in let location = L.Location.create ~uri ~range in let message = Asai.Diagnostic.string_of_text message.value in L.DiagnosticRelatedInformation.create ~location ~message let render_lsp_diagnostic (uri : L.DocumentUri.t) (diag : diagnostic) : Lsp_Diagnostic.t = let range = Lsp_shims.Loc.lsp_range_of_range diag.explanation.loc in let severity = Lsp_shims.Diagnostic.lsp_severity_of_severity @@ diag.severity in let code = `String (Reporter.Message.short_code diag.message) in let source = let Lsp_state.{forest; _} = Lsp_state.get () in let uri = URI_scheme.lsp_uri_to_uri ~base: forest.config.url uri in let@ doc = Option.map @~ Option.bind (State.find_opt forest uri) Tree.to_doc in Lsp.Text_document.text doc in let message = Asai.Diagnostic.string_of_text diag.explanation.value in let = Bwd.to_list @@ Bwd.map (render_lsp_related_info uri) diag.extra_remarks in Lsp_Diagnostic.create ~range ~severity ~code ?source ~message: (`String message) ~relatedInformation () let broadcast notif = let msg = Broadcast.to_jsonrpc notif in send @@ RPC.Packet.Notification msg let publish (uri : Lsp.Uri.t) (diagnostics : diagnostic list) = let diagnostics = List.map (render_lsp_diagnostic uri) diagnostics in let params = L.PublishDiagnosticsParams.create ~uri ~diagnostics () in broadcast @@ PublishDiagnostics params
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>