package vscoq-language-server
VSCoq language server
Install
Dune Dependency
Authors
Maintainers
Sources
vscoq-language-server-2.2.6.tar.gz
md5=f528c1760966ac10d48b5f1c5531411a
sha512=1f69538ae5f78854b34e3f1a9d408714843e899bb96d063c2bfac410339b6a13ee5f30d5e7b3cd2bbd673169bcfdb550153ba741092cdc3ee3a8ca6446cc2240
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 * Quickfix.t list option)) list
Source
val shift_overview :
state ->
before:RawDocument.t ->
after:RawDocument.t ->
start:int ->
offset:int ->
state
we know if it worked and we have the state in this process
we know if it worked but we do not have the state in this process
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 * state * prepared_task option * errored_sentence
Source
val execute :
state ->
Document.document ->
(Vernacstate.t * events * bool) ->
prepared_task ->
bool ->
prepared_task option * state * Vernacstate.t * events * errored_sentence
Coq toplevels for delegation without fork
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>