package vsrocq-language-server

  1. Overview
  2. Docs
VSRocq language server

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (3)

Authors

  1. E
    Enrico Tassi
  2. M
    Maxime Dénès
  3. R
    Romain Tetley

Maintainers

  1. E
    Enrico Tassi <enrico.tassi@inria.fr>

Sources

vsrocq-language-server-2.3.3.tar.gz
md5=c3f17c36f162c6be3ed6f35a30e3a18d
sha512=32c67c0a915d0983332337d891ccc40d3204b04e83c8d307cffdda06df7798db8bedb74e705101d2c83d595cfb2e4f82ecbf576fe3c385ec7ead9689f50f7d05

doc/vsrocq-language-server.dm/Dm/Scheduler/index.html

Module Dm.SchedulerSource

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.

Sourcetype state

State for incremental schedule construction

Sourceval initial_state : state
Sourcetype error_recovery_strategy =
  1. | RSkip
  2. | RAdmitted
Sourcetype task =
  1. | Skip of {
    1. id : Types.sentence_id;
    2. error : Pp.t option;
    }
  2. | Block of {
    1. id : Types.sentence_id;
    2. synterp : Vernacstate.Synterp.t;
    3. error : Pp.t Loc.located;
    }
  3. | Exec of executable_sentence
  4. | OpaqueProof of {
    1. terminator : executable_sentence;
    2. opener_id : Types.sentence_id;
    3. proof_using : Vernacexpr.section_subset_expr;
    4. tasks : executable_sentence list;
    }
  5. | Query of executable_sentence
Sourcetype schedule

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

Sourceval initial_schedule : schedule
Sourceval schedule_errored_sentence : Types.sentence_id -> Pp.t Loc.located -> Vernacstate.Synterp.t -> schedule -> 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.

Sourceval 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

Computes what should be invalidated

Sourceval string_of_schedule : schedule -> string