-
Notifications
You must be signed in to change notification settings - Fork 350
/
Utils.lean
188 lines (163 loc) · 6.38 KB
/
Utils.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
/-
Copyright (c) 2020 Wojciech Nawrocki. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki, Marc Huisinga
-/
prelude
import Init.System.Uri
import Lean.Data.Lsp.Communication
import Lean.Data.Lsp.Diagnostics
import Lean.Data.Lsp.Extra
import Lean.Data.Lsp.TextSync
import Lean.Server.InfoUtils
namespace IO
/-- Throws an `IO.userError`. -/
def throwServerError (err : String) : IO α :=
throw (userError err)
namespace FS.Stream
/--
Chains two streams by creating a new stream s.t. writing to it
just writes to `a` but reading from it also duplicates the read output
into `b`, c.f. `a | tee b` on Unix.
NB: if `a` is written to but this stream is never read from,
the output will *not* be duplicated. Use this if you only care
about the data that was actually read.
-/
def chainRight (a : Stream) (b : Stream) (flushEagerly : Bool := false) : Stream :=
{ a with
flush := a.flush *> b.flush
read := fun sz => do
let bs ← a.read sz
b.write bs
if flushEagerly then b.flush
pure bs
getLine := do
let ln ← a.getLine
b.putStr ln
if flushEagerly then b.flush
pure ln }
/-- Like `tee a | b` on Unix. See `chainOut`. -/
def chainLeft (a : Stream) (b : Stream) (flushEagerly : Bool := false) : Stream :=
{ b with
flush := a.flush *> b.flush
write := fun bs => do
a.write bs
if flushEagerly then a.flush
b.write bs
putStr := fun s => do
a.putStr s
if flushEagerly then a.flush
b.putStr s }
/-- Prefixes all written outputs with `pre`. -/
def withPrefix (a : Stream) (pre : String) : Stream :=
{ a with
write := fun bs => do
a.putStr pre
a.write bs
putStr := fun s =>
a.putStr (pre ++ s) }
end FS.Stream
end IO
namespace Lean.Server
/-- Meta-Data of a document. -/
structure DocumentMeta where
/-- URI where the document is located. -/
uri : Lsp.DocumentUri
/-- Version number of the document. Incremented whenever the document is edited. -/
version : Nat
/-- Current text of the document. -/
text : FileMap
/--
Controls when dependencies of the document are built on `textDocument/didOpen` notifications.
-/
dependencyBuildMode : Lsp.DependencyBuildMode
deriving Inhabited
/-- Extracts an `InputContext` from `doc`. -/
def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
input := doc.text.source
fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
fileMap := doc.text
/--
Replaces the range `r` (using LSP UTF-16 positions) in `text` (using UTF-8 positions)
with `newText`.
-/
def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMap :=
let start := text.lspPosToUtf8Pos r.start
let «end» := text.lspPosToUtf8Pos r.«end»
let pre := text.source.extract 0 start
let post := text.source.extract «end» text.source.endPos
(pre ++ newText ++ post).toFileMap
open IO
/--
Duplicates an I/O stream to a log file `fName` in LEAN_SERVER_LOG_DIR
if that envvar is set.
-/
def maybeTee (fName : String) (isOut : Bool) (h : FS.Stream) : IO FS.Stream := do
match (← IO.getEnv "LEAN_SERVER_LOG_DIR") with
| none => pure h
| some logDir =>
IO.FS.createDirAll logDir
let hTee ← FS.Handle.mk (System.mkFilePath [logDir, fName]) FS.Mode.write
let hTee := FS.Stream.ofHandle hTee
pure $ if isOut then
hTee.chainLeft h true
else
h.chainRight hTee true
open Lsp
/-- Returns the document contents with the change applied. -/
def applyDocumentChange (oldText : FileMap) : (change : Lsp.TextDocumentContentChangeEvent) → FileMap
| TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) =>
replaceLspRange oldText range newText
| TextDocumentContentChangeEvent.fullChange (newText : String) =>
newText.toFileMap
/-- Returns the document contents with all changes applied. -/
def foldDocumentChanges (changes : Array Lsp.TextDocumentContentChangeEvent) (oldText : FileMap) : FileMap :=
changes.foldl applyDocumentChange oldText
/-- Constructs a `textDocument/publishDiagnostics` notification. -/
def mkPublishDiagnosticsNotification (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) :
JsonRpc.Notification Lsp.PublishDiagnosticsParams where
method := "textDocument/publishDiagnostics"
param := {
uri := m.uri
version? := some m.version
diagnostics := diagnostics
}
/-- Constructs a `$/lean/fileProgress` notification. -/
def mkFileProgressNotification (m : DocumentMeta) (processing : Array LeanFileProgressProcessingInfo) :
JsonRpc.Notification Lsp.LeanFileProgressParams where
method := "$/lean/fileProgress"
param := {
textDocument := { uri := m.uri, version? := m.version }
processing
}
/-- Constructs a `$/lean/fileProgress` notification from the given position onwards. -/
def mkFileProgressAtPosNotification (m : DocumentMeta) (pos : String.Pos)
(kind : LeanFileProgressKind := LeanFileProgressKind.processing) :
JsonRpc.Notification Lsp.LeanFileProgressParams :=
mkFileProgressNotification m #[{ range := ⟨m.text.utf8PosToLspPos pos, m.text.utf8PosToLspPos m.text.source.endPos⟩, kind := kind }]
/-- Constructs a `$/lean/fileProgress` notification marking processing as done. -/
def mkFileProgressDoneNotification (m : DocumentMeta) : JsonRpc.Notification Lsp.LeanFileProgressParams :=
mkFileProgressNotification m #[]
-- TODO: should return a request ID (or task?) when we add response handling
def mkApplyWorkspaceEditRequest (params : ApplyWorkspaceEditParams) :
JsonRpc.Request ApplyWorkspaceEditParams :=
⟨"workspace/applyEdit", "workspace/applyEdit", params⟩
end Lean.Server
/--
Converts an UTF-8-based `String.range` in `text` to an equivalent LSP UTF-16-based `Lsp.Range`
in `text`.
-/
def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) : Lean.Lsp.Range :=
⟨text.utf8PosToLspPos r.start, text.utf8PosToLspPos r.stop⟩
open Lean in
/--
Attempts to find a module name in the roots denoted by `srcSearchPath` for `uri`.
Fails if `uri` is not a `file://` uri or if the given `uri` cannot be found in `srcSearchPath`.
-/
def System.SearchPath.searchModuleNameOfUri
(srcSearchPath : SearchPath)
(uri : Lsp.DocumentUri)
: IO (Option Name) := do
let some path := Uri.fileUriToPath? uri
| return none
searchModuleNameOfFileName path srcSearchPath