Diagnostic Job

structure Lapis.Server.Diagnostics.DiagnosticJob : Type

State of a pending diagnostic job

• uri : Protocol.Types.DocumentUri

  Document URI

• version : Int

  Document version when job was scheduled

• cancelled : IO.Ref Bool

  Cancellation flag

• task : Task (Except IO.Error Unit)

  Task running the diagnostic computation

structure Lapis.Server.Diagnostics.DiagnosticsConfig : Type

Configuration for debounced diagnostics

• debounceMs : Nat

  Delay in milliseconds before running diagnostics

• source : Option String

  Source name for diagnostics

def Lapis.Server.Diagnostics.instInhabitedDiagnosticsConfig.default : DiagnosticsConfig

Equations

• Lapis.Server.Diagnostics.instInhabitedDiagnosticsConfig.default = { debounceMs := default, source := default }

instance Lapis.Server.Diagnostics.instInhabitedDiagnosticsConfig : Inhabited DiagnosticsConfig

Equations

• Lapis.Server.Diagnostics.instInhabitedDiagnosticsConfig = { default := Lapis.Server.Diagnostics.instInhabitedDiagnosticsConfig.default }

structure Lapis.Server.Diagnostics.DiagnosticsManager : Type

Manages debounced diagnostic publishing

• pendingJobs : IO.Ref (Std.HashMap String DiagnosticJob)

  Pending diagnostic jobs per URI

• config : DiagnosticsConfig

  Configuration

• outputChannel : Transport.OutputChannel

  Output channel for publishing

def Lapis.Server.Diagnostics.DiagnosticsManager.new (outputChannel : Transport.OutputChannel) (config : DiagnosticsConfig := { }) : IO DiagnosticsManager

Create a new diagnostics manager

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticsManager.cancel (dm : DiagnosticsManager) (uri : Protocol.Types.DocumentUri) : IO Unit

Cancel any pending diagnostic job for a URI

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticsManager.clear (dm : DiagnosticsManager) (uri : Protocol.Types.DocumentUri) : IO Unit

Clear diagnostics for a document

Equations

• dm.clear uri = do dm.cancel uri Lapis.Server.Diagnostics.DiagnosticsManager.publish✝ dm uri none #[]

def Lapis.Server.Diagnostics.DiagnosticsManager.schedule (dm : DiagnosticsManager) (uri : Protocol.Types.DocumentUri) (version : Int) (compute : IO (Array Protocol.Types.Diagnostic)) : IO Unit

Schedule diagnostics with debouncing

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticsManager.schedulePure (dm : DiagnosticsManager) (uri : Protocol.Types.DocumentUri) (version : Int) (diagnostics : Array Protocol.Types.Diagnostic) : IO Unit

Schedule diagnostics with a pure computation

Equations

• dm.schedulePure uri version diagnostics = dm.schedule uri version (pure diagnostics)

def Lapis.Server.Diagnostics.DiagnosticsManager.triggerImmediate (dm : DiagnosticsManager) (uri : Protocol.Types.DocumentUri) (version : Int) (compute : IO (Array Protocol.Types.Diagnostic)) : IO Unit

Trigger immediate diagnostics (no debounce)

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticsManager.flush (dm : DiagnosticsManager) : IO Unit

Wait for all pending diagnostic jobs to complete

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticsManager.cancelAll (dm : DiagnosticsManager) : IO Unit

Cancel all pending diagnostic jobs

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Server.Diagnostics.DiagnosticBuilder : Type

Builder for creating diagnostics

• diagnostics : Array Protocol.Types.Diagnostic
• source : Option String

def Lapis.Server.Diagnostics.DiagnosticBuilder.new (source : Option String := none) : DiagnosticBuilder

Create a new diagnostic builder

Equations

• Lapis.Server.Diagnostics.DiagnosticBuilder.new source = { diagnostics := #[], source := source }

def Lapis.Server.Diagnostics.DiagnosticBuilder.error (b : DiagnosticBuilder) (range : Protocol.Types.Range) (message : String) (code : Option String := none) : DiagnosticBuilder

Add an error diagnostic

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticBuilder.warning (b : DiagnosticBuilder) (range : Protocol.Types.Range) (message : String) (code : Option String := none) : DiagnosticBuilder

Add a warning diagnostic

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticBuilder.info (b : DiagnosticBuilder) (range : Protocol.Types.Range) (message : String) (code : Option String := none) : DiagnosticBuilder

Add an info diagnostic

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticBuilder.hint (b : DiagnosticBuilder) (range : Protocol.Types.Range) (message : String) (code : Option String := none) : DiagnosticBuilder

Add a hint diagnostic

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticBuilder.withTags (b : DiagnosticBuilder) (range : Protocol.Types.Range) (message : String) (severity : Protocol.Types.DiagnosticSeverity) (tags : Array Protocol.Types.DiagnosticTag) (code : Option String := none) : DiagnosticBuilder

Add a diagnostic with tags

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticBuilder.deprecated (b : DiagnosticBuilder) (range : Protocol.Types.Range) (message : String) : DiagnosticBuilder

Mark code as deprecated

Equations

• b.deprecated range message = b.withTags range message Lapis.Protocol.Types.DiagnosticSeverity.hint #[Lapis.Protocol.Types.DiagnosticTag.deprecated]

def Lapis.Server.Diagnostics.DiagnosticBuilder.unnecessary (b : DiagnosticBuilder) (range : Protocol.Types.Range) (message : String) : DiagnosticBuilder

Mark code as unnecessary

Equations

• b.unnecessary range message = b.withTags range message Lapis.Protocol.Types.DiagnosticSeverity.hint #[Lapis.Protocol.Types.DiagnosticTag.unnecessary]

def Lapis.Server.Diagnostics.DiagnosticBuilder.add (b : DiagnosticBuilder) (diag : Protocol.Types.Diagnostic) : DiagnosticBuilder

Add a custom diagnostic

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Diagnostics.DiagnosticBuilder.build (b : DiagnosticBuilder) : Array Protocol.Types.Diagnostic

Build the final diagnostic array

Equations

• b.build = b.diagnostics

def Lapis.Server.Diagnostics.mkError (range : Protocol.Types.Range) (message : String) (source : Option String := none) : Protocol.Types.Diagnostic

Create a single error diagnostic

Equations

• Lapis.Server.Diagnostics.mkError range message source = { range := range, severity := some Lapis.Protocol.Types.DiagnosticSeverity.error, source := source, message := message }

def Lapis.Server.Diagnostics.mkWarning (range : Protocol.Types.Range) (message : String) (source : Option String := none) : Protocol.Types.Diagnostic

Create a single warning diagnostic

Equations

• Lapis.Server.Diagnostics.mkWarning range message source = { range := range, severity := some Lapis.Protocol.Types.DiagnosticSeverity.warning, source := source, message := message }

def Lapis.Server.Diagnostics.mkInfo (range : Protocol.Types.Range) (message : String) (source : Option String := none) : Protocol.Types.Diagnostic

Create a single info diagnostic

Equations

• Lapis.Server.Diagnostics.mkInfo range message source = { range := range, severity := some Lapis.Protocol.Types.DiagnosticSeverity.information, source := source, message := message }

def Lapis.Server.Diagnostics.mkHint (range : Protocol.Types.Range) (message : String) (source : Option String := none) : Protocol.Types.Diagnostic

Create a single hint diagnostic

Equations

• Lapis.Server.Diagnostics.mkHint range message source = { range := range, severity := some Lapis.Protocol.Types.DiagnosticSeverity.hint, source := source, message := message }