feat: change error flag to progress kind in LeanFileProgressProcessingInfo

src/Lean/Data/Lsp/Extra.lean

@@ -35,9 +35,23 @@ instance : FromJson WaitForDiagnostics :=
 instance : ToJson WaitForDiagnostics :=
   ⟨fun o => mkObj []⟩
 
+inductive LeanFileProgressKind
+  | processing | fatalError
+  deriving Inhabited, BEq
+
+instance : FromJson LeanFileProgressKind := ⟨fun j =>
+  match j.getNat? with
+  | Except.ok 1 => LeanFileProgressKind.processing
+  | Except.ok 2 => LeanFileProgressKind.fatalError
+  | _           => throw s!"unknown LeanFileProgressKind '{j}'"⟩
+
+instance : ToJson LeanFileProgressKind := ⟨fun
+  | LeanFileProgressKind.processing => 1
+  | LeanFileProgressKind.fatalError => 2⟩
+
 structure LeanFileProgressProcessingInfo where
   range : Range
-  error : Bool := false
+  kind : LeanFileProgressKind := LeanFileProgressKind.processing
   deriving FromJson, ToJson
 
 /-- `$/lean/fileProgress` client<-server notification.

src/Lean/Server/FileWorker.lean

@@ -99,7 +99,7 @@ section Elab
     if initial && initSnap.msgLog.hasErrors then
       -- treat header processing errors as fatal so users aren't swamped with followup errors
       let hOut := (←read).hOut
-      publishProgressAtPos m initSnap.beginPos hOut (error := true)
+      publishProgressAtPos m initSnap.beginPos hOut (kind := LeanFileProgressKind.fatalError)
       AsyncList.nil
     else
       AsyncList.unfoldAsync (nextCmdSnap m . cancelTk (← read)) initSnap

src/Lean/Server/Utils.lean

@@ -137,8 +137,8 @@ def publishProgress (m : DocumentMeta) (processing : Array LeanFileProgressProce
     }
   }
 
-def publishProgressAtPos (m : DocumentMeta) (pos : String.Pos) (hOut : FS.Stream) (error : Bool := false) : IO Unit :=
-  publishProgress m #[{ range := ⟨m.text.utf8PosToLspPos pos, m.text.utf8PosToLspPos m.text.source.bsize⟩, error := error }] hOut
+def publishProgressAtPos (m : DocumentMeta) (pos : String.Pos) (hOut : FS.Stream) (kind : LeanFileProgressKind := LeanFileProgressKind.processing) : IO Unit :=
+  publishProgress m #[{ range := ⟨m.text.utf8PosToLspPos pos, m.text.utf8PosToLspPos m.text.source.bsize⟩, kind := kind }] hOut
 
 def publishProgressDone (m : DocumentMeta) (hOut : FS.Stream) : IO Unit :=
   publishProgress m #[] hOut