Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: cleanup imports in Lean.Lsp (#6523)
Browse files Browse the repository at this point in the history
This PR splits a definition out of `Lean.Lsp.Basic`, with the effect
that material about JSON is not needed for `Lean.Meta.Sorry` and its
dependencies.
kim-em authored Jan 4, 2025
1 parent 9080df3 commit 639e6e9
Showing 3 changed files with 26 additions and 5 deletions.
1 change: 1 addition & 0 deletions src/Lean/Data/Lsp.lean
Original file line number Diff line number Diff line change
@@ -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
5 changes: 0 additions & 5 deletions src/Lean/Data/Lsp/Basic.lean
Original file line number Diff line number Diff line change
@@ -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
25 changes: 25 additions & 0 deletions src/Lean/Data/Lsp/CancelParams.lean
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 639e6e9

Please sign in to comment.