fix: use correct positions for header errors (#3728)

This lead to incorrect diagnostic spans in the editor and resulted in
header errors that did not show up under "Messages" everywhere in the
file because the `fullRange?` property was missing.

Also changes the "Import out of date" warning diagnostic severity to
"Hint" so that it doesn't show up in the "Problems" view.

src/Lean/Language/Basic.lean

@@ -194,7 +194,7 @@ def Snapshot.Diagnostics.ofMessageLog (msgLog : Lean.MessageLog) :
 def diagnosticsOfHeaderError (msg : String) : ProcessingM Snapshot.Diagnostics := do
   let msgLog := MessageLog.empty.add {
     fileName := "<input>"
-    pos := ⟨0, 0⟩
+    pos := ⟨1, 0⟩
     endPos := (← read).fileMap.toPosition (← read).fileMap.source.endPos
     data := msg
   }

src/Lean/Server/FileWorker.lean

@@ -275,7 +275,7 @@ def setupImports (meta : DocumentMeta) (chanOut : Channel JsonRpc.Message)
   let imports := Elab.headerToImports stx
   let fileSetupResult ← setupFile meta imports fun stderrLine => do
     let progressDiagnostic := {
-      range      := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩
+      range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
       -- make progress visible anywhere in the file
       fullRange? := some ⟨⟨0, 0⟩, meta.text.utf8PosToLspPos meta.text.source.endPos⟩
       severity?  := DiagnosticSeverity.information
@@ -440,16 +440,18 @@ section NotificationHandling
   def handleStaleDependency (p : LeanStaleDependencyParams) : WorkerM Unit := do
     let ctx ← read
     let s ← get
+    let text := s.doc.meta.text
     let _ ← IO.mapTask (t :=  s.srcSearchPathTask) fun srcSearchPath => do
       let some staleDependencyName ← moduleFromDocumentUri srcSearchPath p.staleDependency
         | return
       let diagnostic := {
-        range     := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩
-        severity? := DiagnosticSeverity.warning
-        code?     := some <| .string "LanguageServer_ImportOutOfDate"
-        message   := .text s!"Import '{staleDependencyName}' is out of date; \
+        range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
+        fullRange? := some ⟨⟨0, 0⟩, text.utf8PosToLspPos text.source.endPos⟩
+        severity?  := DiagnosticSeverity.hint
+        code?      := some <| .string "LanguageServer_ImportOutOfDate"
+        message    := .text s!"Import '{staleDependencyName}' is out of date; \
           use the \"Restart File\" command in your editor."
-        data?     := some staleDependencyName.toString
+        data?      := some staleDependencyName.toString
     }
       ctx.stickyDiagnosticsRef.modify fun stickyDiagnostics => stickyDiagnostics.insert diagnostic
       publishDiagnostics ctx s.doc.toEditableDocumentCore
@@ -623,7 +625,7 @@ end MessageHandling
 
 section MainLoop
   variable (hIn : FS.Stream) in
-  partial def mainLoop : WorkerM UInt32 := do
+  partial def mainLoop : WorkerM Unit := do
     let mut st ← get
     let msg ← hIn.readLspMessage
     let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
@@ -650,7 +652,7 @@ section MainLoop
       handleRequest id method (toJson params)
       mainLoop
     | Message.notification "exit" none =>
-      return 0
+      return
     | Message.notification method (some params) =>
       handleNotification method (toJson params)
       mainLoop
@@ -685,21 +687,30 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, param.dependencyBuildMode?.getD .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
-  try
-    let (ctx, st) ← initializeWorker meta o e initParams.param opts
-    let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) do
-      let refreshTask ← runRefreshTask
-      let exitCode ← mainLoop i
-      IO.cancel refreshTask
-      pure exitCode
-    return (0 : UInt32)
+  let (ctx, st) ← try
+    initializeWorker meta o e initParams.param opts
   catch err =>
+    writeError meta err
+    return (1 : UInt32)
+  let exitCode ← StateRefT'.run' (s := st) <| ReaderT.run (r := ctx) do
+    try
+      let refreshTask ← runRefreshTask
+      mainLoop i
+      IO.cancel refreshTask
+      return 0
+    catch err =>
+      let st ← get
+      writeError st.doc.meta err
+      return 1
+  return exitCode
+where
+  writeError (meta : DocumentMeta) (err : Error) : IO Unit := do
     IO.eprintln err
     e.writeLspMessage <| mkPublishDiagnosticsNotification meta #[{
-      range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩
+      range := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩,
+      fullRange? := some ⟨⟨0, 0⟩, meta.text.utf8PosToLspPos meta.text.source.endPos⟩
       severity? := DiagnosticSeverity.error
       message := err.toString }]
-    return (1 : UInt32)
 
 @[export lean_server_worker_main]
 def workerMain (opts : Options) : IO UInt32 := do