diff --git a/src/Init/Lean/Elab/Frontend.lean b/src/Init/Lean/Elab/Frontend.lean
index 654f4d0027..a3ecc36393 100644
--- a/src/Init/Lean/Elab/Frontend.lean
+++ b/src/Init/Lean/Elab/Frontend.lean
@@ -15,7 +15,7 @@ structure Context :=
 (commandStateRef : IO.Ref Command.State)
 (parserStateRef  : IO.Ref Parser.ModuleParserState)
 (cmdPosRef       : IO.Ref String.Pos)
-(parserCtx       : Parser.ParserContextCore)
+(inputCtx        : Parser.InputContext)
 
 abbrev FrontendM := ReaderT Context (EIO Empty)
 
@@ -25,7 +25,7 @@ EIO.catchExceptions x (fun _ => unreachable!)
 @[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 };
+  let cmdCtx : Command.Context := { cmdPos := cmdPos, stateRef := ctx.commandStateRef, fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap };
   EIO.catchExceptions (x cmdCtx) (fun _ => pure ())
 
 def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit :=
@@ -48,17 +48,15 @@ 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 getParserContext : FrontendM Parser.ParserContextCore := do
-cs  ← getCommandState;
-ctx ← read;
-pure { tokens := Parser.getTokenTable cs.env, .. ctx.parserCtx }
+def getInputContext : FrontendM Parser.InputContext := do
+ctx ← read; pure ctx.inputCtx
 
 def processCommand : FrontendM Bool := do
 updateCmdPos;
-cs ← getCommandState;
-ps ← getParserState;
-px ← getParserContext;
-match Parser.parseCommand cs.env px ps cs.messages with
+cmdState    ← getCommandState;
+parserState ← getParserState;
+inputCtx    ← getInputContext;
+match Parser.parseCommand cmdState.env inputCtx parserState cmdState.messages with
 | (cmd, ps, messages) => do
   setParserState ps;
   setMessages messages;
@@ -81,18 +79,18 @@ end Frontend
 
 open Frontend
 
-def IO.processCommands (parserCtx : Parser.ParserContextCore) (parserStateRef : IO.Ref Parser.ModuleParserState) (cmdStateRef : IO.Ref Command.State) : IO Unit := do
+def IO.processCommands (inputCtx : Parser.InputContext) (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) => Empty.rec _ ex) $
-  processCommands { commandStateRef := cmdStateRef, parserStateRef := parserStateRef, cmdPosRef := cmdPosRef, parserCtx := parserCtx }
+  processCommands { commandStateRef := cmdStateRef, parserStateRef := parserStateRef, cmdPosRef := cmdPosRef, inputCtx := inputCtx }
 
 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;
+let inputCtx   := Parser.mkInputContext input fileName;
 parserStateRef ← IO.mkRef { Parser.ModuleParserState . };
 cmdStateRef    ← IO.mkRef $ Command.mkState env {} opts;
-IO.processCommands parserCtx parserStateRef cmdStateRef;
+IO.processCommands inputCtx parserStateRef cmdStateRef;
 cmdState ← cmdStateRef.get;
 pure (cmdState.env, cmdState.messages)
 
@@ -103,13 +101,13 @@ pure (env, messages.toList)
 
 def runFrontend (env : Environment) (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) := do
 let fileName := fileName.getD "<input>";
-let parserCtx := Parser.mkParserContextCore env input fileName;
-match Parser.parseHeader env parserCtx with
+let inputCtx := Parser.mkInputContext input fileName;
+match Parser.parseHeader env inputCtx with
 | (header, parserState, messages) => do
-  (env, messages) ← processHeader header messages parserCtx;
+  (env, messages) ← processHeader header messages inputCtx;
   parserStateRef ← IO.mkRef parserState;
   cmdStateRef    ← IO.mkRef $ Command.mkState env messages opts;
-  IO.processCommands parserCtx parserStateRef cmdStateRef;
+  IO.processCommands inputCtx parserStateRef cmdStateRef;
   cmdState ← cmdStateRef.get;
   pure (cmdState.env, cmdState.messages)
 
diff --git a/src/Init/Lean/Elab/Import.lean b/src/Init/Lean/Elab/Import.lean
index 35ea571892..4d5ac679e0 100644
--- a/src/Init/Lean/Elab/Import.lean
+++ b/src/Init/Lean/Elab/Import.lean
@@ -18,23 +18,23 @@ imports ++ (header.getArg 1).getArgs.toList.map (fun stx =>
   let id      := stx.getIdAt 2;
   { module := normalizeModuleName id, runtimeOnly := runtime })
 
-def processHeader (header : Syntax) (messages : MessageLog) (ctx : Parser.ParserContextCore) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) :=
+def processHeader (header : Syntax) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) :=
 catch
   (do env ← importModules (headerToImports header) trustLevel;
       pure (env, messages))
   (fun e => do
      env ← mkEmptyEnvironment;
      let spos := header.getPos.getD 0;
-     let pos  := ctx.fileMap.toPosition spos;
-     pure (env, messages.add { fileName := ctx.fileName, data := toString e, pos := pos }))
+     let pos  := inputCtx.fileMap.toPosition spos;
+     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos }))
 
 def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do
 env ← mkEmptyEnvironment;
 let fileName := fileName.getD "<input>";
-let ctx := Parser.mkParserContextCore env input fileName;
-match Parser.parseHeader env ctx with
+let inputCtx := Parser.mkInputContext input fileName;
+match Parser.parseHeader env inputCtx with
 | (header, parserState, messages) => do
-  pure (headerToImports header, ctx.fileMap.toPosition parserState.pos, messages)
+  pure (headerToImports header, inputCtx.fileMap.toPosition parserState.pos, messages)
 
 @[export lean_parse_imports]
 def parseImportsExport (input : String) (fileName : Option String) : IO (List Import × Position × List Message) := do
diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 2a2a512f87..c6b7064477 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -412,8 +412,7 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr
 
 @[export lean_parse_expr]
 def oldParseExpr (env : Environment) (input : String) (pos : String.Pos) : Except String (Syntax × String.Pos) := do
-let c := Parser.mkParserContextCore env input "<foo>";
-let c := c.toParserContext env;
+let c := Parser.mkParserContext env (Parser.mkInputContext input "<foo>");
 let s := Parser.mkParserState c.input;
 let s := s.setPos pos;
 let s := (Parser.termParser Parser.appPrec : Parser.Parser).fn Parser.appPrec c s;
diff --git a/src/Init/Lean/Parser/Module.lean b/src/Init/Lean/Parser/Module.lean
index f9dda147bd..f958cc8302 100644
--- a/src/Init/Lean/Parser/Module.lean
+++ b/src/Init/Lean/Parser/Module.lean
@@ -34,16 +34,16 @@ private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : St
 let pos := c.fileMap.toPosition pos;
 { fileName := c.fileName, pos := pos, data := errorMsg }
 
-def parseHeader (env : Environment) (c : ParserContextCore) : Syntax × ModuleParserState × MessageLog :=
-let c   := c.toParserContext env;
-let c   := Module.updateTokens c;
-let s   := mkParserState c.input;
-let s   := whitespace c s;
-let s   := Module.header.fn (0:Nat) c s;
+def parseHeader (env : Environment) (inputCtx : InputContext) : Syntax × ModuleParserState × MessageLog :=
+let ctx := mkParserContext env inputCtx;
+let ctx := Module.updateTokens ctx;
+let s   := mkParserState ctx.input;
+let s   := whitespace ctx s;
+let s   := Module.header.fn (0:Nat) ctx s;
 let stx := s.stxStack.back;
 match s.errorMsg with
 | some errorMsg =>
-  let msg := mkErrorMessage c s.pos (toString errorMsg);
+  let msg := mkErrorMessage ctx s.pos (toString errorMsg);
   (stx, { pos := s.pos, recovering := true }, { MessageLog . }.add msg)
 | none =>
   (stx, { pos := s.pos }, {})
@@ -65,12 +65,12 @@ match s.errorMsg with
 | some _ => pos + 1
 | none   => s.pos
 
-partial def parseCommand (env : Environment) (c : ParserContextCore) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog
+partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog
 | s@{ pos := pos, recovering := recovering }, messages =>
-  if c.input.atEnd pos then
+  if inputCtx.input.atEnd pos then
     (mkEOI pos, s, messages)
   else
-    let c  := c.toParserContext env;
+    let c  := mkParserContext env inputCtx;
     let s  := { ParserState . cache := initCacheForInput c.input, pos := pos };
     let s  := whitespace c s;
     let s  := (commandParser : Parser).fn (0:Nat) c s;
@@ -86,9 +86,9 @@ partial def parseCommand (env : Environment) (c : ParserContextCore) : ModulePar
         let messages := messages.add msg;
         parseCommand { pos := consumeInput c s.pos, recovering := true } messages
 
-private partial def testModuleParserAux (env : Environment) (c : ParserContextCore) (displayStx : Bool) : ModuleParserState → MessageLog → IO Bool
+private partial def testModuleParserAux (env : Environment) (inputCtx : InputContext) (displayStx : Bool) : ModuleParserState → MessageLog → IO Bool
 | s, messages =>
-  match parseCommand env c s messages with
+  match parseCommand env inputCtx s messages with
   | (stx, s, messages) =>
     if isEOI stx || isExitCommand stx then do
       messages.forM $ fun msg => IO.println msg;
@@ -100,14 +100,14 @@ private partial def testModuleParserAux (env : Environment) (c : ParserContextCo
 @[export lean_test_module_parser]
 def testModuleParser (env : Environment) (input : String) (fileName := "<input>") (displayStx := false) : IO Bool :=
 timeit (fileName ++ " parser") $ do
-  let ctx                := mkParserContextCore env input fileName;
-  let (stx, s, messages) := parseHeader env ctx;
+  let inputCtx           := mkInputContext input fileName;
+  let (stx, s, messages) := parseHeader env inputCtx;
   when displayStx (IO.println stx);
-  testModuleParserAux env ctx displayStx s messages
+  testModuleParserAux env inputCtx displayStx s messages
 
-partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleParserState → MessageLog → Array Syntax → IO Syntax
+partial def parseFileAux (env : Environment) (inputCtx : InputContext) : ModuleParserState → MessageLog → Array Syntax → IO Syntax
 | state, msgs, stxs =>
-  match parseCommand env ctx state msgs with
+  match parseCommand env inputCtx state msgs with
   | (stx, state, msgs) =>
     if isEOI stx then
       if msgs.isEmpty then
@@ -122,9 +122,9 @@ partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleP
 def parseFile (env : Environment) (fname : String) : IO Syntax := do
 fname ← IO.realPath fname;
 contents ← IO.readTextFile fname;
-let ctx := mkParserContextCore env contents fname;
-let (stx, state, messages) := parseHeader env ctx;
-parseFileAux env ctx state messages #[stx]
+let inputCtx := mkInputContext contents fname;
+let (stx, state, messages) := parseHeader env inputCtx;
+parseFileAux env inputCtx state messages #[stx]
 
 end Parser
 end Lean
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 026e3d0f58..b35b0bd29c 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -73,17 +73,20 @@ abbrev SyntaxNodeKindSet := PersistentHashMap SyntaxNodeKind Unit
 def SyntaxNodeKindSet.insert (s : SyntaxNodeKindSet) (k : SyntaxNodeKind) : SyntaxNodeKindSet :=
 s.insert k ()
 
-structure ParserContextCore :=
+/-
+  Input string and related data. Recall that the `FileMap` is a helper structure for mapping
+  `String.Pos` in the input string to line/column information.  -/
+structure InputContext :=
 (input    : String)
 (fileName : String)
 (fileMap  : FileMap)
-(tokens   : TokenTable)
 
-instance ParserContextCore.inhabited : Inhabited ParserContextCore :=
-⟨{ input := "", fileName := "", fileMap := arbitrary _, tokens := {} }⟩
+instance InputContext.inhabited : Inhabited InputContext :=
+⟨{ input := "", fileName := "", fileMap := arbitrary _ }⟩
 
-structure ParserContext extends ParserContextCore :=
+structure ParserContext extends InputContext :=
 (env      : Environment)
+(tokens   : TokenTable)
 
 structure Error :=
 (unexpected : String := "")
@@ -1423,23 +1426,21 @@ s.2.foldl (fun ks k _ => k::ks) []
 def getTokenTable (env : Environment) : TokenTable :=
 (tokenTableAttribute.ext.getState env).2
 
-def mkParserContextCore (env : Environment) (input : String) (fileName : String) : ParserContextCore :=
+def mkInputContext (input : String) (fileName : String) : InputContext :=
 { input    := input,
   fileName := fileName,
-  fileMap  := input.toFileMap,
-  tokens   := getTokenTable env }
+  fileMap  := input.toFileMap }
 
-@[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 mkParserContext (env : Environment) (ctx : InputContext) : ParserContext :=
+{ toInputContext := ctx,
+  env            := env,
+  tokens         := getTokenTable env }
 
 def mkParserState (input : String) : ParserState :=
 { cache := initCacheForInput input }
 
 def runParser (env : Environment) (tables : ParsingTables) (input : String) (fileName := "<input>") (kind := "<main>") : Except String Syntax :=
-let c := mkParserContext env input fileName;
+let c := mkParserContext env (mkInputContext input fileName);
 let s := mkParserState input;
 let s := whitespace c s;
 let s := prattParser kind tables (0 : Nat) c s;