refactor: remove redundant calls to DocumentMeta.mod (#12085)

src/Lean/Server/FileWorker.lean

@@ -410,29 +410,32 @@ def setupImports
       message    := stderrLine
     }
     chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[progressDiagnostic]
-  let isSetupError := fileSetupResult.kind matches .importsOutOfDate
-    || fileSetupResult.kind matches .error ..
+  let isSetupError := fileSetupResult matches .importsOutOfDate
+    || fileSetupResult matches .error ..
   chanOut.sync.send <| .ofMsg <| mkIleanHeaderSetupInfoNotification doc isSetupError
   -- clear progress notifications in the end
   chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[]
-  match fileSetupResult.kind with
-  | .importsOutOfDate =>
-    return .error {
-      diagnostics := (← Language.diagnosticsOfHeaderError
-        "Imports are out of date and must be rebuilt; \
-          use the \"Restart File\" command in your editor.")
-      result? := none
-      metaSnap := default
-    }
-  | .error msg =>
-    return .error {
-      diagnostics := (← diagnosticsOfHeaderError msg)
-      result? := none
-      metaSnap := default
-    }
-  | _ => pure ()
-
-  let setup := fileSetupResult.setup
+  let setup ← do
+    match fileSetupResult with
+    | .importsOutOfDate =>
+      return .error {
+        diagnostics := (← Language.diagnosticsOfHeaderError
+          "Imports are out of date and must be rebuilt; \
+            use the \"Restart File\" command in your editor.")
+        result? := none
+        metaSnap := default
+        : Language.Lean.HeaderProcessedSnapshot
+      }
+    | .error msg =>
+      return .error {
+        diagnostics := (← diagnosticsOfHeaderError msg)
+        result? := none
+        metaSnap := default
+      }
+    | .noLakefile =>
+      pure { name := doc.mod, isModule := header.isModule }
+    | .success setup =>
+      pure setup
 
   -- override cmdline options with file options
   let opts := cmdlineOpts.mergeBy (fun _ _ fileOpt => fileOpt) setup.options.toOptions

src/Lean/Server/FileWorker/SetupFile.lean

@@ -56,10 +56,10 @@ partial def runLakeSetupFile
   let exitCode ← lakeProc.wait
   return ⟨spawnArgs, exitCode, stdout, stderr⟩
 
-/-- Categorizes possible outcomes of running `lake setup-file`. -/
-inductive FileSetupResultKind where
+/-- Result of running `lake setup-file`. -/
+inductive FileSetupResult where
   /-- File configuration loaded and dependencies updated successfully. -/
-  | success
+  | success (setup : ModuleSetup)
   /-- No Lake project found, no setup was done. -/
   | noLakefile
   /-- Imports must be rebuilt but `--no-build` was specified. -/
@@ -67,43 +67,16 @@ inductive FileSetupResultKind where
   /-- Other error during Lake invocation. -/
   | error (msg : String)
 
-/-- Result of running `lake setup-file`. -/
-structure FileSetupResult where
-  /-- Kind of outcome. -/
-  kind        : FileSetupResultKind
-  /-- Configuration from a successful setup, or else the default. -/
-  setup       : ModuleSetup
-
-def FileSetupResult.ofSuccess (setup : ModuleSetup) : IO FileSetupResult := do return {
-  kind          := FileSetupResultKind.success
-  setup
-}
-
-def FileSetupResult.ofNoLakefile (m : DocumentMeta) (header : ModuleHeader) : IO FileSetupResult := do return {
-  kind          := FileSetupResultKind.noLakefile
-  setup         := {name := m.mod, isModule := header.isModule}
-}
-
-def FileSetupResult.ofImportsOutOfDate (m : DocumentMeta) (header : ModuleHeader) : IO FileSetupResult := do return {
-  kind          := FileSetupResultKind.importsOutOfDate
-  setup         := {name := m.mod, isModule := header.isModule}
-}
-
-def FileSetupResult.ofError (m : DocumentMeta) (header : ModuleHeader) (msg : String) : IO FileSetupResult := do return {
-  kind          := FileSetupResultKind.error msg
-  setup         := {name := m.mod, isModule := header.isModule}
-}
-
 /-- Uses `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`.
 Compilation progress is reported to `handleStderr`. Returns the search path for
 source files and the options for the file. -/
 partial def setupFile (m : DocumentMeta) (header : ModuleHeader) (handleStderr : String → IO Unit) : IO FileSetupResult := do
   let some filePath := System.Uri.fileUriToPath? m.uri
-    | return ← FileSetupResult.ofNoLakefile m header -- untitled files have no lakefile
+    | return FileSetupResult.noLakefile -- untitled files have no lakefile
 
   let lakePath ← determineLakePath
   if !(← System.FilePath.pathExists lakePath) then
-    return ← FileSetupResult.ofNoLakefile m header
+    return FileSetupResult.noLakefile
 
   let result ← runLakeSetupFile m lakePath filePath header handleStderr
 
@@ -112,12 +85,12 @@ partial def setupFile (m : DocumentMeta) (header : ModuleHeader) (handleStderr :
   match result.exitCode with
   | 0 =>
     let Except.ok (setup : ModuleSetup) := Json.parse result.stdout >>= fromJson?
-      | return ← FileSetupResult.ofError m header s!"Invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}"
+      | return FileSetupResult.error s!"Invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}"
     setup.dynlibs.forM loadDynlib
-    FileSetupResult.ofSuccess setup
+    return FileSetupResult.success setup
   | 2 => -- exit code for lake reporting that there is no lakefile
-    FileSetupResult.ofNoLakefile m header
+    return FileSetupResult.noLakefile
   | 3 => -- exit code for `--no-build`
-    FileSetupResult.ofImportsOutOfDate m header
+    return FileSetupResult.importsOutOfDate
   | _ =>
-    FileSetupResult.ofError m header s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}"
+    return FileSetupResult.error s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}"