diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index dcfaa27f1c..68ef3842c5 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -12,10 +12,57 @@ inductive RequestID
 | num (n : JsonNumber)
 | null
 
+-- TODO maybe put this in Json ns?
 inductive Structured
 | arr (elems : Array Json)
 | obj (kvPairs : RBNode String (fun _ => Json))
 
+/-- Error codes defined by JSON-RPC and LSP. -/
+inductive ErrorCode
+| parseError
+| invalidRequest
+| methodNotFound
+| invalidParams
+| internalError
+| serverErrorStart
+| serverErrorEnd
+| serverNotInitialized
+| unknownErrorCode
+-- LSP-specific codes below.
+| requestCancelled
+| contentModified
+
+instance hasFromJsonErrorCode : HasFromJson ErrorCode :=
+⟨fun j => match j with
+  | num n =>
+    if      n = (-32700 : Int) then ErrorCode.parseError
+    else if n = (-32600 : Int) then ErrorCode.invalidRequest
+    else if n = (-32601 : Int) then ErrorCode.methodNotFound
+    else if n = (-32602 : Int) then ErrorCode.invalidParams
+    else if n = (-32603 : Int) then ErrorCode.internalError
+    else if n = (-32099 : Int) then ErrorCode.serverErrorStart
+    else if n = (-32000 : Int) then ErrorCode.serverErrorEnd
+    else if n = (-32002 : Int) then ErrorCode.serverNotInitialized
+    else if n = (-32001 : Int) then ErrorCode.unknownErrorCode
+    else if n = (-32800 : Int) then ErrorCode.requestCancelled
+    else if n = (-32801 : Int) then ErrorCode.contentModified
+    else none
+  | _ => none⟩
+
+instance hasToJsonErrorCode : HasToJson ErrorCode :=
+⟨fun e => match e with
+  | ErrorCode.parseError           => (-32700 : Int)
+  | ErrorCode.invalidRequest       => (-32600 : Int)
+  | ErrorCode.methodNotFound       => (-32601 : Int)
+  | ErrorCode.invalidParams        => (-32602 : Int)
+  | ErrorCode.internalError        => (-32603 : Int)
+  | ErrorCode.serverErrorStart     => (-32099 : Int)
+  | ErrorCode.serverErrorEnd       => (-32000 : Int)
+  | ErrorCode.serverNotInitialized => (-32002 : Int)
+  | ErrorCode.unknownErrorCode     => (-32001 : Int)
+  | ErrorCode.requestCancelled     => (-32800 : Int)
+  | ErrorCode.contentModified      => (-32801 : Int)⟩
+
 -- uses Option Structured because users will likely rarely distinguish between an empty
 -- parameter array and an omitted params field.
 -- uses seperate constructors for notifications and errors because client and server
@@ -24,7 +71,7 @@ inductive Message
 | request (id : RequestID) (method : String) (params? : Option Structured)
 | requestNotification (method : String) (params? : Option Structured)
 | response (id : RequestID) (result : Json)
-| responseError (id : RequestID) (code : JsonNumber) (message : String) (data? : Option Json)
+| responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json)
 
 def Batch := Array Message
 
@@ -44,8 +91,9 @@ instance requestIDToJson : HasToJson RequestID :=
   | RequestID.str s => s
   | RequestID.num n => num n
   | RequestID.null  => null⟩
+
 instance requestIDFromJson : HasFromJson RequestID :=
-⟨fun j => match j with 
+⟨fun j => match j with
   | str s => RequestID.str s
   | num n => RequestID.num n
   | _     => none⟩
@@ -54,6 +102,7 @@ instance structuredToJson : HasToJson Structured :=
 ⟨fun s => match s with
   | Structured.arr a => arr a
   | Structured.obj o => obj o⟩
+
 instance structuredFromJson : HasFromJson Structured :=
 ⟨fun j => match j with
   | arr a => Structured.arr a
@@ -61,7 +110,7 @@ instance structuredFromJson : HasFromJson Structured :=
   | _     => none⟩
 
 instance messageToJson : HasToJson Message :=
-⟨fun m =>   
+⟨fun m =>
   mkObj $ ⟨"jsonrpc", "2.0"⟩ :: match m with
   | Message.request id method params? =>
     [⟨"id", toJson id⟩, ⟨"method", method⟩] ++ opt "params" params?
@@ -70,8 +119,8 @@ instance messageToJson : HasToJson Message :=
   | Message.response id result =>
     [⟨"id", toJson id⟩, ⟨"result", result⟩]
   | Message.responseError id code message data? =>
-    [⟨"id", toJson id⟩, 
-     ⟨"error", mkObj $ 
+    [⟨"id", toJson id⟩,
+     ⟨"error", mkObj $
        [⟨"code", toJson code⟩, ⟨"message", message⟩] ++ opt "data" data?⟩]⟩
 
 def aux1 (j : Json) : Option Message := do
@@ -93,7 +142,7 @@ pure (Message.response id result)
 def aux4 (j : Json) : Option Message := do
 id ← j.getObjValAs? RequestID "id";
 err ← j.getObjVal? "error";
-code ← err.getObjValAs? JsonNumber "code";
+code ← err.getObjValAs? ErrorCode "code";
 message ← err.getObjValAs? String "message";
 let data? := err.getObjVal? "data";
 pure (Message.responseError id code message data?)
@@ -123,7 +172,7 @@ match m with
 | Message.request id method params? =>
   if method = expectedMethod then
     match params? with
-    | some params => 
+    | some params =>
       let j := toJson params;
       match fromJson? j with
       | some v => pure ⟨id, v⟩
@@ -139,7 +188,7 @@ match m with
 | Message.requestNotification method params? =>
   if method = expectedMethod then
     match params? with
-    | some params => 
+    | some params =>
       let j := toJson params;
       match fromJson? j with
       | some v => pure v
diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean
index db9e8b8e76..79a4ea6e52 100644
--- a/src/Lean/Data/Lsp/Capabilities.lean
+++ b/src/Lean/Data/Lsp/Capabilities.lean
@@ -7,21 +7,23 @@ open Lean
 open Lean.Json
 open Lean.JsonRpc
 
--- TODO: right now we ignore the capabilities
+-- TODO: right now we ignore the client's capabilities
 inductive ClientCapabilities | mk
 
--- largely unimplemented
-structure ServerCapabilities :=
-(textDocumentSync? : Option TextDocumentSyncOptions := none)
-
-def mkLeanServerCapabilities : ServerCapabilities :=
-{textDocumentSync? := some {openClose := true, change? := TextDocumentSyncKind.incremental}}
-
 instance clientCapabilitiesHasFromJson : HasFromJson ClientCapabilities :=
 ⟨fun j => ClientCapabilities.mk⟩
 
+-- TODO largely unimplemented
+structure ServerCapabilities :=
+(textDocumentSync? : Option TextDocumentSyncOptions := none)
+
 instance serverCapabilitiesHasToJson : HasToJson ServerCapabilities :=
 ⟨fun o => mkObj $
   opt "textDocumentSync" o.textDocumentSync? ++ []⟩
 
+def mkLeanServerCapabilities : ServerCapabilities :=
+{ textDocumentSync? := some
+  { openClose := true
+  , change? := TextDocumentSyncKind.incremental }}
+
 end Lean.Lsp
diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean
index 7db8c57097..742f556cd2 100644
--- a/src/Lean/Data/Lsp/Communication.lean
+++ b/src/Lean/Data/Lsp/Communication.lean
@@ -29,8 +29,9 @@ private partial def readHeaderFields : FS.Handle → IO (List (String × String)
     | some hf => do
       tail ← readHeaderFields h;
       pure (hf :: tail)
-    | none => throw (userError "invalid header field")
-    
+    | none => throw (userError $ "invalid header field" ++ l)
+
+-- Returns the Content-Length.
 private def readLspHeader (h : FS.Handle) : IO Nat := do
 fields ← readHeaderFields h;
 match fields.lookup "Content-Length" with
@@ -57,9 +58,9 @@ def writeLspMessage (h : FS.Handle) (m : Message) : IO Unit := do
 let j := (toJson m).compress;
 let header := "Content-Length: " ++ toString j.utf8ByteSize ++ "\r\n\r\n";
 h.putStr (header ++ j);
-IO.println "starting to flush now";
-h.flush;
-IO.println "flushed"
+--IO.println "starting to flush now";
+h.flush
+--IO.println "flushed";
 
 def writeLspResponse {α : Type*} [Lean.HasToJson α] (h : FS.Handle) (id : RequestID) (r : α) : IO Unit :=
 writeLspMessage h (Message.response id (toJson r))
diff --git a/src/Lean/Data/Lsp/GeneralMessage.lean b/src/Lean/Data/Lsp/GeneralMessage.lean
index e38dcbfe73..046920147a 100644
--- a/src/Lean/Data/Lsp/GeneralMessage.lean
+++ b/src/Lean/Data/Lsp/GeneralMessage.lean
@@ -6,46 +6,38 @@ namespace Lean.Lsp
 open Lean
 open Lean.Json
 
-structure ClientInfo := (name : String) (version? : Option String := none)
-
-inductive Trace
-| messages
-| verbose
-
-structure InitializeParams :=
--- id of parent process, none if no parent process
-(processId? : Option Int := none)
-(clientInfo? : Option ClientInfo := none)
--- we don't support the deprecated rootPath
--- none: no folder is open
-(rootUri? : Option String := none) 
-(initializationOptions? : Option Json := none)
-(capabilities : ClientCapabilities)
-(trace? : Option Trace := none) -- none: no trace
---(workspaceFolders? : Option Unit) TODO
-
-inductive Initialized
-| mk
-
-structure ServerInfo :=
+structure ClientInfo :=
 (name : String)
 (version? : Option String := none)
 
-structure InitializeResult :=
-(capabilities : ServerCapabilities)
-(serverInfo? : Option String := none)
-
 instance clientInfoHasFromJson : HasFromJson ClientInfo :=
 ⟨fun j => do
   name ← j.getObjValAs? String "name";
   let version? := j.getObjValAs? String "version";
   pure ⟨name, version?⟩⟩
 
+inductive Trace
+| messages
+| verbose
+
 instance traceHasFromJson : HasFromJson Trace :=
 ⟨fun j => match j.getStr? with
-  | some "messages" => Trace.messages
-  | some "verbose" => Trace.verbose
-  | _ => none⟩
+| some "messages" => Trace.messages
+| some "verbose" => Trace.verbose
+| _ => none⟩
+
+structure InitializeParams :=
+-- id of parent process, none if no parent process
+(processId? : Option Int := none)
+(clientInfo? : Option ClientInfo := none)
+/- We don't support the deprecated rootPath
+(rootPath? : Option String)-/
+-- none: no folder is open
+(rootUri? : Option String := none)
+(initializationOptions? : Option Json := none)
+(capabilities : ClientCapabilities)
+(trace? : Option Trace := none) -- none: no trace
+--(workspaceFolders? : Option Unit) TODO
 
 instance initializeParamsHasFromJson : HasFromJson InitializeParams :=
 ⟨fun j => do
@@ -64,15 +56,26 @@ instance initializeParamsHasFromJson : HasFromJson InitializeParams :=
   let trace? := j.getObjValAs? Trace "trace";
   pure ⟨processId?, clientInfo?, rootUri?, initializationOptions?, capabilities, trace?⟩⟩
 
+inductive Initialized
+| mk
+
 instance initializedHasFromJson : HasFromJson Initialized :=
 ⟨fun j => Initialized.mk⟩
 
+structure ServerInfo :=
+(name : String)
+(version? : Option String := none)
+
 instance serverInfoHasToJson : HasToJson ServerInfo :=
 ⟨fun o => mkObj $
-  ⟨"name", o.name⟩ :: opt "version" o.version? ++ []⟩
+  ⟨"name", o.name⟩ :: opt "version" o.version?⟩
+
+structure InitializeResult :=
+(capabilities : ServerCapabilities)
+(serverInfo? : Option ServerInfo := none)
 
 instance initializeResultHasToJson : HasToJson InitializeResult :=
 ⟨fun o => mkObj $
-  ⟨"capabilities", toJson o.capabilities⟩ :: opt "serverInfo" o.serverInfo? ++ []⟩
+  ⟨"capabilities", toJson o.capabilities⟩ :: opt "serverInfo" o.serverInfo?⟩
 
 end Lean.Lsp
diff --git a/src/Lean/Data/Lsp/Structure.lean b/src/Lean/Data/Lsp/Structure.lean
index ab6c0783c7..b921e1ad59 100644
--- a/src/Lean/Data/Lsp/Structure.lean
+++ b/src/Lean/Data/Lsp/Structure.lean
@@ -18,7 +18,7 @@ structure Range := (start : Position) («end» : Position)
 
 structure Location := (uri : DocumentUri) (range : Range)
 
-structure LocationLink := 
+structure LocationLink :=
 -- span in origin that is highlighted (e.g. underlined).
 -- default for none: word range at mouse position
 (originSelectionRange? : Option Range)
@@ -29,29 +29,69 @@ structure LocationLink :=
 -- must be a subrange of targetRange
 (targetSelectionRange : Range)
 
-inductive DiagnosticSeverity 
+inductive DiagnosticSeverity
 | error | warning | information | hint
 
-inductive DiagnosticCode 
-| int (i : Int) 
-| string (s : String) 
+instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity :=
+⟨fun j => match j.getNat? with
+  | some 1 => DiagnosticSeverity.error
+  | some 2 => DiagnosticSeverity.warning
+  | some 3 => DiagnosticSeverity.information
+  | some 4 => DiagnosticSeverity.hint
+  | _      => none⟩
 
-inductive DiagnosticTag 
--- faded out in client
+instance diagnosticSeverityHasToJson : HasToJson DiagnosticSeverity :=
+⟨fun o => match o with
+  | DiagnosticSeverity.error       => (1 : Nat)
+  | DiagnosticSeverity.warning     => (2 : Nat)
+  | DiagnosticSeverity.information => (3 : Nat)
+  | DiagnosticSeverity.hint        => (4 : Nat)⟩
+
+inductive DiagnosticCode
+| int (i : Int)
+| string (s : String)
+
+instance diagnosticCodeHasToJson : HasToJson DiagnosticCode :=
+⟨fun o => match o with
+  | DiagnosticCode.int i    => i
+  | DiagnosticCode.string s => s⟩
+
+inductive DiagnosticTag
+/- Unused or unnecessary code.
+
+Clients are allowed to render diagnostics with this tag faded out instead of having
+an error squiggle. -/
 | unnecessary
--- struck through in client
+/- Deprecated or obsolete code.
+
+Clients are allowed to rendered diagnostics with this tag strike through. -/
 | deprecated
 
-structure DiagnosticRelatedInformation := (location : Location) (message : String)
+/- Represents a related message and source code location for a diagnostic. This should be
+used to point to code locations that cause or are related to a diagnostics, e.g when duplicating
+a symbol in a scope. -/
+structure DiagnosticRelatedInformation :=
+(location : Location)
+(message : String)
 
 structure Diagnostic :=
+/- The range at which the message applies. -/
 (range : Range)
--- none: client is free to choose severity
+/- The diagnostic's severity. Can be omitted. If omitted it is up to the
+client to interpret diagnostics as error, warning, info or hint. -/
 (severity? : Option DiagnosticSeverity := none)
+/- The diagnostic's code, which might appear in the user interface. -/
 (code? : Option DiagnosticCode := none)
+/- A human-readable string describing the source of this
+diagnostic, e.g. 'typescript' or 'super lint'. -/
 (source? : Option String := none)
+/- The diagnostic's message. -/
 (message : String)
+/- Additional metadata about the diagnostic.
+@since 3.15.0 -/
 (tags? : Option (Array DiagnosticTag) := none)
+/- An array of related diagnostic information, e.g. when symbol-names within
+a scope collide all definitions can be marked via this property. -/
 (relatedInformation? : Option (Array DiagnosticRelatedInformation) := none)
 
 structure Command :=
@@ -63,11 +103,11 @@ structure Command :=
 
 structure TextEdit :=
 -- text insertion: start = end
-(range : Range) 
+(range : Range)
 -- text deletion: empty string
 (newText : String)
 
--- no intermediate states: 
+-- no intermediate states:
 -- - ranges may not overlap
 -- - multiple inserts can have the same starting position
 -- - the order of the array induces the insert order
@@ -77,7 +117,7 @@ def TextEditBatch := Array TextEdit
 
 structure TextDocumentIdentifier := (uri : DocumentUri)
 
-structure VersionedTextDocumentIdentifier := 
+structure VersionedTextDocumentIdentifier :=
 (uri : DocumentUri)
 -- increases after each change, undo and redo
 -- none used when a document is not open and the
@@ -88,7 +128,7 @@ structure TextDocumentEdit :=
 (textDocument : VersionedTextDocumentIdentifier)
 (edits : TextEditBatch)
 
--- TODO(Marc): missing: 
+-- TODO(Marc): missing:
 -- File Resource Changes, WorkspaceEdit
 -- both of these are pretty global, we can look at their
 -- uses when single file behaviour works.
@@ -103,11 +143,11 @@ structure TextDocumentItem :=
 (text : String)
 
 -- parameter literal for requests
-structure TextDocumentPositionParams := 
+structure TextDocumentPositionParams :=
 (textDocument : TextDocumentIdentifier)
 (position : Position)
 
-structure DocumentFilter := 
+structure DocumentFilter :=
 (language? : Option String := none) -- language id
 -- uri scheme like 'file' or 'untitled'
 (scheme? : Option String := none)
@@ -126,7 +166,7 @@ def DocumentSelector := Array DocumentFilter
 structure TextDocumentRegistrationOptions := (documentSelector? : Option DocumentSelector := none)
 
 -- TODO(Marc): missing:
--- StaticRegistrationOptions, 
+-- StaticRegistrationOptions,
 -- MarkupContent, WorkDoneProgressBegin, WorkDoneProgressReport,
 -- WorkDoneProgressEnd, WorkDoneProgressParams,
 -- WorkDoneProgressOptions, PartialResultParams
@@ -154,15 +194,6 @@ instance locationHasFromJson : HasFromJson Location :=
   range ← j.getObjValAs? Range "range";
   pure ⟨uri, range⟩⟩
 
-
-instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity :=
-⟨fun j => match j.getNat? with
-  | some 1 => DiagnosticSeverity.error
-  | some 2 => DiagnosticSeverity.warning
-  | some 3 => DiagnosticSeverity.information
-  | some 4 => DiagnosticSeverity.hint
-  | _      => none⟩
-
 instance diagnosticCodeHasFromJson : HasFromJson DiagnosticCode :=
 ⟨fun j => match j with
   | num (i : Int) => DiagnosticCode.int i
@@ -224,7 +255,6 @@ instance documentSelectorHasFromJson : HasFromJson DocumentSelector :=
 instance textDocumentRegistrationOptionsHasFromJson : HasFromJson TextDocumentRegistrationOptions :=
 ⟨fun j => some ⟨j.getObjValAs? DocumentSelector "documentSelector"⟩⟩
 
-
 instance documentUriHasToJson : HasToJson DocumentUri :=
 ⟨fun (o : String) => o⟩
 
@@ -234,24 +264,12 @@ instance positionHasToJson : HasToJson Position :=
 
 instance rangeHasToJson : HasToJson Range :=
 ⟨fun o => mkObj $
-  ⟨"start", toJson o.start⟩ :: ⟨"«end»", toJson o.«end»⟩ :: []⟩
+  ⟨"start", toJson o.start⟩ :: ⟨"end", toJson o.«end»⟩ :: []⟩
 
 instance locationHasToJson : HasToJson Location :=
 ⟨fun o => mkObj $
   ⟨"uri", toJson o.uri⟩ :: ⟨"range", toJson o.range⟩ :: []⟩
 
-instance diagnosticSeverityHasToJson : HasToJson DiagnosticSeverity :=
-⟨fun o => match o with
-  | DiagnosticSeverity.error       => (1 : Nat)
-  | DiagnosticSeverity.warning     => (2 : Nat)
-  | DiagnosticSeverity.information => (3 : Nat)
-  | DiagnosticSeverity.hint        => (4 : Nat)⟩
-
-instance diagnosticCodeHasToJson : HasToJson DiagnosticCode :=
-⟨fun o => match o with
-  | DiagnosticCode.int i    => i
-  | DiagnosticCode.string s => s⟩
-
 instance diagnosticTagHasToJson : HasToJson DiagnosticTag :=
 ⟨fun o => match o with
   | DiagnosticTag.unnecessary => (1 : Nat)
@@ -263,7 +281,7 @@ instance diagnosticRelatedInformationHasToJson : HasToJson DiagnosticRelatedInfo
 
 instance diagnosticHasToJson : HasToJson Diagnostic :=
 ⟨fun o => mkObj $
-  ⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++ 
+  ⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++
     opt "source" o.source? ++ ⟨"message", o.message⟩ :: opt "tags" o.tags? ++ []⟩
 
 end Lean.Lsp
diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean
index a52325f29c..56cf1525f6 100644
--- a/src/Lean/Data/Lsp/TextSync.lean
+++ b/src/Lean/Data/Lsp/TextSync.lean
@@ -7,19 +7,30 @@ open Lean
 open Lean.Json
 
 inductive TextDocumentSyncKind
--- synced by sending full content and on every update
-| full 
--- synced by sending full content on open and otherwise
--- incremental updates
-| incremental 
+/- Documents should not be synced at all. -/
+--| none
+/- Documents are synced by always sending the full content of the document. -/
+| full
+/- Documents are synced by sending the full content on open. After that only incremental updates to the document are send. -/
+| incremental
 
 structure TextDocumentSyncOptions :=
-(openClose : Bool) -- open/close notifications are sent to server
-(change? : Option TextDocumentSyncKind := none) -- none: not synced
+/- Open and close notifications are sent to the server.
+If omitted open close notification should not be sent. -/
+(openClose : Bool)
+/- Change notifications are sent to the server.
+If omitted it defaults to TextDocumentSyncKind.None.
+none: not synced -/
+(change? : Option TextDocumentSyncKind := none)
 
 structure DidOpenTextDocumentParams :=
 (textDocument : TextDocumentItem)
 
+instance didOpenTextDocumentParamsHasFromJson : HasFromJson DidOpenTextDocumentParams :=
+⟨fun j => do
+  textDocument ← j.getObjValAs? TextDocumentItem "textDocument";
+  pure ⟨textDocument⟩⟩
+
 structure TextDocumentChangeRegistrationOptions :=
 (documentSelector? : Option DocumentSelector := none)
 (syncKind : TextDocumentSyncKind)
@@ -61,11 +72,6 @@ instance textDocumentSyncOptionsHasToJson : HasToJson TextDocumentSyncOptions :=
 ⟨fun o => mkObj $
   ⟨"openClose", o.openClose⟩ :: opt "change" o.change? ++ []⟩
 
-instance didOpenTextDocumentParamsHasFromJson : HasFromJson DidOpenTextDocumentParams :=
-⟨fun j => do
-  textDocument ← j.getObjValAs? TextDocumentItem "textDocument";
-  pure ⟨textDocument⟩⟩
-
 instance textDocumentChangeRegistrationOptionsHasFromJson : HasFromJson TextDocumentChangeRegistrationOptions :=
 ⟨fun j => do
   let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector";
@@ -73,7 +79,7 @@ instance textDocumentChangeRegistrationOptionsHasFromJson : HasFromJson TextDocu
   pure ⟨documentSelector?, syncKind⟩⟩
 
 instance textDocumentContentChangeEventHasFromJson : HasFromJson TextDocumentContentChangeEvent :=
-⟨fun j => 
+⟨fun j =>
   (do
     range ← j.getObjValAs? Range "range";
     text ← j.getObjValAs? String "text";
diff --git a/src/Lean/Server/Server.lean b/src/Lean/Server/Server.lean
index 8d47cfb84c..4fc3e199f7 100644
--- a/src/Lean/Server/Server.lean
+++ b/src/Lean/Server/Server.lean
@@ -15,7 +15,10 @@ open Lean.Elab
 -- LSP indexes text with rows and colums
 abbrev DocumentText := Array String
 
-structure Document := (version : Int) (text : DocumentText) (env : Environment)
+structure Document :=
+(version : Int)
+(text : DocumentText)
+(headerEnv : Environment)
 
 abbrev DocumentMap := RBMap DocumentUri Document (fun a b => Decidable.decide (a < b))
 
@@ -28,6 +31,18 @@ match @fromJson? paramType _ params with
 | some parsed => pure parsed
 | none        => throw (userError "got param with wrong structure")
 
+def runFrontend (text : String) : IO (Environment × Environment × MessageLog) := do
+let inputCtx := Parser.mkInputContext text "<input>";
+envNul ← mkEmptyEnvironment;
+match Parser.parseHeader envNul inputCtx with
+| (header, parserState, messages) => do
+  (env, messages) ← processHeader header messages inputCtx;
+  parserStateRef ← IO.mkRef parserState;
+  cmdStateRef    ← IO.mkRef $ Command.mkState env messages {};
+  IO.processCommands inputCtx parserStateRef cmdStateRef;
+  cmdState ← cmdStateRef.get;
+  pure (env, cmdState.env, cmdState.messages)
+
 def updateFrontend (env : Environment) (input : String) : IO (Environment × MessageLog) := do
 let inputCtx := Parser.mkInputContext input "<input>";
 parserStateRef ← IO.mkRef ({} : Parser.ModuleParserState);
@@ -48,7 +63,10 @@ let severity := match m.severity with
 | MessageSeverity.error       => DiagnosticSeverity.error;
 let source := "Lean 4 server";
 let message := toString (format m.data);
-{range := range, severity? := severity, source? := source, message := message}
+{ range := range
+, severity? := severity
+, source? := source
+, message := message}
 
 namespace ServerState
 
@@ -61,49 +79,59 @@ match openDocuments.find? key with
 def updateOpenDocuments (s : ServerState) (key : DocumentUri) (val : Document) : IO Unit :=
 s.openDocumentsRef.modify (fun documents => (documents.erase key).insert key val)
 
-def sendDiagnostics (s : ServerState) (uri : DocumentUri) (d : Document) (log : MessageLog) : IO Unit := 
+def sendDiagnostics (s : ServerState) (uri : DocumentUri) (d : Document) (log : MessageLog) : IO Unit :=
 let diagnostics := log.msgs.map (msgToDiagnostic d.text);
-writeLspNotification s.o "textDocument/publishDiagnostics" {PublishDiagnosticsParams . uri := uri, version? := d.version, diagnostics := diagnostics.toArray}
+writeLspNotification s.o "textDocument/publishDiagnostics"
+  { uri := uri
+  , version? := d.version
+  , diagnostics := diagnostics.toArray : PublishDiagnosticsParams }
 
 def handleDidOpen (s : ServerState) (p : DidOpenTextDocumentParams) : IO Unit := do
-let d := p.textDocument;
-let text := d.text.splitOnEOLs;
-(env, msgLog) ← runFrontend {const2ModIdx := {}, constants := {}, extensions := #[]} ("\n".intercalate text);
-let newDoc : Document := ⟨d.version, text.toArray, env⟩;
-s.openDocumentsRef.modify (fun openDocuments => openDocuments.insert d.uri newDoc);
-s.sendDiagnostics d.uri newDoc msgLog
+let doc := p.textDocument;
+let text := doc.text.splitOnEOLs;
+(headerEnv, env, msgLog) ← runFrontend ("\n".intercalate text);
+let newDoc : Document := ⟨doc.version, text.toArray, headerEnv⟩;
+s.openDocumentsRef.modify (fun openDocuments => openDocuments.insert doc.uri newDoc);
+s.sendDiagnostics doc.uri newDoc msgLog
 
 def handleDidChange (s : ServerState) (p : DidChangeTextDocumentParams) : IO Unit := do
-let d := p.textDocument;
-let c := p.contentChanges;
-oldDoc ← s.findOpenDocument d.uri;
-some newVersion ← pure d.version? | throw (userError "expected version number");
+let doc := p.textDocument;
+let changes := p.contentChanges;
+oldDoc ← s.findOpenDocument doc.uri;
+some newVersion ← pure doc.version? | throw (userError "expected version number");
 if newVersion <= oldDoc.version then do
   throw (userError "got outdated version number")
-else c.forM $ fun change =>
+else changes.forM $ fun change =>
   match change with
   | TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) => do
     let newDocText := replaceRange oldDoc.text range newText;
-    -- (newEnv, newMsgLog) ← updateFrontend oldDoc.env ("\n".intercalate newDocText.toList);
-    (newEnv, msgLog) ← runFrontend {const2ModIdx := {}, constants := {}, extensions := #[]} ("\n".intercalate newDocText.toList);
-    let newDoc : Document := ⟨newVersion, newDocText, newEnv⟩;
-    s.updateOpenDocuments d.uri newDoc;
-    s.sendDiagnostics d.uri newDoc msgLog
-  | TextDocumentContentChangeEvent.fullChange (text : String) => throw (userError "got content change that replaces the full document (not supported)") 
+    (newEnv, msgLog) ← updateFrontend oldDoc.headerEnv ("\n".intercalate newDocText.toList);
+    let newDoc : Document := ⟨newVersion, newDocText, oldDoc.headerEnv⟩;
+    s.updateOpenDocuments doc.uri newDoc;
+    s.sendDiagnostics doc.uri newDoc msgLog
+  | TextDocumentContentChangeEvent.fullChange (text : String) =>
+    throw (userError "got content change that replaces the full document (not supported)")
 
 def handleNotification (s : ServerState) (method : String) (params : Json) : IO Unit := do
-let h := (fun paramType [HasFromJson paramType] (handler : ServerState → paramType → IO Unit) => 
+let h := (fun paramType [HasFromJson paramType] (handler : ServerState → paramType → IO Unit) =>
   parseParams paramType params >>= handler s);
 match method with
 | "textDocument/didOpen"   => h DidOpenTextDocumentParams handleDidOpen
 | "textDocument/didChange" => h DidChangeTextDocumentParams handleDidChange
 | _                        => throw (userError "got unsupported notification method")
 
+def handleRequest (s : ServerState) (id : RequestID) (method : String) (params : Json)
+  : IO Unit := do
+  match method with
+  | _ => throw (userError "Not supporting requests for now!")
+
 partial def mainLoop : ServerState → IO Unit
 | s => do
   m ← readLspMessage s.i;
   match m with
-  | Message.request id method (some params) => pure ()
+  | Message.request id method (some params) => do
+    s.handleRequest id method (toJson params);
+    mainLoop s
   | Message.requestNotification method (some params) => do
     s.handleNotification method (toJson params);
     mainLoop s
@@ -114,7 +142,9 @@ end ServerState
 def initialize (i o : FS.Handle) : IO Unit := do
 -- ignore InitializeParams for MWE
 r ← readLspRequestAs i "initialize" InitializeParams;
-writeLspResponse o r.id mkLeanServerCapabilities;
+writeLspResponse o r.id ({ capabilities := mkLeanServerCapabilities
+                          , serverInfo? := some { name := "Lean 4 server"
+                                                , version? := "0.0.1" }} : InitializeResult);
 _ ← readLspRequestNotificationAs i "initialized" Initialized;
 openDocumentsRef ← IO.mkRef (RBMap.empty : DocumentMap);
 ServerState.mainLoop ⟨i, o, openDocumentsRef⟩