| /- | |
| Copyright (c) 2020 Marc Huisinga. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Marc Huisinga | |
| -/ | |
| prelude | |
| import Lean.Data.Lsp | |
| namespace Lean.Lsp | |
| class FileSource (α : Type) where | |
| fileSource : α → DocumentUri | |
| export FileSource (fileSource) | |
| instance : FileSource Location := | |
| ⟨fun l => l.uri⟩ | |
| instance : FileSource TextDocumentIdentifier := | |
| ⟨fun i => i.uri⟩ | |
| instance : FileSource VersionedTextDocumentIdentifier := | |
| ⟨fun i => i.uri⟩ | |
| instance : FileSource TextDocumentEdit := | |
| ⟨fun e => fileSource e.textDocument⟩ | |
| instance : FileSource TextDocumentItem := | |
| ⟨fun i => i.uri⟩ | |
| instance : FileSource TextDocumentPositionParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource DidOpenTextDocumentParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource DidChangeTextDocumentParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource DidSaveTextDocumentParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource DidCloseTextDocumentParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource CompletionParams := | |
| ⟨fun h => fileSource h.toTextDocumentPositionParams⟩ | |
| instance : FileSource HoverParams := | |
| ⟨fun h => fileSource h.toTextDocumentPositionParams⟩ | |
| instance : FileSource DeclarationParams := | |
| ⟨fun h => fileSource h.toTextDocumentPositionParams⟩ | |
| instance : FileSource DefinitionParams := | |
| ⟨fun h => fileSource h.toTextDocumentPositionParams⟩ | |
| instance : FileSource TypeDefinitionParams := | |
| ⟨fun h => fileSource h.toTextDocumentPositionParams⟩ | |
| instance : FileSource ReferenceParams := | |
| ⟨fun h => fileSource h.toTextDocumentPositionParams⟩ | |
| instance : FileSource WaitForDiagnosticsParams := | |
| ⟨fun p => p.uri⟩ | |
| instance : FileSource DocumentHighlightParams := | |
| ⟨fun h => fileSource h.toTextDocumentPositionParams⟩ | |
| instance : FileSource DocumentSymbolParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource SemanticTokensParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource SemanticTokensRangeParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource FoldingRangeParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource PlainGoalParams := | |
| ⟨fun p => fileSource p.textDocument⟩ | |
| instance : FileSource PlainTermGoalParams where | |
| fileSource p := fileSource p.textDocument | |
| instance : FileSource RpcConnectParams where | |
| fileSource p := p.uri | |
| instance : FileSource RpcCallParams where | |
| fileSource p := fileSource p.textDocument | |
| instance : FileSource RpcReleaseParams where | |
| fileSource p := p.uri | |
| instance : FileSource RpcKeepAliveParams where | |
| fileSource p := p.uri | |
| instance : FileSource CodeActionParams where | |
| fileSource p := fileSource p.textDocument | |
| end Lean.Lsp |