chore: simplify and extend Modulize.lean (#10692)

Take explicit list of files instead of asking Lake, take `--meta` flag
instead of guessing based on module name.

script/Modulize.lean

@@ -1,53 +1,30 @@
 import Lake.CLI.Main
 
 /-!
-A simple script that inserts `module` and `@[expose] public section` into un-modulized files and
+
+Usage: `lean --run script/Modulize.lean [--meta] file1.lean file2.lean ...`
+
+A simple script that inserts `module` and `public section` into un-modulized files and
 bumps their imports to `public`.
+
+When `--meta` is passed, `public meta section` and `public meta import` is used instead.
 -/
 
 open Lean Parser.Module
 
 def main (args : List String) : IO Unit := do
-  initSearchPath (← findSysroot)
-  -- the list of root modules
-  let mut mods := args.toArray.map (·.toName)
-
-  if mods.isEmpty then
-    -- Determine default module(s) to run modulize on
-    mods ← try
-      let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
-      let config ← Lake.MonadError.runEIO <| Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
-      let some workspace ← Lake.loadWorkspace config |>.toBaseIO
-        | throw <| IO.userError "failed to load Lake workspace"
-      let defaultTargetModules := workspace.root.defaultTargets.flatMap fun target =>
-        if let some lib := workspace.root.findLeanLib? target then
-          lib.roots
-        else if let some exe := workspace.root.findLeanExe? target then
-          #[exe.config.root]
-        else
-          #[]
-      pure defaultTargetModules
-    catch _ =>
-      pure #[]
-
-  -- Only submodules of `pkg` will be edited or have info reported on them
-  let pkg := mods[0]!.components.head!
-
-  -- Load all the modules
-  let imps := mods.map ({ module := · })
-  let env ← importModules imps {}
-
-  let srcSearchPath ← getSrcSearchPath
-
-  for mod in env.header.moduleNames do
-    if !pkg.isPrefixOf mod then
-      continue
+  let mut args := args
+  let mut doMeta := false
+  while !args.isEmpty && args[0]!.startsWith "-" do
+    match args[0]! with
+    | "--meta" => doMeta := true
+    | arg => throw <| .userError s!"unknown flag '{arg}'"
+    args := args.tail
 
+  for path in args do
     -- Parse the input file
-    let some path ← srcSearchPath.findModuleWithExt "lean" mod
-      | throw <| .userError "error: failed to find source file for {mod}"
     let mut text ← IO.FS.readFile path
-    let inputCtx := Parser.mkInputContext text path.toString
+    let inputCtx := Parser.mkInputContext text path
     let (header, parserState, msgs) ← Parser.parseHeader inputCtx
     if !msgs.toList.isEmpty then -- skip this file if there are parse errors
       msgs.forM fun msg => msg.toString >>= IO.println
@@ -57,15 +34,13 @@ def main (args : List String) : IO Unit := do
     if moduleTk?.isSome then
       continue
 
-    let looksMeta := mod.components.any (· ∈ [`Tactic, `Linter])
-
     -- initial whitespace if empty header
     let startPos := header.raw.getPos? |>.getD parserState.pos
 
     -- insert section if any trailing text
     if header.raw.getTrailingTailPos?.all (· < text.endPos) then
       let insertPos := header.raw.getTailPos? |>.getD startPos  -- empty header
-      let mut sec := if looksMeta then
+      let mut sec := if doMeta then
         "public meta section"
       else
         "@[expose] public section"
@@ -78,7 +53,7 @@ def main (args : List String) : IO Unit := do
     -- prepend each import with `public `
     for imp in imps.reverse do
       let insertPos := imp.raw.getPos?.get!
-      let prfx := if looksMeta then "public meta " else "public "
+      let prfx := if doMeta then "public meta " else "public "
       text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.endPos
 
     -- insert `module` header