package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Unicode_completion : sig ... end
type t = {
  1. mem_stats : bool;
    (*

    mem_stats Call Obj.reachable_words for every sentence. This is very slow and not very useful, so disabled by default

    *)
  2. gc_quick_stats : bool;
    (*

    gc_quick_stats Show the diff of Gc.quick_stats data for each sentence

    *)
  3. client_version : string;
  4. eager_diagnostics : bool;
    (*

    eager_diagnostics Send (full) diagnostics after processing each

    *)
  5. goal_after_tactic : bool;
    (*

    When showing goals and the cursor is in a tactic, if false, show goals before executing the tactic, if true, show goals after

    *)
  6. show_coq_info_messages : bool;
    (*

    Show `msg_info` messages in diagnostics

    *)
  7. show_notices_as_diagnostics : bool;
    (*

    Show `msg_notice` messages in diagnostics

    *)
  8. admit_on_bad_qed : bool;
    (*

    admit_on_bad_qed There are two possible error recovery strategies when a Qed fails: one is not to add the constant to the state, the other one is admit it. We find the second behavior more useful, but YMMV.

    *)
  9. debug : bool;
    (*

    Enable debug on Coq side, including backtraces

    *)
  10. unicode_completion : Unicode_completion.t;
  11. max_errors : int;
  12. pp_type : int;
    (*

    Pretty-printing type in Info Panel Request, 0 = string; 1 = Pp.t; 2 = Coq Layout Engine

    *)
  13. show_stats_on_hover : bool;
    (*

    Show stats on hover

    *)
  14. show_loc_info_on_hover : bool;
    (*

    Show loc info on hover

    *)
  15. show_universes_on_hover : bool;
    (*

    Show universe data on hover

    *)
  16. pp_json : bool;
    (*

    Whether to pretty print the protocol JSON on the wire

    *)
  17. send_perf_data : bool;
    (*

    Whether to send the perf data notification

    *)
  18. send_diags : bool;
    (*

    Whether to send the diagnostics notification

    *)
  19. verbosity : int;
    (*

    Verbosity, 1 = reduced, 2 = default. As of today reduced will disable all logging, and the diagnostics and perf_data notification

    *)
  20. check_only_on_request : bool;
    (*

    Experimental setting to check document lazily

    *)
  21. send_diags_extra_data : bool;
    (*

    Send extra diagnostic data on the `data` diagnostic field.

    *)
  22. send_serverStatus : bool;
    (*

    Send server status client notification to the client

    *)
}
val default : t
val v : t ref
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct