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/Scheduler/index.html
Module Dm.Scheduler
Source
The scheduler is the component in charge of planning the execution of sentences. It also defines the task delegation strategy, and computes dependencies between tasks. Scheduling can be done incrementally.
State for incremental schedule construction
Source
type executable_sentence = {
id : Types.sentence_id;
ast : Synterp.vernac_control_entry;
classif : Vernacextend.vernac_classification;
synterp : Vernacstate.Synterp.t;
error_recovery : error_recovery_strategy;
}
Source
type task =
| Skip of {
id : Types.sentence_id;
error : Pp.t option;
}
| Block of {
id : Types.sentence_id;
error : Pp.t Loc.located;
}
| Exec of executable_sentence
| OpaqueProof of {
terminator : executable_sentence;
opener_id : Types.sentence_id;
proof_using : Vernacexpr.section_subset_expr;
tasks : executable_sentence list;
}
| Query of executable_sentence
Holds the dependencies among sentences and a schedule to evaluate all sentences
Source
val schedule_sentence :
(Types.sentence_id
* (Synterp.vernac_control_entry
* Vernacextend.vernac_classification
* Vernacstate.Synterp.t)) ->
state ->
schedule ->
state * schedule
Identifies the structure of the document and dependencies between sentences in order to easily compute the tasks to interpret the a sentence. Input sentence is None on parsing error.
Finds the task to be performed and the state on which the task should run
Computes what should be invalidated
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>