max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: modulize: work around unknown initial command (#12080)

Browse source
This commit is contained in:
Sebastian Ullrich 2026-01-21 21:25:13 +01:00 • committed by GitHub
parent 34d8eeb3be
commit 16873fb123
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
script/Modulize.lean
View file

@ -38,11 +38,11 @@ def main (args : List String) : IO Unit := do
let startPos := header.raw.getPos? |>.getD parserState.pos let startPos := header.raw.getPos? |>.getD parserState.pos
let dummyEnv ← mkEmptyEnvironment let dummyEnv ← mkEmptyEnvironment
let (initCmd, parserState', _) := let (initCmd, parserState', msgs') :=
Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs
-- insert section if any trailing command -- insert section if any trailing command (or error, which could be from an unknown command)
if !initCmd.isOfKind ``Parser.Command.eoi then if !initCmd.isOfKind ``Parser.Command.eoi || msgs'.hasErrors then
let insertPos? := let insertPos? :=
-- put below initial module docstring if any -- put below initial module docstring if any
guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|> guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|>