diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index e58f05f1a8..613441b5bc 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -14,10 +14,6 @@ namespace Lean
 namespace Elab
 namespace Command
 
-structure Context :=
-(fileName : String)
-(fileMap  : FileMap)
-
 structure Scope :=
 (kind          : String)
 (header        : String)
@@ -32,7 +28,6 @@ instance Scope.inhabited : Inhabited Scope := ⟨{ kind := "", header := "" }⟩
 structure State :=
 (env      : Environment)
 (messages : MessageLog := {})
-(cmdPos   : String.Pos := 0)
 (scopes   : List Scope := [{ kind := "root", header := "" }])
 
 instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
@@ -40,11 +35,44 @@ instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State :=
 { env := env, messages := messages, scopes := [{ kind := "root", header := "", opts := opts }] }
 
-abbrev CommandElabM := ReaderT Context (EStateM Exception State)
+structure Context :=
+(fileName : String)
+(fileMap  : FileMap)
+(stateRef : IO.Ref State)
+(cmdPos   : String.Pos := 0)
+
+abbrev CommandElabCoreM (ε) := ReaderT Context (EIO ε)
+abbrev CommandElabM := CommandElabCoreM Exception
 abbrev CommandElab  := SyntaxNode → CommandElabM Unit
 
+def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
+mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
+
+private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
+mkMessageAux ctx ref ("IO error, " ++ toString err) MessageSeverity.error
+
+@[inline] def liftIOCore {α} (ctx : Context) (ref : Syntax) (x : IO α) : EIO Exception α :=
+EIO.adaptExcept (ioErrorToMessage ctx ref) x
+
+@[inline] def liftIO {α} (ref : Syntax) (x : IO α) : CommandElabM α :=
+fun ctx => liftIOCore ctx ref x
+
+private def getState : CommandElabM State :=
+fun ctx => liftIOCore ctx Syntax.missing $ ctx.stateRef.get
+
+private def setState (s : State) : CommandElabM Unit :=
+fun ctx => liftIOCore ctx Syntax.missing $ ctx.stateRef.set s
+
+@[inline] private def modifyGetState {α} (f : State → α × State) : CommandElabM α := do
+s ← getState; let (a, s) := f s; setState s; pure a
+
+instance CommandElabCoreM.monadState : MonadState State CommandElabM :=
+{ get       := getState,
+  set       := setState,
+  modifyGet := @modifyGetState }
+
 instance CommandElabM.monadLog : MonadLog CommandElabM :=
-{ getCmdPos   := do s ← get; pure s.cmdPos,
+{ getCmdPos   := do ctx ← read; pure ctx.cmdPos,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
   logMessage  := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
@@ -107,7 +135,7 @@ let scope := s.scopes.head!;
 { config         := { opts := scope.opts, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true },
   fileName       := ctx.fileName,
   fileMap        := ctx.fileMap,
-  cmdPos         := s.cmdPos,
+  cmdPos         := ctx.cmdPos,
   currNamespace  := scope.currNamespace,
   univNames      := scope.univNames,
   openDecls      := scope.openDecls }
@@ -125,8 +153,22 @@ match result with
 | EStateM.Result.error (Term.Exception.error ex) newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, .. s }
 | EStateM.Result.error Term.Exception.postpone newS   => unreachable!
 
-@[inline] def runTermElabM {α} (x : TermElabM α) : CommandElabM α :=
-fun ctx s => toCommandResult ctx s $ (Term.elabBinders (getVarDecls s) (fun _ => x)) (mkTermContext ctx s) (mkTermState s)
+instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
+⟨throw $ arbitrary _⟩
+
+@[inline] def runTermElabM {α} (x : TermElabM α) : CommandElabM α := do
+ctx ← read;
+s ← get;
+match ((Term.elabBinders (getVarDecls s) (fun _ => x)) (mkTermContext ctx s)).run (mkTermState s) with
+| EStateM.Result.ok a newS                            => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
+| EStateM.Result.error (Term.Exception.error ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
+| EStateM.Result.error Term.Exception.postpone newS   => unreachable!
+
+@[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
+catch x (fun ex => do logMessage ex; pure ())
+
+@[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit :=
+fun ctx => EIO.catchExceptions (withLogging x ctx) (fun _ => pure ())
 
 def dbgTrace {α} [HasToString α] (a : α) : CommandElabM Unit :=
 _root_.dbgTrace (toString a) $ fun _ => pure ()
diff --git a/src/Init/Lean/Elab/Frontend.lean b/src/Init/Lean/Elab/Frontend.lean
index 9bdca702fa..cd8db204fd 100644
--- a/src/Init/Lean/Elab/Frontend.lean
+++ b/src/Init/Lean/Elab/Frontend.lean
@@ -11,40 +11,52 @@ namespace Lean
 namespace Elab
 namespace Frontend
 
-structure State :=
-(commandState : Command.State)
-(parserState  : Parser.ModuleParserState)
+structure Context :=
+(commandStateRef : IO.Ref Command.State)
+(parserStateRef  : IO.Ref Parser.ModuleParserState)
+(cmdPosRef       : IO.Ref String.Pos)
+(parserCtx       : Parser.ParserContextCore)
 
-abbrev FrontendM := ReaderT Parser.ParserContextCore (StateM State)
+abbrev FrontendM := ReaderT Context (EIO Empty)
 
-private def getCmdContext : FrontendM Command.Context := do
-c ← read;
-pure { fileName := c.fileName, fileMap := c.fileMap }
+@[inline] def liftIOCore! {α} [Inhabited α] (x : IO α) : EIO Empty α :=
+EIO.catchExceptions x (fun _ => unreachable!)
 
-@[inline] def runCommandElabM (x : Command.CommandElabM Unit) : FrontendM Unit := do
-fun ctx s =>
-  let parserState := s.parserState;
-  match x { fileName := ctx.fileName, fileMap := ctx.fileMap } s.commandState with
-  | EStateM.Result.ok _ newCmdState     => ((), { commandState := newCmdState, parserState := parserState })
-  | EStateM.Result.error ex newCmdState =>
-    let newCmdState := { messages := newCmdState.messages.add ex, .. newCmdState };
-    ((), { commandState := newCmdState, parserState := parserState })
+@[inline] def runCommandElabM (x : Command.CommandElabM Unit) : FrontendM Unit :=
+fun ctx => do
+  cmdPos ← liftIOCore! $ ctx.cmdPosRef.get;
+  let cmdCtx : Command.Context := { cmdPos := cmdPos, stateRef := ctx.commandStateRef, fileName := ctx.parserCtx.fileName, fileMap := ctx.parserCtx.fileMap };
+  EIO.catchExceptions (x cmdCtx) (fun _ => pure ())
 
 def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit :=
-runCommandElabM (Command.elabCommand stx)
+runCommandElabM (Command.withLogging $ Command.elabCommand stx)
 
 def updateCmdPos : FrontendM Unit :=
-modify $ fun s => { commandState := { cmdPos := s.parserState.pos, .. s.commandState }, .. s }
+fun ctx => do
+  parserState ← liftIOCore! $ ctx.parserStateRef.get;
+  liftIOCore! $ ctx.cmdPosRef.set parserState.pos
+
+def getParserState : FrontendM Parser.ModuleParserState :=
+fun ctx => liftIOCore! $ ctx.parserStateRef.get
+
+def getCommandState : FrontendM Command.State :=
+fun ctx => liftIOCore! $ ctx.commandStateRef.get
+
+def setParserState (ps : Parser.ModuleParserState) : FrontendM Unit :=
+fun ctx => liftIOCore! $ ctx.parserStateRef.set ps
+
+def setMessages (msgs : MessageLog) : FrontendM Unit :=
+fun ctx => liftIOCore! $ ctx.commandStateRef.modify $ fun s => { messages := msgs, .. s }
 
 def processCommand : FrontendM Bool := do
 updateCmdPos;
-s ← get;
-let cs := s.commandState;
-let ps := s.parserState;
+cs ← getCommandState;
+ps ← getParserState;
 c ← read;
-match Parser.parseCommand cs.env c ps cs.messages with
+match Parser.parseCommand cs.env c.parserCtx ps cs.messages with
 | (cmd, ps, messages) => do
-  set { commandState := { messages := messages, .. cs }, parserState := ps };
+  setParserState ps;
+  setMessages messages;
   if Parser.isEOI cmd || Parser.isExitCommand cmd then do
     pure true -- Done
   else do
@@ -64,23 +76,33 @@ end Frontend
 
 open Frontend
 
-def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : Environment × MessageLog :=
-let fileName        := fileName.getD "<input>";
-let ctx             := Parser.mkParserContextCore env input fileName;
-let cmdState        := Command.mkState env {} opts;
-match (processCommands ctx).run { commandState := cmdState, parserState := {} } with
-| (_, { commandState := { env := env, messages := messages, .. }, .. }) => (env, messages)
+def IO.processCommands (parserCtx : Parser.ParserContextCore) (parserStateRef : IO.Ref Parser.ModuleParserState) (cmdStateRef : IO.Ref Command.State) : IO Unit := do
+ps ← parserStateRef.get;
+cmdPosRef ← IO.mkRef ps.pos;
+EIO.adaptExcept (fun (ex : Empty) => unreachable!) $ -- TODO: compiler support for Empty.rec is missing
+  processCommands { commandStateRef := cmdStateRef, parserStateRef := parserStateRef, cmdPosRef := cmdPosRef, parserCtx := parserCtx }
+
+def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
+let fileName   := fileName.getD "<input>";
+let parserCtx  := Parser.mkParserContextCore env input fileName;
+parserStateRef ← IO.mkRef { Parser.ModuleParserState . };
+cmdStateRef    ← IO.mkRef $ Command.mkState env {} opts;
+IO.processCommands parserCtx parserStateRef cmdStateRef;
+cmdState ← cmdStateRef.get;
+pure (cmdState.env, cmdState.messages)
 
 def testFrontend (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) := do
 env ← mkEmptyEnvironment;
 let fileName := fileName.getD "<input>";
-let ctx := Parser.mkParserContextCore env input fileName;
-match Parser.parseHeader env ctx with
+let parserCtx := Parser.mkParserContextCore env input fileName;
+match Parser.parseHeader env parserCtx with
 | (header, parserState, messages) => do
-  (env, messages) ← processHeader header messages ctx;
-  let cmdState := Command.mkState env messages opts;
-  match (processCommands ctx).run { commandState := cmdState, parserState := parserState } with
-  | (_, { commandState := { env := env, messages := messages, .. }, .. }) => pure (env, messages)
+  (env, messages) ← processHeader header messages parserCtx;
+  parserStateRef ← IO.mkRef parserState;
+  cmdStateRef    ← IO.mkRef $ Command.mkState env messages opts;
+  IO.processCommands parserCtx parserStateRef cmdStateRef;
+  cmdState ← cmdStateRef.get;
+  pure (cmdState.env, cmdState.messages)
 
 end Elab
 end Lean
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 9e6d0a627a..14ef4b2ce0 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -26,9 +26,9 @@ def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld
 @[inline] def EIO.adaptExcept {α ε ε'} (f : ε → ε') (x : EIO ε α) : EIO ε' α :=
 EStateM.adaptExcept f x
 
-@[inline] def EIO.catchExceptions {ε} (x : EIO ε Unit) (h : ε → EIO Empty Unit) : EIO Empty Unit :=
+@[inline] def EIO.catchExceptions {α ε} (x : EIO ε α) (h : ε → EIO Empty α) : EIO Empty α :=
 fun s => match x s with
-| EStateM.Result.ok _ s     => EStateM.Result.ok () s
+| EStateM.Result.ok a s     => EStateM.Result.ok a s
 | EStateM.Result.error ex s => h ex s
 
 instance (ε : Type) : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index ef0785b473..37042a2dce 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -5,7 +5,7 @@ open Lean.Elab
 def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
 do env  ← MetaIO.getEnv;
    opts ← MetaIO.getOptions;
-   let (env, messages) := process input env opts;
+   (env, messages) ← liftM $ process input env opts;
    messages.forM $ fun msg => IO.println msg;
    when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
    when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index 0d509672c5..b6342aba1f 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -5,7 +5,7 @@ open Lean.Elab
 def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
 do env  ← MetaIO.getEnv;
    opts ← MetaIO.getOptions;
-   let (env, messages) := process input env opts;
+   (env, messages) ← liftM $ process input env opts;
    messages.toList.forM $ fun msg => IO.println msg;
    when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
    when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");