diff --git a/src/Lean/Data/Json/Handle.lean b/src/Lean/Data/Json/Handle.lean
index 4f7d4c388e..80444fca75 100644
--- a/src/Lean/Data/Json/Handle.lean
+++ b/src/Lean/Data/Json/Handle.lean
@@ -10,7 +10,8 @@ open IO
 
 def readJson (h : FS.Handle) (nBytes : Nat) : IO Json := do
 bytes ← h.read nBytes;
-some s ← pure bytes.utf8ToString | throw (userError ("got non-utf8 string '" ++ toString bytes ++ "'"));
+some s ← pure bytes.utf8ToString
+  | throw (userError ("got non-utf8 string '" ++ toString bytes ++ "'"));
 j ← ofExcept (Json.parse s);
 pure j
 
diff --git a/src/Lean/Data/Json/Printer.lean b/src/Lean/Data/Json/Printer.lean
index d9822a5f15..8c6ed569b6 100644
--- a/src/Lean/Data/Json/Printer.lean
+++ b/src/Lean/Data/Json/Printer.lean
@@ -74,7 +74,7 @@ partial def compress : Json → String
 | num s      => s.toString
 | str s      => renderString s
 | arr elems  => "[" ++ ",".intercalate (elems.map compress).toList ++ "]"
-| obj kvs    => 
+| obj kvs    =>
   let ckvs := kvs.fold (fun acc k j => (renderString k ++ ":" ++ compress j) :: acc) [];
   "{" ++ ",".intercalate ckvs ++ "}"
 
diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index 9680076be9..e8b74c18a9 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -3,10 +3,10 @@ import Init.System.IO
 import Std.Data.RBTree
 import Lean.Data.Json
 
-namespace Lean.JsonRpc
+namespace Lean
+namespace JsonRpc
 
-open Lean
-open Lean.Json
+open Json
 open Std (RBNode)
 
 inductive RequestID
@@ -156,7 +156,8 @@ instance messageFromJson : HasFromJson Message :=
   "2.0" ← j.getObjVal? "jsonrpc" | none;
   aux1 j <|> aux2 j <|> aux3 j <|> aux4 j⟩
 
-end Lean.JsonRpc
+end JsonRpc
+end Lean
 
 namespace IO.FS.Handle
 
diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean
index 31697ed679..e3490a515f 100644
--- a/src/Lean/Data/Lsp/Capabilities.lean
+++ b/src/Lean/Data/Lsp/Capabilities.lean
@@ -1,11 +1,11 @@
 import Lean.Data.JsonRpc
 import Lean.Data.Lsp.TextSync
 
-namespace Lean.Lsp
+namespace Lean
+namespace Lsp
 
-open Lean
-open Lean.Json
-open Lean.JsonRpc
+open Json
+open JsonRpc
 
 -- TODO: right now we ignore the client's capabilities
 inductive ClientCapabilities | mk
@@ -29,4 +29,5 @@ def mkLeanServerCapabilities : ServerCapabilities :=
   , change? := TextDocumentSyncKind.incremental }
 , hoverProvider := true }
 
-end Lean.Lsp
+end Lsp
+end Lean
diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean
index 208b0d8ec7..cdc2350eb4 100644
--- a/src/Lean/Data/Lsp/Communication.lean
+++ b/src/Lean/Data/Lsp/Communication.lean
@@ -1,11 +1,11 @@
 import Init.System.IO
 import Lean.Data.JsonRpc
 
-namespace Lean.Lsp
+namespace Lean
+namespace Lsp
 
 open IO
-open Lean
-open Lean.JsonRpc
+open JsonRpc
 
 private def parseHeaderField (s : String) : Option (String × String) :=
 if s = "" ∨ s.takeRight 2 ≠ "\r\n" then
@@ -44,11 +44,11 @@ def readLspMessage (h : FS.Handle) : IO Message := do
 nBytes ← readLspHeader h;
 h.readMessage nBytes
 
-def readLspRequestAs (h : FS.Handle) (expectedMethod : String) (α : Type*) [Lean.HasFromJson α] : IO (Request α) := do
+def readLspRequestAs (h : FS.Handle) (expectedMethod : String) (α : Type*) [HasFromJson α] : IO (Request α) := do
 nBytes ← readLspHeader h;
 h.readRequestAs nBytes expectedMethod α
 
-def readLspRequestNotificationAs (h : FS.Handle) (expectedMethod : String) (α : Type*) [Lean.HasFromJson α] : IO α := do
+def readLspRequestNotificationAs (h : FS.Handle) (expectedMethod : String) (α : Type*) [HasFromJson α] : IO α := do
 nBytes ← readLspHeader h;
 h.readRequestNotificationAs nBytes expectedMethod α
 
@@ -60,13 +60,14 @@ let header := "Content-Length: " ++ toString j.utf8ByteSize ++ "\r\n\r\n";
 h.putStr (header ++ j);
 h.flush
 
-def writeLspResponse {α : Type*} [Lean.HasToJson α] (h : FS.Handle) (id : RequestID) (r : α) : IO Unit :=
+def writeLspResponse {α : Type*} [HasToJson α] (h : FS.Handle) (id : RequestID) (r : α) : IO Unit :=
 writeLspMessage h (Message.response id (toJson r))
 
-def writeLspNotification {α : Type*} [Lean.HasToJson α] (h : FS.Handle) (method : String) (r : α) : IO Unit :=
+def writeLspNotification {α : Type*} [HasToJson α] (h : FS.Handle) (method : String) (r : α) : IO Unit :=
 match toJson r with
 | Json.obj o => writeLspMessage h (Message.requestNotification method o)
 | Json.arr a => writeLspMessage h (Message.requestNotification method a)
 | _          => throw (userError "internal server error in Lean.Lsp.writeLspNotification: tried to write lsp notification that is neither a json object nor a json array")
 
-end Lean.Lsp
+end Lsp
+end Lean
diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index 627a81665d..edb2072fd5 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -3,10 +3,10 @@ import Lean.Data.Json
 import Lean.Data.Lsp.Structure
 import Lean.Data.Lsp.Utf16
 
-namespace Lean.Lsp
+namespace Lean
+namespace Lsp
 
-open Lean
-open Lean.Json
+open Json
 
 inductive DiagnosticSeverity
 | error | warning | information | hint
@@ -135,7 +135,7 @@ instance publishDiagnosticsParamsHasToJson : HasToJson PublishDiagnosticsParams
   ⟨"uri", toJson o.uri⟩ :: opt "version" o.version? ++ ⟨"diagnostics", toJson o.diagnostics⟩ :: []⟩
 
 /-- Transform a Lean Message into an LSP Diagnostic. -/
-def msgToDiagnostic (text : DocumentText) (m : Lean.Message) : Diagnostic :=
+def msgToDiagnostic (text : DocumentText) (m : Message) : Diagnostic :=
 -- Lean Message line numbers are 1-based while LSP Positions are 0-based.
 let lowLn := m.pos.line - 1;
 let low : Lsp.Position := ⟨lowLn, (text.get! lowLn).codepointPosToUtf16Pos m.pos.column⟩;
@@ -156,4 +156,5 @@ let message := toString (format m.data);
 , source? := source
 , message := message}
 
-end Lean.Lsp
+end Lsp
+end Lean
diff --git a/src/Lean/Data/Lsp/GeneralMessage.lean b/src/Lean/Data/Lsp/GeneralMessage.lean
index 046920147a..e62ef5d2b0 100644
--- a/src/Lean/Data/Lsp/GeneralMessage.lean
+++ b/src/Lean/Data/Lsp/GeneralMessage.lean
@@ -1,10 +1,10 @@
 import Lean.Data.Lsp.Capabilities
 import Lean.Data.Json
 
-namespace Lean.Lsp
+namespace Lean
+namespace Lsp
 
-open Lean
-open Lean.Json
+open Json
 
 structure ClientInfo :=
 (name : String)
@@ -78,4 +78,5 @@ instance initializeResultHasToJson : HasToJson InitializeResult :=
 ⟨fun o => mkObj $
   ⟨"capabilities", toJson o.capabilities⟩ :: opt "serverInfo" o.serverInfo?⟩
 
-end Lean.Lsp
+end Lsp
+end Lean
diff --git a/src/Lean/Data/Lsp/Hover.lean b/src/Lean/Data/Lsp/Hover.lean
index 364c61dbe0..62f9f73ad5 100644
--- a/src/Lean/Data/Lsp/Hover.lean
+++ b/src/Lean/Data/Lsp/Hover.lean
@@ -1,10 +1,10 @@
 import Lean.Data.Json
 import Lean.Data.Lsp.Structure
 
-namespace Lean.Lsp
+namespace Lean
+namespace Lsp
 
-open Lean
-open Lean.Json
+open Json
 
 /- The result of a hover request. -/
 structure Hover :=
@@ -12,7 +12,7 @@ structure Hover :=
 --(contents: MarkedString | MarkedString[] | MarkupContent)
 /- An optional range is a range inside a text document
 that is used to visualize a hover, e.g. by changing the background color. -/
-(range? : Range)
+(range? : Option Range := none)
 
 structure HoverParams extends TextDocumentPositionParams
 
@@ -21,5 +21,5 @@ instance hoverParamsHasFromJson : HasFromJson HoverParams :=
   tdpp : TextDocumentPositionParams ← fromJson? j;
   pure ⟨tdpp⟩⟩
 
-end Lean.Lsp
-
+end Lsp
+end Lean
diff --git a/src/Lean/Data/Lsp/Structure.lean b/src/Lean/Data/Lsp/Structure.lean
index 18b35cf00b..2260a83562 100644
--- a/src/Lean/Data/Lsp/Structure.lean
+++ b/src/Lean/Data/Lsp/Structure.lean
@@ -1,9 +1,9 @@
 import Lean.Data.Json
 
-namespace Lean.Lsp
+namespace Lean
+namespace Lsp
 
-open Lean
-open Lean.Json
+open Json
 
 -- all Ints/Nats in this file are Floats in LSP
 
@@ -203,4 +203,5 @@ instance textDocumentRegistrationOptionsHasFromJson : HasFromJson TextDocumentRe
 -- Markup and Progress can be implemented
 -- later when the basic functionality stands.
 
-end Lean.Lsp
+end Lsp
+end Lean
diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean
index 20cd8c668c..2320fb4f1f 100644
--- a/src/Lean/Data/Lsp/TextSync.lean
+++ b/src/Lean/Data/Lsp/TextSync.lean
@@ -1,10 +1,10 @@
 import Lean.Data.Json
 import Lean.Data.Lsp.Structure
 
-namespace Lean.Lsp
+namespace Lean
+namespace Lsp
 
-open Lean
-open Lean.Json
+open Json
 
 inductive TextDocumentSyncKind
 /- Documents should not be synced at all. -/
@@ -112,4 +112,5 @@ instance didCloseTextDocumentParamsHasFromJson : HasFromJson DidCloseTextDocumen
   textDocument ← j.getObjValAs? TextDocumentIdentifier "textDocument";
   pure ⟨textDocument⟩⟩
 
-end Lean.Lsp
+end Lsp
+end Lean
diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
index e4de030488..817c48f1d8 100644
--- a/src/Lean/Data/Lsp/Utf16.lean
+++ b/src/Lean/Data/Lsp/Utf16.lean
@@ -72,7 +72,8 @@ n.repeat (fun acc => acc.eraseIdx i) as
 
 end Array
 
-namespace Lean.Lsp
+namespace Lean
+namespace Lsp
 
 def replaceRange (text : Array String) (r : Range) (newText : String) : Array String :=
 let sl := r.start.line;
@@ -91,4 +92,5 @@ let replaced := (focused.utf16Replace newText si endIdx).splitOnEOLs.toArray;
 (text.eraseAll sl (el - sl + 1)).insertAll sl replaced
 
 
-end Lean.Lsp
+end Lsp
+end Lean
diff --git a/src/Lean/Server/Server.lean b/src/Lean/Server/Server.lean
index 78fbeb745a..37e74cc449 100644
--- a/src/Lean/Server/Server.lean
+++ b/src/Lean/Server/Server.lean
@@ -6,11 +6,14 @@ import Lean.Server.Snapshots
 import Lean.Data.Lsp
 import Lean.Data.Json.FromToJson
 
-namespace Lean.Server
+namespace Lean
+namespace Server
+
+open Lsp
+
 namespace Editable
 
-open Lean.Lsp
-open Lean.Elab
+open Elab
 
 /-- A document editable in the sense that we track the environment
 and parser state after each command so that edits can be applied
@@ -26,7 +29,7 @@ structure EditableDocument :=
 
 /-- Compiles the contents of a Lean file. -/
 def compileDocument (version : Nat) (text : DocumentText)
-  : IO (Lean.MessageLog × EditableDocument) := do
+  : IO (MessageLog × EditableDocument) := do
 let contents := "\n".intercalate text.toList;
 headerSnap ← Snapshots.compileHeader contents;
 cmdSnaps ← Snapshots.compileCmdsAfter contents headerSnap;
@@ -34,8 +37,8 @@ let docOut : EditableDocument := ⟨version, text, headerSnap, cmdSnaps⟩;
 let msgLog := (cmdSnaps.getLastD headerSnap).msgLog;
 pure (msgLog, docOut)
 
-def updateDocument (doc : EditableDocument) (changePos : Position) (newVersion : Nat)
-  (newText : DocumentText) : IO (Lean.MessageLog × EditableDocument) := do
+def updateDocument (doc : EditableDocument) (changePos : Lsp.Position) (newVersion : Nat)
+  (newText : DocumentText) : IO (MessageLog × EditableDocument) := do
 let newContents := "\n".intercalate newText.toList;
 let changePos := doc.text.lnColToLinearPos changePos;
 let recompileEverything := compileDocument newVersion newText;
@@ -67,10 +70,7 @@ open Editable
 
 open IO
 open Std (RBMap RBMap.empty)
-open Lean
-open Lean.JsonRpc
-open Lean.Lsp
-open Lean.Elab
+open JsonRpc
 
 abbrev DocumentMap :=
   RBMap DocumentUri EditableDocument (fun a b => Decidable.decide (a < b))
@@ -201,7 +201,8 @@ Message.requestNotification "exit" none ← readLspMessage i
   | throw (userError "Expected an Exit Notification.");
 pure ()
 
-end Lean.Server
+end Server
+end Lean
 
 def main (n : List String) : IO UInt32 := do
 i ← IO.stdin;
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 4e38dad9f4..96850fd8f0 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -9,9 +9,11 @@ each command. Importantly, we allow (re)starting compilation from any
 snapshot/position in the file for interactive editing purposes. -/
 
 namespace Lean
-namespace Elab
+namespace Server
 namespace Snapshots
 
+open Elab
+
 /-- The data associated with a snapshot is different depending on whether
 it was produced from the header or from a command. -/
 inductive SnapshotData
@@ -81,8 +83,8 @@ else do
     , fileMap := inputCtx.fileMap
     };
   EIO.adaptExcept
-    (fun e => unreachable!) -- TODO(WN): ignoring exceptions ok here?
-    (Elab.Command.withLogging
+    (fun e => Empty.rec _ e)
+    (Elab.Command.catchExceptions
       (Elab.Command.elabCommand cmdStx)
       cmdCtx);
   postCmdState ← cmdStateRef.get;
@@ -104,5 +106,5 @@ partial def compileCmdsAfter (contents : String) : Snapshot → IO (List Snapsho
   | none => pure []
 
 end Snapshots
-end Elab
+end Server
 end Lean