package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.5.8.16.tbz
sha256=5a0819d6ceb18cf031ece2c466eefd27f018d85c1c7472038bbb7c2663714b6e
sha512=be97b25db922014681dce75a68566b887f692c60208b698f03ce8b2fc0c1a2eab5c0c563d698eeb1d21dea5405468e958e67cce9a6c94a3106529f1b4ebfce13
doc/src/coq-lsp.coq/loader.ml.html
Source file loader.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 55 56 57(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) (************************************************************************) (* Coq serialization API/Plugin *) (* Copyright 2016-2019 MINES ParisTech *) (* Copyright 2019-2022 Inria *) (* Written by Emilio J. Gallego Arias *) (************************************************************************) [@@@ocamlformat "disable"] let list_last l = List.(nth l (length l - 1)) (* Should improve *) let map_serlib fl_pkg = let supported = match fl_pkg with (* Supported by serlib *) (* directory *) | "coq-core.plugins.cc" (* cc *) | "coq-core.plugins.extraction" (* extraction *) | "coq-core.plugins.firstorder" (* firstorder *) | "coq-core.plugins.funind" (* funind *) | "coq-core.plugins.ltac" (* ltac *) | "coq-core.plugins.ltac2" (* ltac2 *) | "coq-core.plugins.micromega" (* micromega *) | "coq-core.plugins.ring" (* ring *) | "coq-core.plugins.ssreflect" (* ssreflect *) | "coq-core.plugins.ssrmatching" (* ssrmatching *) | "coq-core.plugins.number_string_notation" (* syntax *) | "coq-core.plugins.tauto" (* tauto *) | "coq-core.plugins.zify" (* zify *) -> true | _ -> Feedback.msg_warning Pp.(str "Missing serlib plugin: " ++ str fl_pkg); false in if supported then let plugin_name = String.split_on_char '.' fl_pkg |> list_last in Some ("coq-serapi.serlib." ^ plugin_name) else None let plugin_handler user_loader = let loader = Option.default (Fl_dynload.load_packages ~debug:false) user_loader in fun fl_pkg -> let _, fl_pkg = Mltop.PluginSpec.repr fl_pkg in match map_serlib fl_pkg with | Some serlib_pkg -> loader [serlib_pkg] | None -> loader [fl_pkg]