diff --git a/script/Modulize.lean b/script/Modulize.lean index 9f55f2b7e8..9804d25eee 100644 --- a/script/Modulize.lean +++ b/script/Modulize.lean @@ -29,7 +29,7 @@ def main (args : List String) : IO Unit := do if !msgs.toList.isEmpty then -- skip this file if there are parse errors msgs.forM fun msg => msg.toString >>= IO.println throw <| .userError "parse errors in file" - let `(header| $[module%$moduleTk?]? $imps:import*) := header + let `(header| $[module%$moduleTk?]? $[prelude%$preludeTk?]? $imps:import*) := header | throw <| .userError s!"unexpected header syntax of {path}" if moduleTk?.isSome then continue @@ -57,19 +57,21 @@ def main (args : List String) : IO Unit := do sec := "\n\n" ++ sec if insertPos?.isNone then sec := sec ++ "\n\n" - text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos + let insertPos := text.pos! insertPos + text := text.extract text.startPos insertPos ++ sec ++ text.extract insertPos text.endPos -- prepend each import with `public ` for imp in imps.reverse do let insertPos := imp.raw.getPos?.get! let prfx := if doMeta then "public meta " else "public " - text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos + let insertPos := text.pos! insertPos + text := text.extract text.startPos insertPos ++ prfx ++ text.extract insertPos text.endPos -- insert `module` header - let mut initText := text.extract 0 startPos - if !initText.trim.isEmpty then + let mut initText := text.extract text.startPos (text.pos! startPos) + if !initText.trimAscii.isEmpty then -- If there is a header comment, preserve it and put `module` in the line after - initText := initText.trimRight ++ "\n" - text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos + initText := initText.trimAsciiEnd.toString ++ "\n" + text := initText ++ "module\n\n" ++ text.extract (text.pos! startPos) text.endPos IO.FS.writeFile path text