package vscoq-language-server
VSCoq language server
Install
Dune Dependency
Authors
Maintainers
Sources
vscoq-language-server-2.2.0.tar.gz
md5=1a5e8a51bc5c10d50055364c2d58ef24
sha512=f044284a187a11161740ea93be2d4ffe6a52db3e9e84fbd45b561dc1edd760ecf76a3792609f8e339aba637e1e6a417d47ecaee6a1d9a54d8352a38e9363ec8c
doc/vscoq-language-server.dm/Dm/ExecutionManager/index.html
Module Dm.ExecutionManager
Source
The event manager is in charge of the actual event of tasks (as defined by the scheduler), caching event states and invalidating them. It can delegate to worker processes via DelegationManager
Source
type options = {
delegation_mode : delegation_mode;
completion_options : Protocol.Settings.Completion.t;
enableDiagnostics : bool;
}
Execution state, includes the cache
Source
val invalidate :
Document.document ->
Scheduler.schedule ->
Types.sentence_id ->
state ->
state
Source
val all_errors :
state ->
(Types.sentence_id * (Loc.t option * Pp.t * Types.Quickfix.t list option))
list
Source
val shift_overview :
state ->
before:RawDocument.t ->
after:RawDocument.t ->
start:int ->
offset:int ->
state
Returns the vernac state after the sentence
Events for the main loop
Execution happens in two steps. In particular the event one takes only one task at a time to ease checking for interruption
Source
val build_tasks_for :
Document.document ->
Scheduler.schedule ->
state ->
Types.sentence_id ->
bool ->
Vernacstate.t * prepared_task list * state * Types.sentence_id option
Source
val execute :
state ->
(Vernacstate.t * events * bool) ->
prepared_task ->
state * Vernacstate.t * events * bool * errored_sentence
Source
val update_overview :
prepared_task ->
prepared_task list ->
state ->
Document.document ->
state
Coq toplevels for delegation without fork
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>