package vscoq-language-server

You can search for identifiers within the package.

in-package search v0.2.0

vscoq-language-server.dm
- Dm
vscoq-language-server.language
- Language
  - Hover
vscoq-language-server.lsp
- Protocol

Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

type state

State for incremental schedule construction

val initial_state : state

type error_recovery_strategy =

| RSkip
| RAdmitted

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;

}

type task =

| Skip of {
1. id : Types.sentence_id;
2. error : Pp.t option;
}
| Exec of executable_sentence
| OpaqueProof of {
1. terminator : executable_sentence;
2. opener_id : Types.sentence_id;
3. proof_using : Vernacexpr.section_subset_expr;
4. tasks : executable_sentence list;
}
| Query of executable_sentence

type schedule

Holds the dependencies among sentences and a schedule to evaluate all sentences

val initial_schedule : schedule

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.

val task_for_sentence : 
  schedule ->
  Types.sentence_id ->
  Types.sentence_id option * task

Finds the task to be performed and the state on which the task should run

val dependents : schedule -> Types.sentence_id -> Types.sentence_id_set

Computes what should be invalidated

val string_of_schedule : schedule -> string