diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index bb361dd798..627a81665d 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -1,11 +1,121 @@
+import Lean.Message
 import Lean.Data.Json
 import Lean.Data.Lsp.Structure
+import Lean.Data.Lsp.Utf16
 
 namespace Lean.Lsp
 
 open Lean
 open Lean.Json
 
+inductive DiagnosticSeverity
+| error | warning | information | hint
+
+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 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 diagnosticCodeHasFromJson : HasFromJson DiagnosticCode :=
+⟨fun j => match j with
+  | num (i : Int) => DiagnosticCode.int i
+  | str s         => DiagnosticCode.string s
+  | _             => none⟩
+
+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
+/- Deprecated or obsolete code.
+
+Clients are allowed to rendered diagnostics with this tag strike through. -/
+| deprecated
+
+instance diagnosticTagHasFromJson : HasFromJson DiagnosticTag :=
+⟨fun j => match j.getNat? with
+  | some 1 => DiagnosticTag.unnecessary
+  | some 2 => DiagnosticTag.deprecated
+  | _      => none⟩
+
+instance diagnosticTagHasToJson : HasToJson DiagnosticTag :=
+⟨fun o => match o with
+  | DiagnosticTag.unnecessary => (1 : Nat)
+  | DiagnosticTag.deprecated  => (2 : Nat)⟩
+
+/- 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)
+
+instance diagnosticRelatedInformationHasFromJson : HasFromJson DiagnosticRelatedInformation :=
+⟨fun j => do
+  location ← j.getObjValAs? Location "location";
+  message ← j.getObjValAs? String "message";
+  pure ⟨location, message⟩⟩
+
+instance diagnosticRelatedInformationHasToJson : HasToJson DiagnosticRelatedInformation :=
+⟨fun o => mkObj $
+  ⟨"location", toJson o.location⟩ :: ⟨"message", o.message⟩ :: []⟩
+
+structure Diagnostic :=
+/- The range at which the message applies. -/
+(range : Range)
+/- 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)
+
+instance diagnosticHasFromJson : HasFromJson Diagnostic :=
+⟨fun j => do
+  range ← j.getObjValAs? Range "range";
+  let severity? := j.getObjValAs? DiagnosticSeverity "severity";
+  let code? := j.getObjValAs? DiagnosticCode "code";
+  let source? := j.getObjValAs? String "source";
+  message ← j.getObjValAs? String "message";
+  let tags? := j.getObjValAs? (Array DiagnosticTag) "tags";
+  let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation";
+  pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩
+
+instance diagnosticHasToJson : HasToJson Diagnostic :=
+⟨fun o => mkObj $
+⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++
+opt "source" o.source? ++ ⟨"message", o.message⟩ :: opt "tags" o.tags? ++ []⟩
+
 structure PublishDiagnosticsParams :=
 (uri : DocumentUri)
 -- version number of document for which
@@ -24,6 +134,26 @@ instance publishDiagnosticsParamsHasToJson : HasToJson PublishDiagnosticsParams
 ⟨fun o => mkObj $
   ⟨"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 :=
+-- 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⟩;
+let high : Lsp.Position := match m.endPos with
+| some endPos =>
+let highLn := endPos.line - 1;
+⟨highLn, (text.get! highLn).codepointPosToUtf16Pos endPos.column⟩
+| none        => low;
+let range : Range := ⟨low, high⟩;
+let severity := match m.severity with
+| MessageSeverity.information => DiagnosticSeverity.information
+| MessageSeverity.warning     => DiagnosticSeverity.warning
+| MessageSeverity.error       => DiagnosticSeverity.error;
+let source := "Lean 4 server";
+let message := toString (format m.data);
+{ range := range
+, severity? := severity
+, source? := source
+, message := message}
 
 end Lean.Lsp
diff --git a/src/Lean/Data/Lsp/Structure.lean b/src/Lean/Data/Lsp/Structure.lean
index 0c51482eb7..05ab738626 100644
--- a/src/Lean/Data/Lsp/Structure.lean
+++ b/src/Lean/Data/Lsp/Structure.lean
@@ -5,11 +5,14 @@ namespace Lean.Lsp
 open Lean
 open Lean.Json
 
--- all Ints in this file are Floats in LSP
+-- all Ints/Nats in this file are Floats in LSP
 
 -- as in http://tools.ietf.org/html/rfc3986
 abbrev DocumentUri := String
 
+-- LSP indexes text with rows and colums
+abbrev DocumentText := Array String
+
 -- character is accepted liberally: actual character := min(line length, character)
 structure Position := (line : Nat) (character : Nat)
 
@@ -19,6 +22,15 @@ instance positionHasFromJson : HasFromJson Position :=
   character ← j.getObjValAs? Nat "character";
   pure ⟨line, character⟩⟩
 
+namespace Position
+
+/-- Computes a linear position from an LSP-style 0-indexed (ln, col) position
+and the text. -/
+def lnColToLinearPos (pos : Position) (text : DocumentText) : String.Pos :=
+text.foldrRange 0 pos.line (fun ln acc => acc + ln.length + 1) pos.character
+
+end Position
+
 -- [start, end)
 structure Range := (start : Position) («end» : Position)
 
@@ -35,70 +47,6 @@ structure LocationLink :=
 -- must be a subrange of targetRange
 (targetSelectionRange : Range)
 
-inductive DiagnosticSeverity
-| error | warning | information | hint
-
-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 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
-/- Deprecated or obsolete code.
-
-Clients are allowed to rendered diagnostics with this tag strike through. -/
-| deprecated
-
-/- 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)
-/- 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 :=
 (title : String)
@@ -133,7 +81,7 @@ structure VersionedTextDocumentIdentifier :=
 -- increases after each change, undo and redo
 -- none used when a document is not open and the
 -- disk content is the master
-(version? : Option Int := none)
+(version? : Option Nat := none)
 
 structure TextDocumentEdit :=
 (textDocument : VersionedTextDocumentIdentifier)
@@ -150,7 +98,7 @@ structure TextDocumentItem :=
 -- when handling more than language
 (languageId : String)
 -- increases after each change, undo and redo
-(version : Int)
+(version : Nat)
 (text : String)
 
 -- parameter literal for requests
@@ -205,46 +153,17 @@ instance locationHasFromJson : HasFromJson Location :=
   range ← j.getObjValAs? Range "range";
   pure ⟨uri, range⟩⟩
 
-instance diagnosticCodeHasFromJson : HasFromJson DiagnosticCode :=
-⟨fun j => match j with
-  | num (i : Int) => DiagnosticCode.int i
-  | str s         => DiagnosticCode.string s
-  | _             => none⟩
-
-instance diagnosticTagFromJson : HasFromJson DiagnosticTag :=
-⟨fun j => match j.getNat? with
-  | some 1 => DiagnosticTag.unnecessary
-  | some 2 => DiagnosticTag.deprecated
-  | _      => none⟩
-
-instance diagnosticRelatedInformationHasFromJson : HasFromJson DiagnosticRelatedInformation :=
-⟨fun j => do
-  location ← j.getObjValAs? Location "location";
-  message ← j.getObjValAs? String "message";
-  pure ⟨location, message⟩⟩
-
-instance diagnosticHasFromJson : HasFromJson Diagnostic :=
-⟨fun j => do
-  range ← j.getObjValAs? Range "range";
-  let severity? := j.getObjValAs? DiagnosticSeverity "severity";
-  let code? := j.getObjValAs? DiagnosticCode "code";
-  let source? := j.getObjValAs? String "source";
-  message ← j.getObjValAs? String "message";
-  let tags? := j.getObjValAs? (Array DiagnosticTag) "tags";
-  let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation";
-  pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩
-
 instance versionedTextDocumentIdentifierHasFromJson : HasFromJson VersionedTextDocumentIdentifier :=
 ⟨fun j => do
   uri ← j.getObjValAs? DocumentUri "uri";
-  let version? := j.getObjValAs? Int "version";
+  let version? := j.getObjValAs? Nat "version";
   pure ⟨uri, version?⟩⟩
 
 instance textDocumentItemHasFromJson : HasFromJson TextDocumentItem :=
 ⟨fun j => do
   uri ← j.getObjValAs? DocumentUri "uri";
   languageId ← j.getObjValAs? String "languageId";
-  version ← j.getObjValAs? Int "version";
+  version ← j.getObjValAs? Nat "version";
   text ← j.getObjValAs? String "text";
   pure ⟨uri, languageId, version, text⟩⟩
 
@@ -276,18 +195,4 @@ instance locationHasToJson : HasToJson Location :=
 ⟨fun o => mkObj $
   ⟨"uri", toJson o.uri⟩ :: ⟨"range", toJson o.range⟩ :: []⟩
 
-instance diagnosticTagHasToJson : HasToJson DiagnosticTag :=
-⟨fun o => match o with
-  | DiagnosticTag.unnecessary => (1 : Nat)
-  | DiagnosticTag.deprecated  => (2 : Nat)⟩
-
-instance diagnosticRelatedInformationHasToJson : HasToJson DiagnosticRelatedInformation :=
-⟨fun o => mkObj $
-  ⟨"location", toJson o.location⟩ :: ⟨"message", o.message⟩ :: []⟩
-
-instance diagnosticHasToJson : HasToJson Diagnostic :=
-⟨fun o => mkObj $
-  ⟨"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/Server/Server.lean b/src/Lean/Server/Server.lean
index 8bbc3c987c..2f2ddc4555 100644
--- a/src/Lean/Server/Server.lean
+++ b/src/Lean/Server/Server.lean
@@ -2,7 +2,7 @@ import Init.System.IO
 import Std.Data.RBMap
 
 import Lean.Environment
-import Lean.Elab.Frontend
+import Lean.Server.Snapshots
 import Lean.Data.Lsp
 import Lean.Data.Json.FromToJson
 
@@ -15,16 +15,54 @@ open Lean.JsonRpc
 open Lean.Lsp
 open Lean.Elab
 
--- LSP indexes text with rows and colums
-abbrev DocumentText := Array String
 
-structure Document :=
-(version : Int)
+/-- A document editable in the sense that we track the environment
+and parser state after each command so that edits can be applied
+without recompiling code appearing earlier in the file. -/
+structure EditableDocument :=
+(version : Nat)
 (text : DocumentText)
-(headerEnv : Environment)
-(headerParserState : Parser.ModuleParserState)
+/- The first snapshot is that after the header. -/
+(header : Snapshots.Snapshot)
+/- Subsequent snapshots occur after each command. -/
+-- TODO(WN): These should probably be asynchronous Tasks
+(snapshots : List Snapshots.Snapshot)
 
-abbrev DocumentMap := RBMap DocumentUri Document (fun a b => Decidable.decide (a < b))
+/-- Compiles the contents of a Lean file. -/
+def compileDocument (version : Nat) (contents : String)
+  : IO (MessageLog × EditableDocument) := do
+let inputCtx := Parser.mkInputContext contents "<input>";
+emptyEnv ← mkEmptyEnvironment;
+let (headerStx, headerParserState, msgLog) := Parser.parseHeader emptyEnv inputCtx;
+(headerEnv, msgLog) ← Elab.processHeader headerStx msgLog inputCtx;
+let headerSnap : Snapshots.Snapshot := ⟨headerEnv, headerParserState⟩;
+(msgLog, cmdSnaps) ← Snapshots.compileCmdsAfter contents msgLog headerSnap;
+let docOut : EditableDocument := ⟨version, contents.splitOnEOLs.toArray, headerSnap, cmdSnaps⟩;
+pure (msgLog, docOut)
+
+def updateDocument (doc : EditableDocument) (changePos : String.Pos) (newVersion : Nat) (newContents : String)
+  : IO (MessageLog × EditableDocument) :=
+if changePos < doc.header.pos then do -- The header changed, recompile everything.
+  e ← IO.stderr;
+  e.putStrLn $ "\nchangePos = " ++ toString changePos;
+  e.putStrLn "Recompiling header";
+  compileDocument newVersion newContents
+else do
+  e ← IO.stderr;
+  e.putStrLn $ "\nchangePos = " ++ toString changePos;
+  let validSnaps := doc.snapshots.filter (fun snap => snap.pos ≤ changePos);
+  -- The lowest-in-the-file snapshot which is still valid;
+  let lastSnap := validSnaps.getLastD doc.header;
+  e.putStrLn $ "Last snap @ " ++ toString lastSnap.pos;
+  (msgLog, snaps) ← Snapshots.compileCmdsAfter newContents {} lastSnap;
+  let newDoc := { version := newVersion
+                , header := doc.header
+                , text := newContents.splitOnEOLs.toArray
+                , snapshots := doc.snapshots ++ snaps : EditableDocument };
+  pure (msgLog, newDoc)
+
+abbrev DocumentMap :=
+  RBMap DocumentUri EditableDocument (fun a b => Decidable.decide (a < b))
 
 structure ServerState :=
 (i o : FS.Handle)
@@ -35,78 +73,44 @@ match @fromJson? paramType _ params with
 | some parsed => pure parsed
 | none        => throw (userError "got param with wrong structure")
 
-def runFrontend (text : String) : IO (Environment × Environment × Parser.ModuleParserState × MessageLog) := do
-let inputCtx := Parser.mkInputContext text "<input>";
-emptyEnv ← mkEmptyEnvironment;
-match Parser.parseHeader emptyEnv inputCtx with
-| (headerStx, headerParserState, messages) => do
-  (headerEnv, messages) ← processHeader headerStx messages inputCtx;
-  parserStateRef ← IO.mkRef headerParserState;
-  cmdStateRef ← IO.mkRef $ Command.mkState headerEnv messages {};
-  IO.processCommands inputCtx parserStateRef cmdStateRef;
-  cmdState ← cmdStateRef.get;
-  pure (headerEnv, cmdState.env, headerParserState, cmdState.messages)
-
-def updateFrontend (doc : Document) (input : String) : IO (Environment × MessageLog) := do
-let inputCtx := Parser.mkInputContext input "<input>";
-parserStateRef ← IO.mkRef doc.headerParserState;
-cmdStateRef    ← IO.mkRef $ Command.mkState doc.headerEnv;
-IO.processCommands inputCtx parserStateRef cmdStateRef;
-cmdState ← cmdStateRef.get;
-pure (cmdState.env, cmdState.messages)
-
-def msgToDiagnostic (text : DocumentText) (m : Lean.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⟩;
-let high : Lsp.Position := match m.endPos with
-| some endPos =>
-  let highLn := endPos.line - 1;
-  ⟨highLn, (text.get! highLn).codepointPosToUtf16Pos endPos.column⟩
-| none        => low;
-let range : Range := ⟨low, high⟩;
-let severity := match m.severity with
-| MessageSeverity.information => DiagnosticSeverity.information
-| MessageSeverity.warning     => DiagnosticSeverity.warning
-| MessageSeverity.error       => DiagnosticSeverity.error;
-let source := "Lean 4 server";
-let message := toString (format m.data);
-{ range := range
-, severity? := severity
-, source? := source
-, message := message}
+-- def ServerM α := StateT ServerState (IO α)
+-- Computes a task with result type α in the ServerM monad.
+-- def ServerTaskM α := ServerM (Task α)
+-- Handles a request with params of type α and response params β.
+-- def RequestHandler α β := Request α → ServerTaskM (Response β)
 
 namespace ServerState
 
-def findOpenDocument (s : ServerState) (key : DocumentUri) : IO Document := do
+def findOpenDocument (s : ServerState) (key : DocumentUri) : IO EditableDocument := do
 openDocuments ← s.openDocumentsRef.get;
 match openDocuments.find? key with
 | some doc => pure doc
 | none     => throw (userError "got unknown document uri")
 
-def updateOpenDocuments (s : ServerState) (key : DocumentUri) (val : Document) : IO Unit :=
+def updateOpenDocuments (s : ServerState) (key : DocumentUri) (val : EditableDocument) : IO Unit :=
 s.openDocumentsRef.modify (fun documents => (documents.erase key).insert key val)
 
--- Clears diagnostics for the document version 'd'.
+-- Clears diagnostics for the document version 'version'.
 -- TODO how to clear all diagnostics? Sending version 'none' doesn't seem to work
-def clearDiagnostics (s : ServerState) (uri : DocumentUri) (d : Document) : IO Unit :=
+-- TODO arg should be versioneddocumentidentifier
+def clearDiagnostics (s : ServerState) (uri : DocumentUri) (version : Nat) : IO Unit :=
 writeLspNotification s.o "textDocument/publishDiagnostics"
   { uri := uri
-  , version? := d.version
+  , version? := version
   , diagnostics := #[] : PublishDiagnosticsParams }
 
-def sendDiagnostics (s : ServerState) (uri : DocumentUri) (d : Document) (log : MessageLog) : IO Unit :=
-let diagnostics := log.msgs.map (msgToDiagnostic d.text);
+def sendDiagnostics (s : ServerState) (uri : DocumentUri) (doc : EditableDocument)
+  (log : MessageLog) : IO Unit :=
+let diagnostics := log.msgs.map (msgToDiagnostic doc.text);
 writeLspNotification s.o "textDocument/publishDiagnostics"
   { uri := uri
-  , version? := d.version
+  , version? := doc.version
   , diagnostics := diagnostics.toArray : PublishDiagnosticsParams }
 
 def handleDidOpen (s : ServerState) (p : DidOpenTextDocumentParams) : IO Unit := do
 let doc := p.textDocument;
 let text := doc.text.splitOnEOLs;
-(headerEnv, env, headerParserState, msgLog) ← runFrontend ("\n".intercalate text);
-let newDoc : Document := ⟨doc.version, text.toArray, headerEnv, headerParserState⟩;
+(msgLog, newDoc) ← compileDocument doc.version doc.text;
 s.openDocumentsRef.modify (fun openDocuments => openDocuments.insert doc.uri newDoc);
 s.sendDiagnostics doc.uri newDoc msgLog
 
@@ -121,16 +125,20 @@ else changes.forM $ fun change =>
   match change with
   | TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) => do
     let newDocText := replaceRange oldDoc.text range newText;
-    (newEnv, msgLog) ← updateFrontend oldDoc ("\n".intercalate newDocText.toList);
-    let newDoc : Document := ⟨newVersion, newDocText, oldDoc.headerEnv, oldDoc.headerParserState⟩;
+    (msgLog, newDoc) ← updateDocument oldDoc
+                                      (range.start.lnColToLinearPos oldDoc.text)
+                                      newVersion
+                                      ("\n".intercalate newDocText.toList);
     s.updateOpenDocuments docId.uri newDoc;
     -- Clients don't have to clear diagnostics, so we clear them
     -- for the *previous* version here.
-    s.clearDiagnostics docId.uri oldDoc;
+    s.clearDiagnostics docId.uri oldDoc.version;
+    -- TODO(WN): at this point we need to re-add the diagnostics for above the
+    -- part that was recompiled. This should be stored in `Snapshot` probably
     s.sendDiagnostics docId.uri newDoc msgLog
 
   | TextDocumentContentChangeEvent.fullChange (text : String) =>
-    throw (userError "got content change that replaces the full document (not supported)")
+    throw (userError "TODO impl computing the diff of two sources.")
 
 def handleDidClose (s : ServerState) (p : DidCloseTextDocumentParams) : IO Unit := do
 -- TODO is any extra cleanup needed?
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
new file mode 100644
index 0000000000..8cecd81557
--- /dev/null
+++ b/src/Lean/Server/Snapshots.lean
@@ -0,0 +1,70 @@
+import Init.System.IO
+
+import Lean.Elab.Import
+import Lean.Elab.Command
+
+/-! One can think of this module as being a partial reimplementation
+of Lean.Elab.Frontend which also stores a snapshot of the world after
+each command. Importantly, we allow starting compilation from any
+snapshot/position in the file for interactive editing purposes. -/
+
+namespace Lean
+namespace Elab
+namespace Snapshots
+
+/-- What Lean knows about the world after each command. -/
+structure Snapshot :=
+/- The (ln,col) after the command. *Not* the
+same as mpState.pos as that's a linear Nat. -/
+--(pos : Position)
+(env : Environment)
+(mpState : Parser.ModuleParserState)
+--(opts : Options) TODO these are set_option options right? might need to store them
+
+def Snapshot.pos (s : Snapshot) : String.Pos := s.mpState.pos
+
+/-- Compiles the next command occuring after the given snapshot.
+If there is no next command, returns `none`. -/
+-- NOTE(WN): this code is really very similar to Elab.Frontend.
+-- Is there a point in generalizing it over "store snapshots"/"don't store snapshots" via
+-- changing the FrontendM monad? I say no because it would likely result in
+-- confusing isServer? conditionals.
+-- TODO(WN): should probably take inputCtx and live in some SnapshotsM := ReaderT Context (EIO Empty)
+def compileNextCmd (contents : String) (msgLog : MessageLog) (snap : Snapshot)
+  : IO (Option (MessageLog × Snapshot)) := do
+let inputCtx := Parser.mkInputContext contents "<input>";
+let (cmdStx, cmdParserState, msgLog) :=
+  Parser.parseCommand snap.env inputCtx snap.mpState msgLog;
+e ← IO.stderr;
+e.putStrLn $ "Cmd @ " ++ toString snap.pos ++ " = " ++ (toString $ cmdStx.formatStx none true);
+if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
+  pure none
+else do
+  cmdStateRef ← IO.mkRef $ Elab.Command.mkState snap.env msgLog { : Options };
+  let cmdCtx : Elab.Command.Context :=
+    { cmdPos := snap.pos
+    , stateRef := cmdStateRef
+    , fileName := inputCtx.fileName
+    , fileMap := inputCtx.fileMap };
+  EIO.adaptExcept
+    (fun e => unreachable!) -- TODO(WN): ignoring exceptions ok here?
+    (Elab.Command.withLogging
+      (Elab.Command.elabCommand cmdStx)
+      cmdCtx);
+  postCmdState ← cmdStateRef.get;
+  let postCmdSnap : Snapshot := ⟨postCmdState.env, cmdParserState⟩;
+  pure $ some (postCmdState.messages, postCmdSnap)
+
+partial def compileCmdsAfter (contents : String) : MessageLog → Snapshot
+  → IO (MessageLog × List Snapshot)
+| msgLog, snap => do
+  cmdOut ← compileNextCmd contents msgLog snap;
+  match cmdOut with
+  | some (msgLog, snap) => do
+    (msgLog, snaps) ← compileCmdsAfter msgLog snap;
+    pure (msgLog, snap :: snaps)
+  | none => pure (msgLog, [])
+
+end Snapshots
+end Elab
+end Lean