structure Lean.Lsp.WorkspaceFolder : Type

• uri : Lean.Lsp.DocumentUri
• name : String

instance Lean.Lsp.instToJsonWorkspaceFolder : Lean.ToJson Lean.Lsp.WorkspaceFolder

instance Lean.Lsp.instFromJsonWorkspaceFolder : Lean.FromJson Lean.Lsp.WorkspaceFolder

structure Lean.Lsp.FileSystemWatcher : Type

• globPattern : String
• kind : Option Nat

instance Lean.Lsp.instFromJsonFileSystemWatcher : Lean.FromJson Lean.Lsp.FileSystemWatcher

instance Lean.Lsp.instToJsonFileSystemWatcher : Lean.ToJson Lean.Lsp.FileSystemWatcher

def Lean.Lsp.FileSystemWatcher.create : Nat

def Lean.Lsp.FileSystemWatcher.change : Nat

def Lean.Lsp.FileSystemWatcher.delete : Nat

structure Lean.Lsp.DidChangeWatchedFilesRegistrationOptions : Type

• watchers : Array Lean.Lsp.FileSystemWatcher

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions : Lean.FromJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions

instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions : Lean.ToJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions

inductive Lean.Lsp.FileChangeType : Type

• Created: Lean.Lsp.FileChangeType
• Changed: Lean.Lsp.FileChangeType
• Deleted: Lean.Lsp.FileChangeType

instance Lean.Lsp.instFromJsonFileChangeType : Lean.FromJson Lean.Lsp.FileChangeType

instance Lean.Lsp.instToJsonFileChangeType : Lean.ToJson Lean.Lsp.FileChangeType

structure Lean.Lsp.FileEvent : Type

• uri : Lean.Lsp.DocumentUri
• type : Lean.Lsp.FileChangeType

instance Lean.Lsp.instFromJsonFileEvent : Lean.FromJson Lean.Lsp.FileEvent

instance Lean.Lsp.instToJsonFileEvent : Lean.ToJson Lean.Lsp.FileEvent

structure Lean.Lsp.DidChangeWatchedFilesParams : Type

• changes : Array Lean.Lsp.FileEvent

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams : Lean.FromJson Lean.Lsp.DidChangeWatchedFilesParams

instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams : Lean.ToJson Lean.Lsp.DidChangeWatchedFilesParams