initialize initializeAckRef : IO.Ref (Option Nat) ← IO.mkRef none
initialize readerFailureRef : IO.Ref (Option (UInt32 × String)) ← IO.mkRef none

private def hexDigit (n : Nat) : Char :=
  if n < 10 then Char.ofNat (48 + n) else Char.ofNat (65 + (n - 10))

private def fileUri (path : String) : String :=
  if path.startsWith "/" then s!"file://{path}" else s!"file:///{path}"

private def pctEncodeByte (b : UInt8) : String :=
  let n := b.toNat
  let hi := n / 16
  let lo := n % 16
  String.singleton '%' ++ String.singleton (hexDigit hi) ++ String.singleton (hexDigit lo)
private def isUriPathSafeByte (b : UInt8) : Bool :=
  let n := b.toNat
  (48 <= n && n <= 57) ||   -- 0-9
  (65 <= n && n <= 90) ||   -- A-Z
  (97 <= n && n <= 122) ||  -- a-z
  n == 45 ||                -- -
  n == 46 ||                -- .
  n == 95 ||                -- _
  n == 126 ||               -- ~
  n == 47                   -- /
private def encodeUriPath (path : String) : String :=
  let bytes := path.toUTF8
  Id.run do
    let mut out := ""
    for b in bytes do
      if isUriPathSafeByte b then
        out := out.push (Char.ofNat b.toNat)
      else
        out := out ++ pctEncodeByte b
    return out

def fileUri (path : String) : String :=
  let absPath :=
    if path.startsWith "/" then
      path
    else
      "/" ++ path
  s!"file://{encodeUriPath absPath}"

def responseId? (j : Lean.Json) : Option Nat := do
  let id ← (j.getObjVal? "id").toOption
  jsonNat? id
def isResponseForRequest (j : Lean.Json) (reqId : Nat) : Bool :=
  responseId? j == some reqId

          initializeAckRef.set (some reqId)

            initializeAckRef.set (some reqId)

private partial def readLoop (h : IO.FS.Handle) : IO Unit := do

private partial def readLoop (pid : UInt32) (h : IO.FS.Handle) : IO Unit := do

    readLoop h
  catch _ =>

    readLoop pid h
  catch e =>
    readerFailureRef.set (some (pid, toString e))

private def clearFailedSessionIfAny : IO Unit := do
  match (← sessionRef.get), (← readerFailureRef.get) with
  | some s, some (pid, _) =>
      if s.child.pid == pid then
        readerFailureRef.set none
        try
          let _ ← terminateSession s
          pure ()
        catch _ =>
          pure ()
        sessionRef.set none
        resetUiState
      else
        pure ()
  | _, _ => pure ()
private def waitForInitializeAck (child : LspChild) (reqId : Nat) (timeoutMs : Nat := 5000) : IO Bool := do
  let tries := (timeoutMs / 10) + 1
  let rec loop : Nat → IO Bool
    | 0 => pure false
    | n + 1 => do
        match (← child.tryWait) with
        | some _ => pure false
        | none =>
            match (← initializeAckRef.get) with
            | some got =>
                initializeAckRef.set none
                if got == reqId then
                  pure true
                else
                  loop n
            | none =>
                IO.sleep 10
                loop n
  loop tries

  let initializeReq := mkRequest session.nextId "initialize" initParams

  let reqId := session.nextId
  let initializeReq := mkRequest reqId "initialize" initParams
  initializeAckRef.set none

  let acked ← waitForInitializeAck session.child reqId
  if !acked then
    throw (IO.userError "LSP initialize handshake timed out")

  pure { session with nextId := session.nextId + 1 }

  pure { session with nextId := reqId + 1 }

  clearFailedSessionIfAny

        readerFailureRef.set none

        let reader ← IO.asTask (readLoop child.stdout)

        let reader ← IO.asTask (readLoop child.pid child.stdout)

        clearFailedSessionIfAny

        readerFailureRef.set none

        readerFailureRef.set none

          readerFailureRef.set none

            readerFailureRef.set none

            readerFailureRef.set none

  clearFailedSessionIfAny

  clearFailedSessionIfAny

import Test.Lsp

  Test.Lsp.test

import ViE
import Test.Utils
namespace Test.Lsp
open Test.Utils
def test : IO Unit := do
  IO.println "Starting LSP Test..."
  let leanBuf := { ViE.initialBuffer with filename := some "Main.lean" }
  let txtBuf := { ViE.initialBuffer with filename := some "notes.txt" }
  assertEqual "isLeanBuffer true for .lean" true (ViE.Lsp.Lean.isLeanBuffer leanBuf)
  assertEqual "isLeanBuffer false for non-.lean" false (ViE.Lsp.Lean.isLeanBuffer txtBuf)
  let uriAbs := ViE.Lsp.Lean.fileUri "/tmp/a b#c%.lean"
  assertEqual "fileUri percent-encodes reserved bytes" "file:///tmp/a%20b%23c%25.lean" uriAbs
  let uriRel := ViE.Lsp.Lean.fileUri "tmp/test.lean"
  assertEqual "fileUri normalizes relative path with leading slash" "file:///tmp/test.lean" uriRel
  let okResp : Lean.Json := Lean.Json.mkObj [("id", (12 : Lean.Json)), ("result", Lean.Json.null)]
  let errResp : Lean.Json := Lean.Json.mkObj [("id", (13 : Lean.Json)), ("error", Lean.Json.mkObj [("code", (1 : Lean.Json))])]
  let notif : Lean.Json := Lean.Json.mkObj [("method", .str "textDocument/publishDiagnostics"), ("params", Lean.Json.mkObj [])]
  assertEqual "responseId? parses result response id" (some 12) (ViE.Lsp.Lean.responseId? okResp)
  assertEqual "responseId? parses error response id" (some 13) (ViE.Lsp.Lean.responseId? errResp)
  assertEqual "responseId? is none for notifications" (none : Option Nat) (ViE.Lsp.Lean.responseId? notif)
  assertEqual "isResponseForRequest true for same id" true (ViE.Lsp.Lean.isResponseForRequest okResp 12)
  assertEqual "isResponseForRequest false for different id" false (ViE.Lsp.Lean.isResponseForRequest okResp 99)
  let s0 := ViE.initialState
  let sStatus ← ViE.Lsp.Lean.cmdLsp ["status"] s0
  assertEqual "lsp status reports stopped when no session" "LSP: stopped" sStatus.message
  let sStop ← ViE.Lsp.Lean.cmdLsp ["stop"] s0
  assertEqual "lsp stop reports not running when no session" "LSP is not running" sStop.message
  IO.println "LSP Test passed!"
end Test.Lsp