diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index 387b172da3..1cdecbdff1 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,10 +7,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 import Lean.Elab.Import
 import Lean.Elab.Command
 
-namespace Lean
-namespace Elab
-namespace Frontend
-
+namespace Lean.Elab.Frontend
 structure State :=
 (commandState : Command.State)
 (parserState  : Parser.ModuleParserState)
@@ -24,10 +22,10 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
 modify fun s => { s with commandState := commandState }
 
 @[inline] def runCommandElabM (x : Command.CommandElabM Unit) : FrontendM Unit := do
-ctx ← read;
-s ← get;
-let cmdCtx : Command.Context := { cmdPos := s.cmdPos, fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap };
-sNew? ← liftM $ EIO.toIO (fun _ => IO.Error.userError "unexpected error") (do (_, s) ← (x cmdCtx).run s.commandState; pure $ some s);
+let ctx ← read
+let s ← get
+let cmdCtx : Command.Context := { cmdPos := s.cmdPos, fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap }
+let sNew? ← liftM $ EIO.toIO (fun _ => IO.Error.userError "unexpected error") (do (_, s) ← (x cmdCtx).run s.commandState; pure $ some s)
 match sNew? with
 | some sNew => setCommandState sNew
 | none      => pure ()
@@ -38,63 +36,56 @@ runCommandElabM (Command.elabCommand stx)
 def updateCmdPos : FrontendM Unit := do
 modify fun s => { s with cmdPos := s.parserState.pos }
 
-def getParserState : FrontendM Parser.ModuleParserState := do s ← get; pure s.parserState
-def getCommandState : FrontendM Command.State := do s ← get; pure s.commandState
+def getParserState : FrontendM Parser.ModuleParserState := do pure (← get).parserState
+def getCommandState : FrontendM Command.State := do pure (← get).commandState
 def setParserState (ps : Parser.ModuleParserState) : FrontendM Unit := modify fun s => { s with parserState := ps }
 def setMessages (msgs : MessageLog) : FrontendM Unit := modify fun s => { s with commandState := { s.commandState with messages := msgs } }
-def getInputContext : FrontendM Parser.InputContext := do ctx ← read; pure ctx.inputCtx
+def getInputContext : FrontendM Parser.InputContext := do pure (← read).inputCtx
 
 def processCommand : FrontendM Bool := do
-updateCmdPos;
-cmdState    ← getCommandState;
-parserState ← getParserState;
-inputCtx    ← getInputContext;
-match Parser.parseCommand cmdState.env inputCtx parserState cmdState.messages with
-| (cmd, ps, messages) => do
-  setParserState ps;
-  setMessages messages;
-  if Parser.isEOI cmd || Parser.isExitCommand cmd then do
+updateCmdPos
+let cmdState ← getCommandState
+match Parser.parseCommand cmdState.env (← getInputContext) (← getParserState) cmdState.messages with
+| (cmd, ps, messages) =>
+  setParserState ps
+  setMessages messages
+  if Parser.isEOI cmd || Parser.isExitCommand cmd then
     pure true -- Done
-  else do
-    elabCommandAtFrontend cmd;
+  else
+    elabCommandAtFrontend cmd
     pure false
 
-partial def processCommandsAux : Unit → FrontendM Unit
-| () => do
-  done ← processCommand;
-  if done then pure ()
-  else processCommandsAux ()
-
-def processCommands : FrontendM Unit :=
-processCommandsAux ()
+partial def processCommands : FrontendM Unit := do
+let done ← processCommand
+unless done do
+  processCommands
 
 end Frontend
 
 open Frontend
 
 def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO Command.State := do
-(_, s) ← (processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos };
+let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
 pure s.commandState
 
 def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
-let fileName   := fileName.getD "<input>";
-let inputCtx   := Parser.mkInputContext input fileName;
-commandState ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts);
+let fileName   := fileName.getD "<input>"
+let inputCtx   := Parser.mkInputContext input fileName
+let commandState ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
 pure (commandState.env, commandState.messages)
 
 @[export lean_process_input]
 def processExport (env : Environment) (input : String) (opts : Options) (fileName : String) : IO (Environment × List Message) := do
-(env, messages) ← process input env opts fileName;
+let (env, messages) ← process input env opts fileName
 pure (env, messages.toList)
 
 @[export lean_run_frontend]
 def runFrontend (env : Environment) (input : String) (opts : Options) (fileName : String) : IO (Environment × List Message) := do
-let inputCtx := Parser.mkInputContext input fileName;
+let inputCtx := Parser.mkInputContext input fileName
 match Parser.parseHeader env inputCtx with
-| (header, parserState, messages) => do
-  (env, messages) ← processHeader header messages inputCtx;
-  cmdState ← IO.processCommands inputCtx parserState (Command.mkState env messages opts);
+| (header, parserState, messages) =>
+  let (env, messages) ← processHeader header messages inputCtx
+  let cmdState ← IO.processCommands inputCtx parserState (Command.mkState env messages opts)
   pure (cmdState.env, cmdState.messages.toList)
 
-end Elab
-end Lean
+end Lean.Elab