package forester

  1. Overview
  2. Docs
A tool for tending mathematical forests

Install

Dune Dependency

Authors

Maintainers

Sources

5.0.tar.gz
md5=24f4aed96a8b8af33aba13fba66f1b37
sha512=d36b896aca11858bb4a00fc704c16cc27a1f197bdb3e479d6132fd70f70d67d7158096285cb0b6fb00db14417f0f822cc27fe65d82f0971e42378fd8271ce573

doc/src/forester.language_server/Diagnostics.ml.html

Source file Diagnostics.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
(*
 * 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
 *
 *)

(* When computing the diagnostics for a specific text document, do we know that
   the emitted diagnostics should be reported to the same URI?
   *)

open Forester_core
open Forester_compiler

open struct module L = Lsp.Types end
open State.Syntax

let compute (document : Lsp.Text_document.t) =
  let Lsp_state.{forest; _} = Lsp_state.get () in
  let lsp_uri = Lsp.Text_document.documentUri document in
  let uri = URI_scheme.lsp_uri_to_uri ~base: forest.config.url lsp_uri in
  match forest.?{uri} with
  | [] ->
    Eio.traceln "Clearing diagnostics for %s" (Lsp.Uri.to_path lsp_uri);
    Publish.publish lsp_uri []
  | diagnostics ->
    Eio.traceln "publishing %i diagnostics to %s" (List.length diagnostics) (Lsp.Uri.to_path lsp_uri);
    Publish.publish lsp_uri diagnostics
OCaml

Innovation. Community. Security.