From 3d1ff59f113acfdf106692c82d7f220759342f59 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Nov 2022 10:36:40 +0100
Subject: [PATCH] fix: parseImports': respect `prelude`

---
 src/Lean/Elab/ParseImportsFast.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/ParseImportsFast.lean b/src/Lean/Elab/ParseImportsFast.lean
index 8ba15b18d5..bcb5d83427 100644
--- a/src/Lean/Elab/ParseImportsFast.lean
+++ b/src/Lean/Elab/ParseImportsFast.lean
@@ -118,9 +118,6 @@ partial def whitespace : Parser := fun input s =>
 @[inline] partial def keyword (k : String) : Parser :=
   keywordCore k (fun _ s => s.mkError s!"`{k}` expected") (fun _ s => s)
 
-@[inline] partial def keywordOpt (k : String) : Parser :=
-  keywordCore k (fun _ s => s) (fun _ s => s)
-
 @[inline] def isIdCont : String → State → Bool := fun input s =>
   let i := s.pos
   let curr := input.get i
@@ -186,8 +183,11 @@ partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
   | none => many p input s
   | some _ => { pos, error? := none, imports := s.imports.shrink size }
 
+@[inline] partial def preludeOpt (k : String) : Parser :=
+  keywordCore k (fun _ s => s.pushModule `Init false) (fun _ s => s)
+
 def main : Parser :=
-  keywordOpt "prelude" >>
+  preludeOpt "prelude" >>
   many (keyword "import" >> keywordCore "runtime" (moduleIdent false) (moduleIdent true))
 
 end ParseImports