CUJ744WGUGBQHTO7BN7II2KB7R4N3IBXO62OG5UJAEZU2LFHHHUAC private def waitForExit (child : LspChild) (tries : Nat := 50) (sleepMs : Nat := 20) : IO Bool := dolet rec loop : Nat → IO Bool| 0 => domatch (← child.tryWait) with| some _ => pure true| none => pure false| n + 1 => domatch (← child.tryWait) with| some _ => pure true| none =>IO.sleep sleepMs.toUInt32loop nloop triesprivate def gracefulStopTries : Nat := 8private def postKillStopTries : Nat := 12private def finalStopTries : Nat := 6private def stopPollMs : Nat := 10
private def terminateSession (s : Session) : IO Bool := dolet killDescendants (sig : String) : IO Unit := dotrylet _ ← IO.Process.output {cmd := "pkill"args := #["-" ++ sig, "-P", toString s.child.pid]stdin := .nullstderr := .null}pure ()catch _ =>pure ()let shutdownReq := mkRequest s.nextId "shutdown" (Lean.Json.mkObj [])let exitNotif := mkNotification "exit" (Lean.Json.mkObj [])trysend s.child.stdin shutdownReqsend s.child.stdin exitNotifcatch _ =>pure ()let stoppedGracefully ← waitForExit s.child gracefulStopTries stopPollMsif stoppedGracefully thenpure trueelsekillDescendants "TERM"trys.child.killcatch _ =>pure ()let stoppedAfterKill ← waitForExit s.child postKillStopTries stopPollMsif stoppedAfterKill thenpure trueelsekillDescendants "KILL"waitForExit s.child finalStopTries stopPollMs
let sInfoOnly := ViE.Window.closeActiveWindow sLean'let sInfoOnly' ← ViE.Lsp.Lean.syncInfoViewWindow sInfoOnlylet wsInfoOnly := sInfoOnly'.getCurrentWorkspaceassertEqual "InfoView-only fallback requests quit" true sInfoOnly'.shouldQuitassertEqual "InfoView-only fallback removes InfoView buffer" true ((wsInfoOnly.buffers.find? (fun b => b.filename == some ViE.Lsp.Lean.infoViewVirtualPath)).isNone)