diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean
index ae85db241e..553acac73f 100644
--- a/library/init/control/estate.lean
+++ b/library/init/control/estate.lean
@@ -134,6 +134,15 @@ instance : MonadState σ (EState ε σ) :=
 instance : MonadExcept ε (EState ε σ) :=
 { throw := @EState.throw _ _, catch := @EState.catch _ _ }
 
+@[inline] def adaptState {σ₁ σ₂} (x : EState ε σ₁ α) (split : σ → σ₁ × σ₂) (merge : σ₁ → σ₂ → σ) : EState ε σ α :=
+fun r => match r with
+  | ⟨Result.error _ _, h⟩ => unreachableError h
+  | ⟨Result.ok _ s, _⟩    =>
+    let (s₁, s₂) := split s;
+    match x (resultOk.mk ⟨⟩ s₁) with
+    | Result.ok a s₁    => Result.ok a (merge s₁ s₂)
+    | Result.error e s₁ => Result.error e (merge s₁ s₂)
+
 @[inline] def run (x : EState ε σ α) (s : σ) : Result ε σ α :=
 x (resultOk.mk ⟨⟩ s)
 
diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index 04fcf7e8dc..1c9c4ac8ca 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -4,18 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
+import init.control.reader
 import init.lean.namegenerator
 import init.lean.scopes
 import init.lean.parser.module
 
 namespace Lean
 
+structure ElabContext :=
+(fileName : String)
+(fileMap  : FileMap)
+
 structure ElabScope :=
 (options : Options := {})
 
 structure ElabState :=
 (env      : Environment)
-(parser   : Parser.ModuleParser)
+(messages : MessageLog := {})
 (cmdPos   : String.Pos := 0)
 (ngen     : NameGenerator := {})
 (scopes   : List ElabScope := [])
@@ -31,7 +36,7 @@ instance : Inhabited ElabException := ⟨other "error"⟩
 
 end ElabException
 
-abbrev Elab := EState ElabException ElabState
+abbrev Elab := ReaderT ElabContext (EState ElabException ElabState)
 
 abbrev TermElab    := Syntax → Elab Expr
 abbrev CommandElab := Syntax → Elab Unit
@@ -180,11 +185,10 @@ mkElabAttribute `commandTerm "command" builtinCommandElabTable
 constant commandElabAttribute : CommandElabAttribute := default _
 
 def logErrorAt (pos : String.Pos) (errorMsg : String) : Elab Unit :=
-do s ← get;
-   let ctx := s.parser.context;
+do ctx ← read;
    let pos := ctx.fileMap.toPosition pos;
-   let msg := { Message . filename := ctx.filename, pos := pos, text := errorMsg };
-   modify (fun s => { parser := { messages := s.parser.messages.add msg, .. s.parser }, .. s })
+   let msg := { Message . filename := ctx.fileName, pos := pos, text := errorMsg };
+   modify (fun s => { messages := s.messages.add msg, .. s })
 
 def logErrorUsingCmdPos (errorMsg : String) : Elab Unit :=
 do s ← get;
@@ -223,61 +227,72 @@ match stx with
   | none      => logError stx ("command elaborator failed, no support for syntax '" ++ toString k ++ "'")
 | _ => logErrorUsingCmdPos ("command elaborator failed, unexpected syntax")
 
-def mkElabState (env : Environment) (parser : Parser.ModuleParser) : ElabState :=
-{ env := env, parser := parser }
+structure FrontendState :=
+(elabState   : ElabState)
+(parserState : Parser.ModuleParserState)
 
-def updateParser (p : Parser.ModuleParser) : Elab Unit :=
-modify (fun s => { parser := p, .. s })
+abbrev Frontend := ReaderT Parser.ParserContextCore (EState ElabException FrontendState)
 
-def updateCmdPos : Elab Unit :=
-modify (fun s => { cmdPos := s.parser.pos, .. s })
+def getElabContext : Frontend ElabContext :=
+do c ← read;
+   pure { fileName := c.filename, fileMap := c.fileMap }
 
-def processCommand : Elab Bool :=
+def elabCommandAtFrontend (stx : Syntax) : Frontend Unit :=
+do c ← getElabContext;
+   monadLift $ EState.adaptState (elabCommand stx c)
+      (fun (s : FrontendState) => (s.elabState, s.parserState))
+      (fun es ps => { elabState := es, parserState := ps })
+
+def updateCmdPos : Frontend Unit :=
+modify $ fun s => { elabState := { cmdPos := s.parserState.pos, .. s.elabState }, .. s }
+
+def processCommand : Frontend Bool :=
 do updateCmdPos;
    s ← get;
-   let p         := s.parser;
-   match Parser.parseCommand s.env p with
-   | (stx, p) => do
-     updateParser p;
-     if Parser.isEOI stx || Parser.isExitCommand stx then do
+   let es := s.elabState;
+   let ps := s.parserState;
+   c ← read;
+   match Parser.parseCommand es.env c ps es.messages with
+   | (cmd, ps, messages) => do
+     set { elabState := { messages := messages, .. es }, parserState := ps };
+     if Parser.isEOI cmd || Parser.isExitCommand cmd then do
        pure true -- Done
      else do
-       elabCommand stx;
+       elabCommandAtFrontend cmd;
        pure false
 
-partial def processCommandsAux : Unit → Elab Unit
+partial def processCommandsAux : Unit → Frontend Unit
 | () := do
   done ← processCommand;
   if done then pure ()
   else processCommandsAux ()
 
-def processCommands : Elab Unit :=
+def processCommands : Frontend Unit :=
 processCommandsAux ()
 
-def processHeader (header : Syntax) (messages : MessageLog) : IO (Option Environment × MessageLog) :=
+def processHeader (header : Syntax) (messages : MessageLog) : IO (Environment × MessageLog) :=
 do IO.println header;
    -- TODO
    env ← mkEmptyEnvironment;
-   pure (some env, messages)
+   pure (env, messages)
 
-def testFrontend (input : String) (filename := "<input>") : IO (Option Environment × MessageLog) :=
+def testFrontend (input : String) (fileName := "<input>") : IO (Environment × MessageLog) :=
 do env ← mkEmptyEnvironment;
-   let (stx, p) := Parser.mkModuleParser env input filename;
-   match stx with
-   | none => pure (none, p.messages)
-   | some stx => do
-     (optEnv, messages) ← processHeader stx p.messages;
-     match optEnv with
-     | none => pure (none, messages)
-     | some env =>
-       let p := { messages := messages, .. p };
-       let s := mkElabState env p;
-       match processCommands.run s with
-       | EState.Result.ok _ s    => pure (some s.env, s.parser.messages)
-       | EState.Result.error _ s => pure (none, s.parser.messages)
+   let ctx := Parser.mkParserContextCore env input fileName;
+   match Parser.parseHeader env ctx with
+   | (header, parserState, messages) => do
+     (env, messages) ← processHeader header messages;
+     let elabState := { ElabState . env := env, messages := messages };
+     match (processCommands ctx).run { elabState := elabState, parserState := parserState } with
+       | EState.Result.ok _ s    => pure (s.elabState.env, s.elabState.messages)
+       | EState.Result.error _ s => pure (s.elabState.env, s.elabState.messages)
+
 
 namespace Elab
 
+instance {α} : Inhabited (Elab α) :=
+⟨fun _ => default _⟩
+
 /- Remark: in an ideal world where performance doesn't matter, we would define `Elab` as
    ```
    ExceptT ElabException (StateT ElabException IO)
diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean
index 099866b8e4..2d24fd9ac2 100644
--- a/library/init/lean/message.lean
+++ b/library/init/lean/message.lean
@@ -45,7 +45,9 @@ structure MessageLog :=
 (revList : List Message := [])
 
 namespace MessageLog
-def empty : MessageLog := ⟨[]⟩
+def empty : MessageLog := ⟨{}⟩
+
+instance : Inhabited MessageLog := ⟨{}⟩
 
 def add (msg : Message) (log : MessageLog) : MessageLog :=
 ⟨msg :: log.revList⟩
diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean
index 9d23d6eb9c..8d4f374cc0 100644
--- a/library/init/lean/parser/module.lean
+++ b/library/init/lean/parser/module.lean
@@ -24,32 +24,30 @@ def updateTokens (c : ParserContext) : ParserContext :=
 
 end Module
 
-structure ModuleParser :=
-(context    : ParserContextCore)
+structure ModuleParserState :=
 (pos        : String.Pos := 0)
-(messages   : MessageLog := {})
-(recovering : Bool := false)
+(recovering : Bool       := false)
 
-instance ModuleParser.inhabited : Inhabited ModuleParser :=
-⟨{context := default _}⟩
+instance ModuleParserState.inhabited : Inhabited ModuleParserState :=
+⟨{}⟩
 
 private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message :=
 let pos := c.fileMap.toPosition pos;
 { filename := c.filename, pos := pos, text := errorMsg }
 
-def mkModuleParser (env : Environment) (input : String) (filename := "<input>") : Option Syntax × ModuleParser :=
-let c   := mkParserContext env input filename;
+def parseHeader (env : Environment) (c : ParserContextCore) : Syntax × ModuleParserState × MessageLog :=
+let c   := c.toParserContext env;
 let c   := Module.updateTokens c;
-let s   := mkParserState input;
+let s   := mkParserState c.input;
 let s   := whitespace c s;
 let s   := Module.header.fn (0:Nat) c s;
+let stx := s.stxStack.back;
 match s.errorMsg with
 | some errorMsg =>
   let msg := mkErrorMessage c s.pos (toString errorMsg);
-  (none, { context := c.toParserContextCore, pos := s.pos, messages := { MessageLog . }.add msg, recovering := true })
+  (stx, { pos := s.pos, recovering := true }, { MessageLog . }.add msg)
 | none =>
-  let stx := s.stxStack.back;
-  (stx, { context := c.toParserContextCore, pos := s.pos })
+  (stx, { pos := s.pos }, {})
 
 private def mkEOI (pos : String.Pos) : Syntax :=
 let atom := mkAtom { pos := pos, trailing := "".toSubstring, leading := "".toSubstring } "";
@@ -68,45 +66,44 @@ match s.errorMsg with
 | some _ => pos + 1
 | none   => s.pos
 
-partial def parseCommand (env : Environment) : ModuleParser → Syntax × ModuleParser
-| p :=
-  if p.context.input.atEnd p.pos then
-    (mkEOI p.pos, p)
+partial def parseCommand (env : Environment) (c : ParserContextCore) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog
+| s@{ pos := pos, recovering := recovering } messages :=
+  if c.input.atEnd pos then
+    (mkEOI pos, s, messages)
   else
-    let c : ParserContext := { env := env, .. p.context };
-    let s : ParserState   := { cache := initCacheForInput c.input, pos := p.pos };
-    let s := (commandParser : Parser).fn (0:Nat) c s;
+    let c  := c.toParserContext env;
+    let s  := { ParserState . cache := initCacheForInput c.input, pos := pos };
+    let s  := (commandParser : Parser).fn (0:Nat) c s;
     match s.errorMsg with
     | none =>
       let stx := s.stxStack.back;
-      let p   := { pos := s.pos, recovering := false, .. p };
-      (stx, p)
+      (stx, { pos := s.pos }, messages)
     | some errorMsg =>
-      if p.recovering then
-        let p := { pos := consumeInput c s.pos, .. p };
-        parseCommand p
+      if recovering then
+        parseCommand { pos := consumeInput c s.pos, recovering := true } messages
       else
-        let msg := mkErrorMessage c s.pos (toString errorMsg);
-        let p   := { pos := s.pos, recovering := true, messages := p.messages.add msg, .. p };
-        parseCommand p
+        let msg      := mkErrorMessage c s.pos (toString errorMsg);
+        let messages := messages.add msg;
+        parseCommand { pos := consumeInput c s.pos, recovering := true } messages
 
-private partial def testModuleParserAux (env : Environment) (displayStx : Bool) : ModuleParser → IO Bool
-| p :=
-  match parseCommand env p with
-  | (stx, p) =>
+private partial def testModuleParserAux (env : Environment) (c : ParserContextCore) (displayStx : Bool) : ModuleParserState → MessageLog → IO Bool
+| s messages :=
+  match parseCommand env c s messages with
+  | (stx, s, messages) =>
     if isEOI stx || isExitCommand stx then do
-      p.messages.toList.mfor $ fun msg => IO.println msg;
-      pure (!p.messages.hasErrors)
+      messages.toList.mfor $ fun msg => IO.println msg;
+      pure (!messages.hasErrors)
     else do
       when displayStx (IO.println stx);
-      testModuleParserAux p
+      testModuleParserAux s messages
 
 @[export lean.test_module_parser_core]
 def testModuleParser (env : Environment) (input : String) (filename := "<input>") (displayStx := false) : IO Bool :=
 timeit (filename ++ " parser") $ do
-  let (stx, p) := mkModuleParser env input filename;
+  let ctx                := mkParserContextCore env input filename;
+  let (stx, s, messages) := parseHeader env ctx;
   when displayStx (IO.println stx);
-  testModuleParserAux env displayStx p
+  testModuleParserAux env ctx displayStx s messages
 
 end Parser
 end Lean
diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 8bfded03e2..76f4766424 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -1381,13 +1381,18 @@ def getSyntaxNodeKinds : IO (List SyntaxNodeKind) :=
 do s ← syntaxNodeKindSetRef.get;
    pure $ s.fold (fun ks k _ => k::ks) []
 
-def mkParserContext (env : Environment) (input : String) (filename : String) : ParserContext :=
-{ env      := env,
-  input    := input,
+def mkParserContextCore (env : Environment) (input : String) (filename : String) : ParserContextCore :=
+{ input    := input,
   filename := filename,
   fileMap  := input.toFileMap,
   tokens   := tokenTableAttribute.ext.getState env }
 
+@[inline] def ParserContextCore.toParserContext (env : Environment) (ctx : ParserContextCore) : ParserContext :=
+{ env := env, toParserContextCore := ctx }
+
+def mkParserContext (env : Environment) (input : String) (filename : String) : ParserContext :=
+(mkParserContextCore env input filename).toParserContext env
+
 def mkParserState (input : String) : ParserState :=
 { cache := initCacheForInput input }