rzk-0.11.3: An experimental proof assistant for synthetic ∞-categories
Safe HaskellNone
LanguageHaskell2010

Language.Rzk.VSCode.Env

Synopsis

Documentation

data RzkCachedModule Source #

What checking one module produced.

cachedModuleChecked is the state of the whole run after this module: the top-level scope and every declaration elaborated so far. That is what a resume starts from — a cached elaborated term names the definitions it uses by their foil name, which only means anything in the scope that produced it, so the scope has to be cached with them.

cachedModuleDecls is the rendered view of this module's own declarations, which is all that completion, symbols and hover need.

data ParseSource Source #

Where a parse came from, deciding whether it may be reused.

Constructors

ParsedFromBuffer Text

Parsed from the editor buffer with this text; reusable for the current file while the buffer text is unchanged.

ParsedFromDisk

Parsed from the file on disk; trusted until invalidated by a file-change notification.

ParseInvalidated

The file changed; must be re-parsed. The module is kept as the last good parse, which hover falls back to while the file fails to parse.

data ParsedModule Source #

A parse result for the reference index. A failed parse is a Nothing module and is not retried until the source changes.

data ReferenceIndexCache Source #

Constructors

ReferenceIndexCache 

Fields

data RzkEnv Source #

Constructors

RzkEnv 

Fields

spawnTypecheckWorker :: LSP () -> LSP () Source #

Run the given action (a project typecheck) on a fresh worker thread, cancelling the previous worker first. Cancellation waits for the old worker to stop, so it can no longer write to the caches once the new one starts. Typechecking runs on a worker so that the handler dispatch thread stays responsive: lsp dispatches messages sequentially, so a multi-second re-check run directly in a notification handler would block every later request (e.g. formatting on save).