package forester
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/Hover.ml.html
Source file Hover.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
(* * 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 Forester_frontend open Forester_search open State.Syntax open struct module L = Lsp.Types module T = Types let (let*) = Option.bind end let compute ({position; textDocument; _}: L.HoverParams.t) = let Lsp_state.{forest; _} = Lsp_state.get () in let render = Plain_text_client.string_of_content ~forest in let uri = URI_scheme.lsp_uri_to_uri ~base: forest.config.url textDocument.uri in let@ content = Option.map @~ match forest.={uri} with | None -> Reporter.fatal Internal_error ~extra_remarks: [Asai.Diagnostic.loctextf "%a is not in the index" URI.pp uri] | Some tree -> let* {nodes; _} = Tree.to_code tree in let* node = Analysis.node_at_code ~position nodes in let tree_under_cursor = let* {value = addr; _} = Analysis.extract_addr node in let uri_under_cursor = URI_scheme.named_uri ~base: forest.config.url addr in State.get_article uri_under_cursor forest in match tree_under_cursor with | Some article -> Some (render article.mainmatter) | None -> let* doc = Tree.to_doc tree in let* search_term = Analysis.word_at ~position doc in let results = List.map snd @@ Index.search forest.search_index search_term in Some Format.(asprintf "Relevant results:@.%a@." (pp_print_list ~pp_sep: (fun out () -> fprintf out "@.") URI.pp) results) in L.Hover.create ~contents: (`MarkupContent {kind = L.MarkupKind.Markdown; value = content}) ()
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>