Module Dm.CompletionItemsSource

Builtin commands, options, tactics, and attributes

Sourcetype builtin_syntax =
  1. | Literal of {
    1. value : string;
    2. subscript : string option;
    }
  2. | Reference of {
    1. value : string;
    2. subscript : string option;
    }
  3. | Alternative of {
    1. children : builtin_syntax list;
    }
  4. | Repeat of {
    1. min : int;
    2. max : int option;
    3. separator : string option;
    4. children : builtin_syntax list;
    }
Sourceval builtin_syntax_of_yojson : Yojson.Safe.t -> builtin_syntax
Sourceval pp_builtin_syntax : builtin_syntax -> string
Sourceval fold_gather : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
Sourceval builtin_syntax_to_snippet : int -> builtin_syntax -> int * string
Sourceval builtin_syntax_list_to_snippet : builtin_syntax list -> string
Sourcetype builtin_item_raw = {
  1. documentation_path : string;
  2. documentation_anchor : string;
  3. syntax : builtin_syntax list;
  4. documentation : string;
}
Sourceval builtin_item_raw_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> builtin_item_raw
Sourcetype builtin_item_kind =
  1. | Command
Sourcetype builtin_item = {
  1. raw : builtin_item_raw;
  2. label : string;
  3. kind : builtin_item_kind;
  4. snippet : string;
  5. documentation_url : string;
}
Sourceval doc_version : string
Sourceval documentation_url_of_item : builtin_item_raw -> string
Sourcetype builtin_index = builtin_item list
Sourcemodule BuiltinIndices : sig ... end

Completion items

Sourcetype completion_level =
  1. | Fully
  2. | Partially
  3. | No_completion
Sourceval symbol_prefix : completion_level option -> string
Sourcetype completion_item_lib = {
  1. ref : Names.GlobRef.t;
  2. path : Libnames.full_path;
  3. typ : Constr.types;
  4. env : Environ.env;
  5. sigma : Evd.evar_map;
  6. completes : completion_level option;
  7. mutable debug_info : string;
}
Sourcetype completion_item =
  1. | Library of completion_item_lib
  2. | Builtin of builtin_item
Sourceval mk_completion_item_lib : Evd.evar_map -> Names.GlobRef.t -> Environ.env -> Constr.constr -> completion_item_lib
Sourceval pp_completion_item_lib : completion_item_lib -> string * string * string * string * string