buildType = "release"

  loaded : Bool := true

    s!"FileBuffer(id={buf.id}, file={buf.filename}, dirty={buf.dirty}, lines={buf.table.lineCount})"

    s!"FileBuffer(id={buf.id}, file={buf.filename}, dirty={buf.dirty}, loaded={buf.loaded}, lines={buf.table.lineCount})"

    return { bits := ViE.SearchBloom.empty.bits, prefixBytes := prefixBytes, suffixBytes := suffixBytes }

    return { bits := ViE.SearchBloom.empty.bits, prefixBytes := prefixBytes, suffixBytes := suffixBytes, hasBits := false }

    return { bits := bits, prefixBytes := prefixBytes, suffixBytes := carry }

    return { bits := bits, prefixBytes := prefixBytes, suffixBytes := carry, hasBits := true }

  if bloomIsEmpty left.bits || bloomIsEmpty right.bits then
    { bits := ViE.SearchBloom.empty.bits, prefixBytes := pref, suffixBytes := suf }

  if !left.hasBits || !right.hasBits then
    { bits := ViE.SearchBloom.empty.bits, prefixBytes := pref, suffixBytes := suf, hasBits := false }

    { bits := bits, prefixBytes := pref, suffixBytes := suf }

    { bits := bits, prefixBytes := pref, suffixBytes := suf, hasBits := true }

def bloomMayContain (bloom : ByteArray) (hashes : Array (Nat × Nat)) : Bool :=

def bloomMayContain (searchMeta : ViE.SearchBloom) (hashes : Array (Nat × Nat)) : Bool :=

  else if bloomIsEmpty bloom then

  else if !searchMeta.hasBits then

    hashes.all (fun (h1, h2) => bloomGetBit bloom h1 && bloomGetBit bloom h2)

    hashes.all (fun (h1, h2) => bloomGetBit searchMeta.bits h1 && bloomGetBit searchMeta.bits h2)

  if pieces.isEmpty then ViE.PieceTree.empty
  else if pieces.size <= ViE.NodeCapacity then
    mkLeaf pieces pt

  if pieces.isEmpty then
    ViE.PieceTree.empty

    let mid := pieces.size / 2
    let left := fromPieces (pieces.extract 0 mid) pt
    let right := fromPieces (pieces.extract mid pieces.size) pt
    mkInternal #[left, right]
  termination_by pieces.size
  decreasing_by
    · simp_wf
      have hgt : ViE.NodeCapacity < pieces.size := Nat.lt_of_not_ge (by assumption)
      have hsize : 0 < pieces.size := Nat.lt_trans (by decide : 0 < ViE.NodeCapacity) hgt
      have hdiv : pieces.size / 2 < pieces.size := Nat.div_lt_self hsize (by decide : 1 < 2)
      exact Nat.lt_of_le_of_lt (Nat.min_le_left _ _) hdiv
    · simp_wf
      have hgt : ViE.NodeCapacity < pieces.size := Nat.lt_of_not_ge (by assumption)
      have hsize : 0 < pieces.size := Nat.lt_trans (by decide : 0 < ViE.NodeCapacity) hgt
      have hge2 : 2 ≤ pieces.size := Nat.le_trans (by decide : 2 ≤ ViE.NodeCapacity) (Nat.le_of_lt hgt)
      have hhalf : 0 < pieces.size / 2 := Nat.div_pos hge2 (by decide : 0 < 2)
      exact Nat.sub_lt hsize hhalf

    Id.run do
      let mut leaves : Array ViE.PieceTree := #[]
      let mut i := 0
      while i < pieces.size do
        let j := min (i + ViE.NodeCapacity) pieces.size
        leaves := leaves.push (mkLeaf (pieces.extract i j) pt)
        i := j
      let mut level := leaves
      while level.size > 1 do
        let mut parents : Array ViE.PieceTree := #[]
        let mut k := 0
        while k < level.size do
          let j := min (k + ViE.NodeCapacity) level.size
          parents := parents.push (mkInternal (level.extract k j))
          k := j
        level := parents
      return level[0]!

    let chunks := Id.run do

    Id.run do
      let mut out : ByteArray := ByteArray.mk (Array.mkEmpty len)

      let mut out : Array ByteArray := #[]

                        let slice := buf.extract (p.start + startInPiece) (p.start + startInPiece + readLen)
                        out := out.push slice

                        let mut r := 0
                        while r < readLen do
                          out := out.push (buf[p.start + startInPiece + r]!)
                          r := r + 1

    chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])

                      if !crossesBoundary && !bloomMayContain m.bits hashes then

                      if !crossesBoundary && !bloomMayContain m hashes then

                    if !bloomMayContain m.bits hashes then

                    if !bloomMayContain m hashes then

                      if !crossesBoundary && !bloomMayContain m.bits hashes then

                      if !crossesBoundary && !bloomMayContain m hashes then

                    if !bloomMayContain m.bits hashes then

                    if !bloomMayContain m hashes then

  hasBits : Bool := false

  suffixBytes := #[]

  suffixBytes := #[],
  hasBits := false

    s!"SearchBloom(bits={sb.bits.size}, prefix={sb.prefixBytes}, suffix={sb.suffixBytes})"

    s!"SearchBloom(bits={sb.bits.size}, hasBits={sb.hasBits}, prefix={sb.prefixBytes}, suffix={sb.suffixBytes})"

import ViE.Buffer.Manager

  return enforceScroll newState

  let loadedState ← ViE.Buffer.ensureActiveBufferLoaded newState
  return enforceScroll loadedState

def ensureBufferLoadedById (state : EditorState) (bufId : Nat) : IO EditorState := do
  let ws := state.getCurrentWorkspace
  match ws.buffers.find? (fun b => b.id == bufId) with
  | none => pure state
  | some buf =>
      if buf.loaded || buf.filename.isNone then
        pure state
      else
        let fname := buf.filename.getD ""
        let loadedBuf ← ViE.loadBufferByteArrayWithConfig fname state.config
        let merged := {
          loadedBuf with
            id := buf.id
            dirty := buf.dirty
            loaded := true
            table := { loadedBuf.table with undoLimit := state.config.historyLimit }
        }
        let s' := state.updateCurrentWorkspace fun ws =>
          { ws with buffers := ws.buffers.map (fun b => if b.id == buf.id then merged else b) }
        pure { s' with message := s!"Loaded \"{fname}\"" }
def ensureActiveBufferLoaded (state : EditorState) : IO EditorState := do
  let ws := state.getCurrentWorkspace
  match ws.layout.findView ws.activeWindowId with
  | none => pure state
  | some v => ensureBufferLoadedById state v.bufferId

    -- Switch to existing buffer

    -- Switch to existing buffer; load if it is a lazy placeholder.

    return { s' with message := s!"Switched to \"{filename}\"" }

    let s'' ← ensureBufferLoadedById s' bid
    return { s'' with message := s!"Switched to \"{filename}\"" }

  loaded := true

    loaded := true

  let buildLeafBits := settings.searchBloomBuildLeafBits
  let placeholderFor (id : Nat) (fname : String) : FileBuffer := {
    id := id
    filename := some fname
    dirty := false
    loaded := false
    table := PieceTable.fromString "" buildLeafBits
    missingEol := false
    cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }
  }
  let filesArr := files.toArray
  let safeActiveIdx := if activeIdx < filesArr.size then activeIdx else 0

  let mut nextId := 0
  for fname in files do
    let buf ← loadBufferByteArrayWithConfig fname settings
    loaded := loaded.push {
      buf with
        id := nextId
        table := { buf.table with undoLimit := settings.historyLimit }
    }
    nextId := nextId + 1

  for i in [0:filesArr.size] do
    let fname := filesArr[i]!
    if i == safeActiveIdx then
      let buf ← loadBufferByteArrayWithConfig fname settings
      loaded := loaded.push {
        buf with
          id := i
          loaded := true
          table := { buf.table with undoLimit := settings.historyLimit }
      }
    else
      loaded := loaded.push (placeholderFor i fname)

  let activeIdx := if activeIdx < loaded.size then activeIdx else 0
  let activeBuf := loaded[activeIdx]!
  let (row, col) := List.getD cursors activeIdx (0, 0)

  let activeBuf := loaded[safeActiveIdx]!
  let (row, col) := List.getD cursors safeActiveIdx (0, 0)

import ViE.Buffer.Manager

      assertEqual "Restored inactive buffer is lazy" false b1.loaded
      assertEqual "Restored active buffer is loaded" true b2.loaded

  let s0 := ({ ViE.initialState with config := ViE.defaultConfig }).updateCurrentWorkspace (fun _ => ws)
  let s1 := s0.updateCurrentWorkspace fun ws =>
    { ws with layout := ws.layout.updateView ws.activeWindowId (fun v => { v with bufferId := 0 }) }
  let s2 ← ViE.Buffer.ensureActiveBufferLoaded s1
  let activeLoaded := s2.getActiveBuffer
  assertEqual "Lazy buffer loads on activation" true activeLoaded.loaded
  assertEqual "Lazy loaded buffer keeps file path" (some f1) activeLoaded.filename