Documentation

Lean.Data.Lsp.Workspace

structure Lean.Lsp.WorkspaceFolder :

uri : DocumentUri
name : String

Instances For

instance Lean.Lsp.instToJsonWorkspaceFolder :

ToJson WorkspaceFolder

Equations

Lean.Lsp.instToJsonWorkspaceFolder = { toJson := Lean.Lsp.toJsonWorkspaceFolder✝ }

instance Lean.Lsp.instFromJsonWorkspaceFolder :

FromJson WorkspaceFolder

Equations

Lean.Lsp.instFromJsonWorkspaceFolder = { fromJson? := Lean.Lsp.fromJsonWorkspaceFolder✝ }

structure Lean.Lsp.FileSystemWatcher :

globPattern : String
kind : Option Nat

Instances For

instance Lean.Lsp.instFromJsonFileSystemWatcher :

FromJson FileSystemWatcher

Equations

Lean.Lsp.instFromJsonFileSystemWatcher = { fromJson? := Lean.Lsp.fromJsonFileSystemWatcher✝ }

instance Lean.Lsp.instToJsonFileSystemWatcher :

ToJson FileSystemWatcher

Equations

Lean.Lsp.instToJsonFileSystemWatcher = { toJson := Lean.Lsp.toJsonFileSystemWatcher✝ }

def Lean.Lsp.FileSystemWatcher.create :

Equations

Lean.Lsp.FileSystemWatcher.create = 1

Instances For

def Lean.Lsp.FileSystemWatcher.change :

Equations

Lean.Lsp.FileSystemWatcher.change = 2

Instances For

def Lean.Lsp.FileSystemWatcher.delete :

Equations

Lean.Lsp.FileSystemWatcher.delete = 4

Instances For

structure Lean.Lsp.DidChangeWatchedFilesRegistrationOptions :

watchers : Array FileSystemWatcher

Instances For

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions :

FromJson DidChangeWatchedFilesRegistrationOptions

Equations

Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions = { fromJson? := Lean.Lsp.fromJsonDidChangeWatchedFilesRegistrationOptions✝ }

instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions :

ToJson DidChangeWatchedFilesRegistrationOptions

Equations

Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions = { toJson := Lean.Lsp.toJsonDidChangeWatchedFilesRegistrationOptions✝ }

inductive Lean.Lsp.FileChangeType :

Created : FileChangeType
Changed : FileChangeType
Deleted : FileChangeType

Instances For

instance Lean.Lsp.instFromJsonFileChangeType :

FromJson FileChangeType

Equations

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

instance Lean.Lsp.instToJsonFileChangeType :

ToJson FileChangeType

Equations

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

structure Lean.Lsp.FileEvent :

uri : DocumentUri
type : FileChangeType

Instances For

instance Lean.Lsp.instFromJsonFileEvent :

FromJson FileEvent

Equations

Lean.Lsp.instFromJsonFileEvent = { fromJson? := Lean.Lsp.fromJsonFileEvent✝ }

instance Lean.Lsp.instToJsonFileEvent :

ToJson FileEvent

Equations

Lean.Lsp.instToJsonFileEvent = { toJson := Lean.Lsp.toJsonFileEvent✝ }

structure Lean.Lsp.DidChangeWatchedFilesParams :

changes : Array FileEvent

Instances For

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams :

FromJson DidChangeWatchedFilesParams

Equations

Lean.Lsp.instFromJsonDidChangeWatchedFilesParams = { fromJson? := Lean.Lsp.fromJsonDidChangeWatchedFilesParams✝ }

instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams :

ToJson DidChangeWatchedFilesParams

Equations

Lean.Lsp.instToJsonDidChangeWatchedFilesParams = { toJson := Lean.Lsp.toJsonDidChangeWatchedFilesParams✝ }