feat: use MonadIO in LSP communication
This commit is contained in:
Wojciech Nawrocki
Sebastian Ullrich
parent
c3b333b9e7
commit
cf3d6e8f5e
4 changed files with 97 additions and 142 deletions
|
|
@ -19,12 +19,12 @@ private def parseHeaderField (s : String) : Option (String × String) :=
|
|||
if s = "" ∨ s.takeRight 2 ≠ "\r\n" then
|
||||
none
|
||||
else
|
||||
let xs := (s.dropRight 2).splitOn ": ";
|
||||
let xs := (s.dropRight 2).splitOn ": "
|
||||
match xs with
|
||||
| [] => none
|
||||
| [_] => none
|
||||
| name :: value :: rest =>
|
||||
let value := ": ".intercalate (value :: rest);
|
||||
let value := ": ".intercalate (value :: rest)
|
||||
some ⟨name, value⟩
|
||||
|
||||
private partial def readHeaderFields (h : FS.Stream) : IO (List (String × String)) := do
|
||||
|
|
@ -47,36 +47,38 @@ private def readLspHeader (h : FS.Stream) : IO Nat := do
|
|||
| none => throw (userError ("Content-Length header value '" ++ length ++ "' is not a Nat"))
|
||||
| none => throw (userError ("no Content-Length header in header fields: " ++ toString fields))
|
||||
|
||||
def readLspMessage (h : FS.Stream) : IO Message := do
|
||||
variables {m : Type → Type} [Monad m] [MonadIO m]
|
||||
|
||||
def readLspMessage (h : FS.Stream) : m Message := do
|
||||
let nBytes ← readLspHeader h
|
||||
h.readMessage nBytes
|
||||
|
||||
def readLspRequestAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do
|
||||
def readLspRequestAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : m (Request α) := do
|
||||
let nBytes ← readLspHeader h
|
||||
h.readRequestAs nBytes expectedMethod α
|
||||
|
||||
def readLspNotificationAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO α := do
|
||||
def readLspNotificationAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : m α := do
|
||||
let nBytes ← readLspHeader h
|
||||
h.readNotificationAs nBytes expectedMethod α
|
||||
|
||||
def writeLspMessage (h : FS.Stream) (m : Message) : IO Unit := do
|
||||
def writeLspMessage (h : FS.Stream) (msg : Message) : m Unit := do
|
||||
-- inlined implementation instead of using jsonrpc's writeMessage
|
||||
-- to maintain the atomicity of putStr
|
||||
let j := (toJson m).compress
|
||||
let j := (toJson msg).compress
|
||||
let header := "Content-Length: " ++ toString j.utf8ByteSize ++ "\r\n\r\n"
|
||||
h.putStr (header ++ j)
|
||||
h.flush
|
||||
|
||||
def writeLspRequest {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (method : String) (params : α) : IO Unit :=
|
||||
def writeLspRequest {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (method : String) (params : α) : m Unit :=
|
||||
writeLspMessage h (Message.request id method (fromJson? (toJson params)))
|
||||
|
||||
def writeLspNotification {α : Type} [ToJson α] (h : FS.Stream) (method : String) (r : α) : IO Unit :=
|
||||
def writeLspNotification {α : Type} [ToJson α] (h : FS.Stream) (method : String) (r : α) : m Unit :=
|
||||
writeLspMessage h (Message.notification method (fromJson? (toJson r)))
|
||||
|
||||
def writeLspResponse {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
|
||||
def writeLspResponse {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : m Unit :=
|
||||
writeLspMessage h (Message.response id (toJson r))
|
||||
|
||||
def writeLspResponseError {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) (data : α) : IO Unit :=
|
||||
def writeLspResponseError {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) (data : α) : m Unit :=
|
||||
writeLspMessage h (Message.responseError id code message (toJson data))
|
||||
|
||||
end Lsp
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ import Std.Data.RBMap
|
|||
|
||||
import Lean.Environment
|
||||
import Lean.Server.Snapshots
|
||||
import Lean.Server.Utils
|
||||
import Lean.Data.Lsp
|
||||
import Lean.Data.Json.FromToJson
|
||||
|
||||
|
|
@ -187,25 +188,11 @@ fun st => st.docRef.get
|
|||
def updatePendingRequests (map : Array (Task (Except IO.Error Unit)) → Array (Task (Except IO.Error Unit))) : ServerM Unit :=
|
||||
fun st => st.pendingRequestsRef.modify map
|
||||
|
||||
def readLspMessage : ServerM JsonRpc.Message :=
|
||||
fun st => monadLift $ readLspMessage st.hIn
|
||||
|
||||
def readLspRequestAs (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM (Request α) :=
|
||||
fun st => monadLift $ readLspRequestAs st.hIn expectedMethod α
|
||||
|
||||
def readLspNotificationAs (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM α :=
|
||||
fun st => monadLift $ readLspNotificationAs st.hIn expectedMethod α
|
||||
|
||||
def writeLspNotification {α : Type*} [HasToJson α] (method : String) (params : α) : ServerM Unit :=
|
||||
fun st => monadLift $ writeLspNotification st.hOut method params
|
||||
|
||||
def writeLspResponse {α : Type*} [HasToJson α] (id : RequestID) (params : α) : ServerM Unit :=
|
||||
fun st => monadLift $ writeLspResponse st.hOut id params
|
||||
|
||||
/-- Clears diagnostics for the document version 'version'. -/
|
||||
-- TODO(WN): how to clear all diagnostics? Sending version 'none' doesn't seem to work
|
||||
def clearDiagnostics (uri : DocumentUri) (version : Nat) : ServerM Unit :=
|
||||
writeLspNotification "textDocument/publishDiagnostics"
|
||||
fun st =>
|
||||
writeLspNotification st.hOut "textDocument/publishDiagnostics"
|
||||
{ uri := uri,
|
||||
version? := version,
|
||||
diagnostics := #[] : PublishDiagnosticsParams }
|
||||
|
|
@ -225,13 +212,6 @@ let text := doc.text.toFileMap;
|
|||
newDoc ← compileDocument h doc.uri doc.version text;
|
||||
pure newDoc
|
||||
|
||||
private 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.bsize;
|
||||
(pre ++ newText ++ post).toFileMap
|
||||
|
||||
def handleDidChange (p : DidChangeTextDocumentParams) : ServerM Unit := do
|
||||
let docId := p.textDocument;
|
||||
let changes := p.contentChanges;
|
||||
|
|
@ -292,8 +272,9 @@ match method with
|
|||
|
||||
partial def mainLoop : Unit → ServerM Unit
|
||||
| () => do
|
||||
st ← read;
|
||||
-- TODO(MH): gracefully terminate when stdin is closed by watchdog?
|
||||
msg ← readLspMessage;
|
||||
msg ← readLspMessage st.hIn;
|
||||
-- TODO(MH): updatePendingRequests ...: get rid of all requests that are finished
|
||||
match msg with
|
||||
| Message.request id method (some params) => do
|
||||
|
|
@ -304,9 +285,9 @@ partial def mainLoop : Unit → ServerM Unit
|
|||
mainLoop ()
|
||||
| _ => throw (userError "got invalid JSON-RPC message")
|
||||
|
||||
def initAndRunServer (i o : FS.Stream) : IO Unit := do
|
||||
-- ignore InitializeParams for MWE
|
||||
initRequest ← Lsp.readLspRequestAs i "initialize" InitializeParams;
|
||||
def initAndRunWorker (i o : FS.Stream) : IO Unit := do
|
||||
-- TODO(WN): act in accordance with InitializeParams
|
||||
_ ← Lsp.readLspRequestAs i "initialize" InitializeParams;
|
||||
docRequest ← Lsp.readLspRequestAs i "textDocument/didOpen" DidOpenTextDocumentParams;
|
||||
doc ← openDocument o docRequest.param;
|
||||
docRef ← IO.mkRef doc;
|
||||
|
|
@ -315,3 +296,8 @@ runReader (mainLoop ()) (⟨i, o, docRef, pendingRequestsRef⟩ : ServerContext)
|
|||
|
||||
end Server
|
||||
end Lean
|
||||
|
||||
def main : IO Unit := do
|
||||
hIn ← IO.getStdin;
|
||||
hOut ← IO.getStdout;
|
||||
Lean.Server.initAndRunWorker hIn hOut
|
||||
|
|
|
|||
15
src/Lean/Server/Utils.lean
Normal file
15
src/Lean/Server/Utils.lean
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
import Lean.Data.Position
|
||||
import Lean.Data.Lsp
|
||||
|
||||
namespace Lean
|
||||
namespace Server
|
||||
|
||||
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.bsize;
|
||||
(pre ++ newText ++ post).toFileMap
|
||||
|
||||
end Server
|
||||
end Lean
|
||||
|
|
@ -11,6 +11,7 @@ import Lean.Elab.Import
|
|||
|
||||
import Lean.Data.Lsp
|
||||
import Lean.Server.HasFileSource
|
||||
import Lean.Server.Utils
|
||||
|
||||
/-!
|
||||
For general server architecture, see `README.md`. This module implements the watchdog process.
|
||||
|
|
@ -63,21 +64,7 @@ open Std (RBMap RBMap.empty)
|
|||
open Lsp
|
||||
open JsonRpc
|
||||
|
||||
private 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.bsize;
|
||||
(pre ++ newText ++ post).toFileMap
|
||||
|
||||
private def parsedImportsEndPos (input : String) : IO String.Pos := do
|
||||
env ← mkEmptyEnvironment;
|
||||
let fileName := "<input>";
|
||||
let inputCtx := Parser.mkInputContext input fileName;
|
||||
let (_, parserState, _) := Parser.parseHeader env inputCtx;
|
||||
pure parserState.pos
|
||||
|
||||
structure EditableDocument :=
|
||||
structure OpenDocument :=
|
||||
(version : Nat)
|
||||
(text : FileMap)
|
||||
(headerEndPos : String.Pos)
|
||||
|
|
@ -85,17 +72,11 @@ structure EditableDocument :=
|
|||
def workerCfg : Process.StdioConfig := ⟨Process.Stdio.piped, Process.Stdio.piped, Process.Stdio.piped⟩
|
||||
|
||||
structure FileWorker :=
|
||||
(doc : EditableDocument)
|
||||
(doc : OpenDocument)
|
||||
(proc : Process.Child workerCfg)
|
||||
|
||||
namespace FileWorker
|
||||
|
||||
def spawnArgs : Process.SpawnArgs := {workerCfg with cmd := "fileworker"}
|
||||
|
||||
def spawn (doc : EditableDocument) : IO FileWorker := do
|
||||
proc ← Process.spawn spawnArgs;
|
||||
pure ⟨doc, proc⟩
|
||||
|
||||
def stdin (fw : FileWorker) : FS.Stream :=
|
||||
FS.Stream.ofHandle fw.proc.stdin
|
||||
|
||||
|
|
@ -105,7 +86,7 @@ FS.Stream.ofHandle fw.proc.stdout
|
|||
def stderr (fw : FileWorker) : FS.Stream :=
|
||||
FS.Stream.ofHandle fw.proc.stderr
|
||||
|
||||
def wait (w : FileWorker) : IO Nat := pure 0
|
||||
def wait (fw : FileWorker) : IO Nat := pure 0 -- TODO
|
||||
|
||||
end FileWorker
|
||||
|
||||
|
|
@ -114,69 +95,26 @@ abbrev FileWorkerMap := RBMap DocumentUri FileWorker (fun a b => Decidable.decid
|
|||
structure ServerContext :=
|
||||
(hIn hOut : FS.Stream)
|
||||
(fileWorkersRef : IO.Ref FileWorkerMap)
|
||||
/- We store these to pass them to workers. -/
|
||||
(initParams : InitializeParams)
|
||||
(workerPath : String)
|
||||
|
||||
abbrev ServerM := ReaderT ServerContext IO
|
||||
|
||||
def updateFileWorkers (key : DocumentUri) (val : FileWorker) : ServerM Unit :=
|
||||
fun st => st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.insert key val)
|
||||
def spawnFileWorker (doc : OpenDocument) : ServerM FileWorker :=
|
||||
fun st => do
|
||||
proc ← Process.spawn {workerCfg with cmd := st.workerPath};
|
||||
pure ⟨doc, proc⟩
|
||||
|
||||
def findFileWorker (key : DocumentUri) : ServerM FileWorker :=
|
||||
def updateFileWorkers (uri : DocumentUri) (val : FileWorker) : ServerM Unit :=
|
||||
fun st => st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.insert uri val)
|
||||
|
||||
def findFileWorker (uri : DocumentUri) : ServerM FileWorker :=
|
||||
fun st => do
|
||||
fileWorkers ← st.fileWorkersRef.get;
|
||||
match fileWorkers.find? key with
|
||||
match fileWorkers.find? uri with
|
||||
| some fw => pure fw
|
||||
| none => throw (userError $ "got unknown document URI (" ++ key ++ ")")
|
||||
|
||||
def readWorkerLspMessage (key : DocumentUri) : ServerM JsonRpc.Message :=
|
||||
findFileWorker key >>= fun fw => monadLift $ readLspMessage fw.stdout
|
||||
|
||||
def readUserLspMessage : ServerM JsonRpc.Message :=
|
||||
fun st => monadLift $ readLspMessage st.hIn
|
||||
|
||||
def readWorkerLspRequestAs (key : DocumentUri) (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM (Request α) :=
|
||||
findFileWorker key >>= fun fw => monadLift $ readLspRequestAs fw.stdout expectedMethod α
|
||||
|
||||
def readUserLspRequestAs (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM (Request α) :=
|
||||
fun st => monadLift $ readLspRequestAs st.hIn expectedMethod α
|
||||
|
||||
def readWorkerLspNotificationAs (key : DocumentUri) (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM α :=
|
||||
findFileWorker key >>= fun fw => monadLift $ readLspNotificationAs fw.stdout expectedMethod α
|
||||
|
||||
def readUserLspNotificationAs (expectedMethod : String) (α : Type*) [HasFromJson α] : ServerM α :=
|
||||
fun st => monadLift $ readLspNotificationAs st.hIn expectedMethod α
|
||||
|
||||
def writeWorkerLspMessage (key : DocumentUri) (msg : JsonRpc.Message) : ServerM Unit :=
|
||||
findFileWorker key >>= fun fw => monadLift $ writeLspMessage fw.stdin msg
|
||||
|
||||
def writeUserLspMessage (msg : JsonRpc.Message) : ServerM Unit :=
|
||||
fun st => monadLift $ writeLspMessage st.hOut msg
|
||||
|
||||
def writeWorkerLspRequest {α : Type*} [HasToJson α] (key : DocumentUri) (id : RequestID) (method : String) (params : α) : ServerM Unit :=
|
||||
findFileWorker key >>= fun fw => monadLift $ writeLspRequest fw.stdin id method params
|
||||
|
||||
def writeUserLspRequest {α : Type*} [HasToJson α] (id : RequestID) (method : String) (params : α) : ServerM Unit :=
|
||||
fun st => monadLift $ writeLspRequest st.hOut id method params
|
||||
|
||||
def writeWorkerLspNotification {α : Type*} [HasToJson α] (key : DocumentUri) (method : String) (params : α) : ServerM Unit :=
|
||||
findFileWorker key >>= fun fw => monadLift $ writeLspNotification fw.stdin method params
|
||||
|
||||
def writeUserLspNotification {α : Type*} [HasToJson α] (method : String) (params : α) : ServerM Unit :=
|
||||
fun st => monadLift $ writeLspNotification st.hOut method params
|
||||
|
||||
def writeWorkerLspResponse {α : Type*} [HasToJson α] (key : DocumentUri) (id : RequestID) (params : α) : ServerM Unit :=
|
||||
findFileWorker key >>= fun fw => monadLift $ writeLspResponse fw.stdin id params
|
||||
|
||||
def writeUserLspResponse {α : Type*} [HasToJson α] (id : RequestID) (params : α) : ServerM Unit :=
|
||||
fun st => monadLift $ writeLspResponse st.hOut id params
|
||||
|
||||
def writeWorkerInitializeParams (key : DocumentUri) : ServerM Unit := do
|
||||
st ← read;
|
||||
writeWorkerLspRequest key (0 : Nat) "initialize" st.initParams
|
||||
|
||||
def writeWorkerDidOpenNotification (key : DocumentUri) : ServerM Unit := do
|
||||
findFileWorker key >>= fun fw => writeWorkerLspNotification key "textDocument/didOpen"
|
||||
(DidOpenTextDocumentParams.mk ⟨key, "lean", fw.doc.version, fw.doc.text.source⟩)
|
||||
| none => throw (userError $ "got unknown document URI (" ++ uri ++ ")")
|
||||
|
||||
def parseParams (paramType : Type*) [HasFromJson paramType] (params : Json) : ServerM paramType :=
|
||||
match fromJson? params with
|
||||
|
|
@ -190,17 +128,24 @@ partial def forwardFileWorkerPackets (fw : FileWorker) : Unit → ServerM Unit
|
|||
| ⟨⟩ => do
|
||||
-- TODO(MH): detect closed stream somehow and terminate gracefully
|
||||
-- TODO(MH): potentially catch unintended termination (e.g. due to stack overflow) and restart process
|
||||
msg ← monadLift $ readLspMessage fw.stdout;
|
||||
-- NOTE: Writes to Lean I/O streams are atomic, so we don't need to synchronise these in principle.
|
||||
writeUserLspMessage msg;
|
||||
msg ← readLspMessage fw.stdout;
|
||||
writeLspMessage fw.stdin msg;
|
||||
forwardFileWorkerPackets ⟨⟩
|
||||
|
||||
def startFileWorker (key : DocumentUri) (version : Nat) (text : FileMap) : ServerM Unit := do
|
||||
private def parsedImportsEndPos (input : String) : IO String.Pos := do
|
||||
emptyEnv ← mkEmptyEnvironment; -- TODO(WN): a lot of things could be purified if `mkEmptyEnvironment` was just a pure ctr
|
||||
let inputCtx := Parser.mkInputContext input "<input>";
|
||||
let (_, parserState, _) := Parser.parseHeader emptyEnv inputCtx;
|
||||
pure parserState.pos
|
||||
|
||||
def startFileWorker (uri : DocumentUri) (version : Nat) (text : FileMap) : ServerM Unit := do
|
||||
st ← read;
|
||||
pos ← monadLift $ parsedImportsEndPos text.source;
|
||||
fw ← monadLift $ FileWorker.spawn ⟨version, text, pos⟩;
|
||||
updateFileWorkers key fw;
|
||||
writeWorkerInitializeParams key;
|
||||
writeWorkerDidOpenNotification key;
|
||||
fw ← spawnFileWorker ⟨version, text, pos⟩;
|
||||
writeLspRequest fw.stdin (0 : Nat) "initialize" st.initParams;
|
||||
writeLspNotification fw.stdin "textDocument/didOpen"
|
||||
(DidOpenTextDocumentParams.mk ⟨uri, "lean", fw.doc.version, fw.doc.text.source⟩);
|
||||
updateFileWorkers uri fw;
|
||||
-- TODO(MH): replace with working IO variant
|
||||
-- TODO(MH): Sebastian said something about this better being implemented as threads
|
||||
-- (due to the long running nature of these tasks) but i did not yet have time to
|
||||
|
|
@ -242,9 +187,9 @@ else changes.forM $ fun change =>
|
|||
terminateFileWorker fw;
|
||||
startFileWorker doc.uri newVersion newDocText
|
||||
else
|
||||
let newDoc : EditableDocument := ⟨newVersion, newDocText, oldHeaderEndPos⟩;
|
||||
let newDoc : OpenDocument := ⟨newVersion, newDocText, oldHeaderEndPos⟩;
|
||||
updateFileWorkers doc.uri { fw with doc := newDoc };
|
||||
writeWorkerLspNotification doc.uri "textDocument/didChange" p
|
||||
writeLspNotification fw.stdin "textDocument/didChange" p
|
||||
| TextDocumentContentChangeEvent.fullChange (text : String) =>
|
||||
throw (userError "TODO impl computing the diff of two sources.")
|
||||
|
||||
|
|
@ -258,7 +203,8 @@ st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.erase doc.uri)
|
|||
def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do
|
||||
let h := (fun α [HasFromJson α] [HasToJson α] [HasFileSource α] => do
|
||||
parsedParams ← parseParams α params;
|
||||
writeWorkerLspRequest (fileSource parsedParams) id method parsedParams);
|
||||
fw ← findFileWorker $ fileSource parsedParams;
|
||||
writeLspRequest fw.stdin id method parsedParams);
|
||||
match method with
|
||||
| "textDocument/hover" => h HoverParams
|
||||
| _ => throw (userError $ "got unsupported request: " ++ method ++
|
||||
|
|
@ -267,7 +213,8 @@ match method with
|
|||
def handleNotification (method : String) (params : Json) : ServerM Unit := do
|
||||
let forward := (fun α [HasFromJson α] [HasToJson α] [HasFileSource α] => do
|
||||
parsedParams ← parseParams α params;
|
||||
writeWorkerLspNotification (fileSource parsedParams) method parsedParams);
|
||||
fw ← findFileWorker $ fileSource parsedParams;
|
||||
writeLspNotification fw.stdin method parsedParams);
|
||||
let handle := (fun α [HasFromJson α] (handler : α → ServerM Unit) => parseParams α params >>= handler);
|
||||
match method with
|
||||
| "textDocument/didOpen" => handle DidOpenTextDocumentParams handleDidOpen
|
||||
|
|
@ -278,10 +225,11 @@ match method with
|
|||
|
||||
partial def mainLoop : Unit → ServerM Unit
|
||||
| () => do
|
||||
msg ← readUserLspMessage;
|
||||
st ← read;
|
||||
msg ← readLspMessage st.hIn;
|
||||
match msg with
|
||||
| Message.request id "shutdown" _ =>
|
||||
writeUserLspResponse id (Json.null)
|
||||
writeLspResponse st.hOut id (Json.null)
|
||||
| Message.request id method (some params) => do
|
||||
handleRequest id method (toJson params);
|
||||
mainLoop ()
|
||||
|
|
@ -299,22 +247,26 @@ def mkLeanServerCapabilities : ServerCapabilities :=
|
|||
save? := none },
|
||||
hoverProvider := true }
|
||||
|
||||
def initAndRunServerAux : ServerM Unit := do
|
||||
st ← read;
|
||||
_ ← readLspNotificationAs st.hIn "initialized" InitializedParams;
|
||||
mainLoop ();
|
||||
Message.notification "exit" none ← readLspMessage st.hIn
|
||||
| throw (userError "Expected an Exit Notification.");
|
||||
pure ()
|
||||
|
||||
def initAndRunServer (i o : FS.Stream) : IO Unit := do
|
||||
some workerPath ← IO.getEnv "LEAN_WORKER_PATH"
|
||||
| throw $ userError "You need to specify LEAN_WORKER_PATH in the environment.";
|
||||
fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap);
|
||||
-- ignore InitializeParams for MWE
|
||||
initRequest ← readLspRequestAs i "initialize" InitializeParams;
|
||||
writeLspResponse o initRequest.id
|
||||
{ capabilities := mkLeanServerCapabilities,
|
||||
serverInfo? := some { name := "Lean 4 server",
|
||||
version? := "0.0.1" } : InitializeResult };
|
||||
runReader
|
||||
(do
|
||||
writeUserLspResponse initRequest.id
|
||||
{ capabilities := mkLeanServerCapabilities,
|
||||
serverInfo? := some { name := "Lean 4 server",
|
||||
version? := "0.0.1" } : InitializeResult };
|
||||
_ ← readUserLspNotificationAs "initialized" InitializedParams;
|
||||
mainLoop ();
|
||||
Message.notification "exit" none ← readUserLspMessage
|
||||
| throw (userError "Expected an Exit Notification.");
|
||||
pure ())
|
||||
(⟨i, o, fileWorkersRef, initRequest.param⟩ : ServerContext)
|
||||
initAndRunServerAux
|
||||
(⟨i, o, fileWorkersRef, initRequest.param, workerPath⟩ : ServerContext)
|
||||
|
||||
end Server
|
||||
end Lean
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue