diff --git a/src/Lean/Data/Lsp.lean b/src/Lean/Data/Lsp.lean index 441d4e82fc..8d3c7daf26 100644 --- a/src/Lean/Data/Lsp.lean +++ b/src/Lean/Data/Lsp.lean @@ -6,6 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude import Lean.Data.Lsp.Basic +import Lean.Data.Lsp.CancelParams import Lean.Data.Lsp.Capabilities import Lean.Data.Lsp.Client import Lean.Data.Lsp.Communication diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index 55fb5dd8ab..a9aaa93c1e 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -6,7 +6,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude import Lean.Data.Json -import Lean.Data.JsonRpc /-! Defines most of the 'Basic Structures' in the LSP specification (https://microsoft.github.io/language-server-protocol/specifications/specification-current/), @@ -19,10 +18,6 @@ namespace Lsp open Json -structure CancelParams where - id : JsonRpc.RequestID - deriving Inhabited, BEq, ToJson, FromJson - abbrev DocumentUri := String /-- We adopt the convention that zero-based UTF-16 positions as sent by LSP clients diff --git a/src/Lean/Data/Lsp/CancelParams.lean b/src/Lean/Data/Lsp/CancelParams.lean new file mode 100644 index 0000000000..84e95838b4 --- /dev/null +++ b/src/Lean/Data/Lsp/CancelParams.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2020 Marc Huisinga. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Marc Huisinga, Wojciech Nawrocki +-/ +prelude +import Lean.Data.JsonRpc + +/-! # Defines `Lean.Lsp.CancelParams`. + +This is separate from `Lean.Data.Lsp.Basic` to reduce transitive dependencies. +-/ + +namespace Lean +namespace Lsp + +open Json + +structure CancelParams where + id : JsonRpc.RequestID + deriving Inhabited, BEq, ToJson, FromJson + +end Lsp +end Lean