chore: cleanup imports in Lean.Lsp

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

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

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