Documentation

Lean.Data.Lsp.Workspace

structure Lean.Lsp.WorkspaceFolder :

Type

uri : Lean.Lsp.DocumentUri
name : String

instance Lean.Lsp.instFromJsonWorkspaceFolder :

Lean.FromJson Lean.Lsp.WorkspaceFolder

Equations

Lean.Lsp.instFromJsonWorkspaceFolder = { fromJson? := [anonymous] }

instance Lean.Lsp.instToJsonWorkspaceFolder :

Lean.ToJson Lean.Lsp.WorkspaceFolder

Equations

Lean.Lsp.instToJsonWorkspaceFolder = { toJson := [anonymous] }

structure Lean.Lsp.FileSystemWatcher :

Type

globPattern : String
kind : Option Nat

instance Lean.Lsp.instToJsonFileSystemWatcher :

Lean.ToJson Lean.Lsp.FileSystemWatcher

Equations

Lean.Lsp.instToJsonFileSystemWatcher = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonFileSystemWatcher :

Lean.FromJson Lean.Lsp.FileSystemWatcher

Equations

Lean.Lsp.instFromJsonFileSystemWatcher = { fromJson? := [anonymous] }

def Lean.Lsp.FileSystemWatcher.create :

Equations

Lean.Lsp.FileSystemWatcher.create = 1

def Lean.Lsp.FileSystemWatcher.change :

Equations

Lean.Lsp.FileSystemWatcher.change = 2

def Lean.Lsp.FileSystemWatcher.delete :

Equations

Lean.Lsp.FileSystemWatcher.delete = 4

structure Lean.Lsp.DidChangeWatchedFilesRegistrationOptions :

Type

watchers : Array Lean.Lsp.FileSystemWatcher

instance Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions :

Lean.ToJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions

Equations

Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions :

Lean.FromJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions

Equations

Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions = { fromJson? := [anonymous] }

inductive Lean.Lsp.FileChangeType :

Type

instance Lean.Lsp.instFromJsonFileChangeType :

Lean.FromJson Lean.Lsp.FileChangeType

Equations

Lean.Lsp.instFromJsonFileChangeType = { fromJson? := fun j => do let a ← Lean.fromJson? j match a with | 1 => pure Lean.Lsp.FileChangeType.Created | 2 => pure Lean.Lsp.FileChangeType.Changed | 3 => pure Lean.Lsp.FileChangeType.Deleted | x => throw (toString "expected 1, 2, or 3, got " ++ toString j ++ toString "") }

instance Lean.Lsp.instToJsonFileChangeType :

Lean.ToJson Lean.Lsp.FileChangeType

Equations

Lean.Lsp.instToJsonFileChangeType = { toJson := fun x => match x with | Lean.Lsp.FileChangeType.Created => Lean.toJson 1 | Lean.Lsp.FileChangeType.Changed => Lean.toJson 2 | Lean.Lsp.FileChangeType.Deleted => Lean.toJson 3 }

structure Lean.Lsp.FileEvent :

Type

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

instance Lean.Lsp.instFromJsonFileEvent :

Lean.FromJson Lean.Lsp.FileEvent

Equations

Lean.Lsp.instFromJsonFileEvent = { fromJson? := [anonymous] }

instance Lean.Lsp.instToJsonFileEvent :

Lean.ToJson Lean.Lsp.FileEvent

Equations

Lean.Lsp.instToJsonFileEvent = { toJson := [anonymous] }

structure Lean.Lsp.DidChangeWatchedFilesParams :

Type

changes : Array Lean.Lsp.FileEvent

instance Lean.Lsp.instFromJsonDidChangeWatchedFilesParams :

Lean.FromJson Lean.Lsp.DidChangeWatchedFilesParams

Equations

Lean.Lsp.instFromJsonDidChangeWatchedFilesParams = { fromJson? := [anonymous] }

instance Lean.Lsp.instToJsonDidChangeWatchedFilesParams :

Lean.ToJson Lean.Lsp.DidChangeWatchedFilesParams

Equations

Lean.Lsp.instToJsonDidChangeWatchedFilesParams = { toJson := [anonymous] }