4kusto/vie - Change BVKFLEK2IK7AOIXLU3KGN7XNWP7KSJLGOPJKJIR7MU4LGN4J5EGQC

Update ViE for Bliku clustered floating UI and direct syntax API

Created by 4kusto on March 6, 2026

BVKFLEK2IK7AOIXLU3KGN7XNWP7KSJLGOPJKJIR7MU4LGN4J5EGQC

Dependencies

In channels

main

Change contents

Replacement in lake-manifest.json at line 8 [5.273]

B:BD[4.111] → [4.111:165]

   "rev": "2836947f0090b29b45b4f012db0a274fb2ac8aee",

[4.111]

[4.165]

   "rev": "12016a98c362360422afaaed6c63127fcc30c102",

File deletion: Syntax.lean
BF:BFD[6.1802] → [7.2867:2902]
BF:BFD[7.2902] → [7.2903:2903]
∅:D[8.109] → [7.2942:2967]
∅:D[4.347] → [7.2942:2967]
B:BD[7.2942] → [7.2942:2967]
B:BD[7.8802] → [7.8802:8803]
∅:D[8.190] → [7.9348:9367]
∅:D[4.403] → [7.9348:9367]
B:BD[7.9348] → [7.9348:9367]
B:BD[7.8803] → [4.348:403]
B:BD[7.2903] → [8.26:109]
B:BD[8.109] → [4.323:347]
```
namespace ViE.UI.Syntax
end ViE.UI.Syntax
abbrev highlightLine := Bliku.Tui.Syntax.highlightLine
import ViE.UI.Syntax.Types
import ViE.UI.Syntax.Lean
import ViE.UI.Syntax.Markdown
import Bliku.Tui.Syntax
```
Deletion in ViE/UI/Window.lean at line 3 [6.1840]
B:BD[6.1887] → [7.739:760]
```
import ViE.UI.Syntax
```
Insertion in ViE/UI/Window.lean at line 4 [6.1840]
[6.1907]
[6.1907]
```
import Bliku.Tui.Syntax
```

Replacement in ViE/UI/Window.lean at line 91 [6.1840]

B:BD[6.6268] → [7.761:835]

      let syntaxSpans := ViE.UI.Syntax.highlightLine buf.filename lineStr

[6.6268]

      let syntaxSpans := Bliku.Tui.Syntax.highlightLine buf.filename lineStr

Replacement in ViE/UI/Window.lean at line 129 [6.1840]

B:BD[7.1257] → [7.1257:1333]

              ViE.UI.Syntax.styleForByteRange syntaxSpans byteStart byteEnd

[7.1257]

[7.1333]

              (Bliku.Tui.Syntax.faceForByteRange Bliku.Tui.Syntax.defaultPalette syntaxSpans byteStart byteEnd).map
                (fun face => face.toAnsi)

Replacement in ViE/UI/Window.lean at line 205 [6.1840]

B:BD[7.1784] → [7.1784:1852]

    let syntaxSpans := ViE.UI.Syntax.highlightLine buf.filename raw

[7.1784]

[9.6913]

    let syntaxSpans := Bliku.Tui.Syntax.highlightLine buf.filename raw

Replacement in ViE/UI/Window.lean at line 227 [6.1840]

B:BD[7.2355] → [7.2355:2433]

                ViE.UI.Syntax.styleForByteRange syntaxSpans byteStart byteEnd

[7.2355]

[7.2433]

                (Bliku.Tui.Syntax.faceForByteRange Bliku.Tui.Syntax.defaultPalette syntaxSpans byteStart byteEnd).map
                  (fun face => face.toAnsi)

File deletion: Types.lean

BF:BFD[8.209] → [8.211:245]

BF:BFD[8.245] → [8.246:246]

∅:D[4.434] → [8.285:311]

B:BD[8.285] → [8.285:311]

∅:D[4.517] → [8.400:401]

B:BD[8.400] → [8.400:401]

∅:D[4.758] → [8.505:506]

B:BD[8.505] → [8.505:506]

∅:D[4.1025] → [8.809:810]

B:BD[8.809] → [8.809:810]

∅:D[4.1146] → [8.1733:1752]

B:BD[8.1733] → [8.1733:1752]

B:BD[8.810] → [4.1026:1146]

B:BD[8.506] → [4.759:1025]

B:BD[8.401] → [4.518:758]

B:BD[8.311] → [4.435:517]

B:BD[8.246] → [4.404:434]


namespace ViE.UI.Syntax
end ViE.UI.Syntax
abbrev detectLanguage := Bliku.Tui.Syntax.detectLanguage
abbrev styleForByteRange := Bliku.Tui.Syntax.styleForByteRange
abbrev markdownHeadingStyle := Bliku.Tui.Syntax.markdownHeadingStyle
abbrev markdownCodeStyle := Bliku.Tui.Syntax.markdownCodeStyle
abbrev markdownLinkStyle := Bliku.Tui.Syntax.markdownLinkStyle
abbrev markdownEmphasisStyle := Bliku.Tui.Syntax.markdownEmphasisStyle
abbrev leanKeywordStyle := Bliku.Tui.Syntax.leanKeywordStyle
abbrev leanCommentStyle := Bliku.Tui.Syntax.leanCommentStyle
abbrev leanStringStyle := Bliku.Tui.Syntax.leanStringStyle
abbrev leanNumberStyle := Bliku.Tui.Syntax.leanNumberStyle
abbrev Language := Bliku.Tui.Syntax.Language
abbrev Span := Bliku.Tui.Syntax.Span
import Bliku.Tui.Syntax.Types

File deletion: Markdown.lean
BF:BFD[8.209] → [8.1753:1790]
BF:BFD[8.1790] → [8.1791:1791]
B:BD[8.1791] → [8.1792:1819]
∅:D[4.1180] → [8.1819:1845]
B:BD[8.1819] → [8.1819:1845]
∅:D[4.1252] → [8.3924:3943]
B:BD[8.3924] → [8.3924:3943]
B:BD[8.1845] → [4.1181:1252]
B:BD[8.1819] → [4.1147:1180]
```
import ViE.UI.Syntax.Types
namespace ViE.UI.Syntax
end ViE.UI.Syntax
abbrev highlightMarkdownLine := Bliku.Tui.Syntax.highlightMarkdownLine
import Bliku.Tui.Syntax.Markdown
```
File deletion: Lean.lean
BF:BFD[8.209] → [8.3944:3977]
BF:BFD[8.3977] → [8.3978:3978]
B:BD[8.3978] → [8.3979:4006]
∅:D[4.1282] → [8.4006:4031]
B:BD[8.4006] → [8.4006:4031]
B:BD[8.4860] → [8.4860:4861]
∅:D[4.1346] → [8.5027:5028]
B:BD[8.5027] → [8.5027:5028]
B:BD[8.6698] → [8.6698:6716]
B:BD[8.4861] → [4.1283:1346]
B:BD[8.4006] → [4.1253:1282]
```
import ViE.UI.Syntax.Types
namespace ViE.UI.Syntax
end ViE.UI.Syntax
abbrev highlightLeanLine := Bliku.Tui.Syntax.highlightLeanLine
import Bliku.Tui.Syntax.Lean
```
Insertion in ViE/Types.lean at line 129 [5.22248]
[4.1726]
[9.8660]
```
  explorerPreviewSplitRatio : Float
```
Replacement in ViE/State/Layout.lean at line 175 [5.42444]
B:BD[6.34120] → [6.34120:34163]
```
  ws.floatingWindows.foldl (fun acc wid =>
```
[6.34120]
[6.34163]
```
  ws.floatingWindows.reverse.foldl (fun acc wid =>
```
Insertion in ViE/State/Config.lean at line 30 [5.53268]
[4.1908]
[9.18751]
```
  explorerPreviewSplitRatio := 0.5
```

Insertion in ViE/Command/Explorer.lean at line 20 [5.108658]

[10.5089]

private partial def setSplitRatioForPair (layout : Layout) (leftId rightId : Nat) (ratio : Float) : Layout :=
  match layout with
  | .window _ _ => layout
  | .hsplit left right currentRatio =>
      let leftHasLeft := left.containsWindow leftId
      let leftHasRight := left.containsWindow rightId
      let rightHasLeft := right.containsWindow leftId
      let rightHasRight := right.containsWindow rightId
      if (leftHasLeft && rightHasRight) || (leftHasRight && rightHasLeft) then
        .hsplit left right ratio
      else if leftHasLeft && leftHasRight then
        .hsplit (setSplitRatioForPair left leftId rightId ratio) right currentRatio
      else if rightHasLeft && rightHasRight then
        .hsplit left (setSplitRatioForPair right leftId rightId ratio) currentRatio
      else
        .hsplit left right currentRatio
  | .vsplit top bottom currentRatio =>
      let topHasLeft := top.containsWindow leftId
      let topHasRight := top.containsWindow rightId
      let bottomHasLeft := bottom.containsWindow leftId
      let bottomHasRight := bottom.containsWindow rightId
      if topHasLeft && topHasRight then
        .vsplit (setSplitRatioForPair top leftId rightId ratio) bottom currentRatio
      else if bottomHasLeft && bottomHasRight then
        .vsplit top (setSplitRatioForPair bottom leftId rightId ratio) currentRatio
      else
        .vsplit top bottom currentRatio
private def applyExplorerPreviewRatio (state : EditorState) (explorerWinId previewWinId : Nat) : EditorState :=
  state.updateCurrentWorkspace fun ws =>
    { ws with
        layout := setSplitRatioForPair ws.layout explorerWinId previewWinId state.config.explorerPreviewSplitRatio
    }

Replacement in ViE/Command/Explorer.lean at line 74 [5.108658]

B:BD[6.71511] → [6.71511:71569]

    let ws := ws.setWindowFloating ws.activeWindowId true

[6.71511]

[6.71569]

    let ws := ws.setWindowFloating ws.activeWindowId false

Replacement in ViE/Command/Explorer.lean at line 79 [5.108658]
B:BD[6.71687] → [6.71687:71729]
```
            ws.setWindowFloating wid true
```
[6.71687]
[6.71729]
```
            ws.setWindowFloating wid false
```
Insertion in ViE/Command/Explorer.lean at line 357 [5.108658]
[11.18655]
[11.18655]
```
    let explorerWinId := ws.activeWindowId
```

Replacement in ViE/Command/Explorer.lean at line 359 [5.108658]

B:BD[11.18695] → [11.18695:18744]

    let s1 := ViE.Window.splitWindow state false

[11.18695]

[11.18793]

    let s1 := applyExplorerPreviewRatio (ViE.Window.splitWindow state false) explorerWinId previewWinId

Insertion in ViE/Command/Explorer.lean at line 441 [5.108658]
[12.5677]
[12.5677]
```
            let explorerWinId := ws.activeWindowId
```

Replacement in ViE/Command/Explorer.lean at line 443 [5.108658]

B:BD[12.5725] → [12.5725:5782]

            let s1 := ViE.Window.splitWindow state false

[12.5725]

[12.5782]

            let s1 := applyExplorerPreviewRatio (ViE.Window.splitWindow state false) explorerWinId previewWinId

Insertion in ViE/Command/Explorer.lean at line 453 [5.108658]
[11.20948]
[11.20948]
```
          let explorerWinId := ws.activeWindowId
```

Replacement in ViE/Command/Explorer.lean at line 455 [5.108658]

B:BD[11.20994] → [11.20994:21049]

          let s1 := ViE.Window.splitWindow state false

[11.20994]

[12.6337]

          let s1 := applyExplorerPreviewRatio (ViE.Window.splitWindow state false) explorerWinId previewWinId

Insertion in ViE/Command/Explorer.lean at line 467 [5.108658]
[12.6676]
[12.6676]
```
          let explorerWinId := ws.activeWindowId
```

Replacement in ViE/Command/Explorer.lean at line 469 [5.108658]

B:BD[12.6722] → [12.6722:6777]

          let s1 := ViE.Window.splitWindow state false

[12.6722]

[12.6777]

          let s1 := applyExplorerPreviewRatio (ViE.Window.splitWindow state false) explorerWinId previewWinId

Insertion in ViE/Command/Explorer.lean at line 485 [5.108658]
[6.78091]
[6.78091]
```
              let explorerWinId := ws.activeWindowId
```

Replacement in ViE/Command/Explorer.lean at line 487 [5.108658]

B:BD[6.78141] → [6.78141:78200]

              let s1 := ViE.Window.splitWindow state false

[6.78141]

[6.78200]

              let s1 := applyExplorerPreviewRatio (ViE.Window.splitWindow state false) explorerWinId previewWinId

Deletion in ViE/BlikuAdapter.lean at line 8 [3.2460]

B:BD[3.2567] → [3.2567:2845]

private def toBlikuMode (m : ViE.Mode) : Bliku.Tui.Mode :=
  match m with
  | .normal => .normal
  | .insert => .insert
  | .command => .command
  | .searchForward => .searchForward
  | .searchBackward => .searchBackward
  | .visual => .visual
  | .visualBlock => .visualBlock

Replacement in ViE/BlikuAdapter.lean at line 13 [3.2460]
B:BD[3.3024] → [3.3024:3051]
```
    bufferId := v.bufferId
```
[3.3024]
[3.3051]
```
    contentId := v.bufferId
```
Replacement in ViE/BlikuAdapter.lean at line 21 [3.2460]
B:BD[3.3247] → [3.3247:3294]
```
  | .window id v => .window id (toBlikuView v)
```
[3.3247]
[3.3294]
```
  | .window id v => .pane id (toBlikuView v)
```

Insertion in ViE/BlikuAdapter.lean at line 24 [3.2460]

[3.3472]


private def containsBoth (l : Bliku.Tui.Layout) (a b : Nat) : Bool :=
  l.containsWindow a && l.containsWindow b
private partial def wrapClusterSubtree
    (l : Bliku.Tui.Layout) (clusterId paneA paneB : Nat) : Bliku.Tui.Layout :=
  if !(containsBoth l paneA paneB) then
    l
  else
    match l with
    | .group gid body =>
        if containsBoth body paneA paneB then
          .group gid (wrapClusterSubtree body clusterId paneA paneB)
        else
          l
    | .hsplit left right ratio =>
        if containsBoth left paneA paneB then
          .hsplit (wrapClusterSubtree left clusterId paneA paneB) right ratio
        else if containsBoth right paneA paneB then
          .hsplit left (wrapClusterSubtree right clusterId paneA paneB) ratio
        else
          .group clusterId l
    | .vsplit top bottom ratio =>
        if containsBoth top paneA paneB then
          .vsplit (wrapClusterSubtree top clusterId paneA paneB) bottom ratio
        else if containsBoth bottom paneA paneB then
          .vsplit top (wrapClusterSubtree bottom clusterId paneA paneB) ratio
        else
          .group clusterId l
    | .pane _ _ => l

Replacement in ViE/BlikuAdapter.lean at line 64 [3.2460]

B:BD[3.3860] → [3.3860:3972]

    if c.cursorCharStyle.isEmpty then (ViE.Color.toBg .white) ++ (ViE.Color.toFg .black) else c.cursorCharStyle

[3.3860]

[3.3972]

    if c.cursorCharStyle.isEmpty then
      (ViE.Color.toBg .white) ++ (ViE.Color.toFg .black)
    else
      c.cursorCharStyle

Replacement in ViE/BlikuAdapter.lean at line 69 [3.2460]

B:BD[3.3998] → [3.3998:4112]

    if c.cursorSpaceStyle.isEmpty then (ViE.Color.toBg .white) ++ (ViE.Color.toFg .black) else c.cursorSpaceStyle

[3.3998]

[3.4112]

    if c.cursorSpaceStyle.isEmpty then
      (ViE.Color.toBg .white) ++ (ViE.Color.toFg .black)
    else
      c.cursorSpaceStyle
  let floatingChromeActiveStyle :=
    if c.statusBarStyle.isEmpty then
      (ViE.Color.toFg .cyan)
    else
      c.statusBarStyle
  let floatingChromeInactiveStyle :=
    if c.statusBarStyle.isEmpty then
      (ViE.Color.toFg .white)
    else
      c.statusBarStyle

Insertion in ViE/BlikuAdapter.lean at line 95 [3.2460]

[3.4558]

    floatingChromeActiveStyle := floatingChromeActiveStyle
    floatingChromeInactiveStyle := floatingChromeInactiveStyle

Replacement in ViE/BlikuAdapter.lean at line 100 [3.2460]

B:BD[3.4588] → [3.4588:4673]

private def toBlikuOverlay (ov : ViE.FloatingOverlay) : Bliku.Tui.FloatingOverlay :=

[3.4588]

[3.4673]

private def toBlikuOverlay (ov : ViE.FloatingOverlay) : Bliku.Tui.OverlayView :=

Replacement in ViE/BlikuAdapter.lean at line 109 [3.2460]

B:BD[3.4814] → [3.4814:4902]

private def toBlikuCompletion (cp : ViE.CompletionPopup) : Bliku.Tui.CompletionPopup :=

[3.4814]

[3.4902]

private def toBlikuCompletion (cp : ViE.CompletionPopup) : Bliku.Tui.CompletionView :=

Insertion in ViE/BlikuAdapter.lean at line 131 [3.2460]

[3.5512]

private def explorerClusterSpecs (state : ViE.EditorState) : Array (Nat × Nat × Nat) := Id.run do
  let ws := state.getCurrentWorkspace
  let mut specs : Array (Nat × Nat × Nat) := #[]
  for (bufId, explorer) in state.explorers.reverse do
    match ws.layout.findWindowIdByBufferId bufId, explorer.previewWindowId with
    | some explorerWinId, some previewWinId =>
        if ws.layout.containsWindow previewWinId then
          specs := specs.push (bufId, explorerWinId, previewWinId)
    | _, _ => pure ()
  return specs
private def toBlikuDesktop (state : ViE.EditorState) : Bliku.DesktopLayout :=
  let ws := state.getCurrentWorkspace
  let clusterSpecs := explorerClusterSpecs state
  let groupedLayout :=
    clusterSpecs.foldl
      (fun acc (clusterId, explorerWinId, previewWinId) =>
        wrapClusterSubtree acc clusterId explorerWinId previewWinId)
      (toBlikuLayout ws.layout)
  let clusteredPaneIds := clusterSpecs.foldl (fun acc (_, explorerWinId, previewWinId) =>
    acc.push explorerWinId |>.push previewWinId) #[]
  let paneClusters :=
    ws.getFloatingWindowIds.foldl (fun acc wid =>
      if clusteredPaneIds.contains wid then
        acc
      else
        let (rowOff, colOff) := ws.getFloatingWindowOffset wid
        acc.push { root := .pane wid, rowOffset := rowOff, colOffset := colOff, sizePolicy := .default }) #[]
  let groupClusters :=
    clusterSpecs.map fun (clusterId, explorerWinId, _) =>
      let (rowOff, colOff) := ws.getFloatingWindowOffset explorerWinId
      {
        root := .group clusterId
        rowOffset := rowOff
        colOffset := colOff
        sizePolicy := .multiPane
        chrome := { kind := .bordered, title := some "Explorer" }
      }
  {
    layout := groupedLayout
    activePaneId := ws.activeWindowId
    floating := { clusters := paneClusters ++ groupClusters }
  }
private def toBlikuSelection (state : ViE.EditorState) : Option Bliku.Tui.SelectionState :=
  match state.selectionStart with
  | none => none
  | some anchor =>
      if state.mode == .visual || state.mode == .visualBlock then
        some {
          anchor := toBlikuCursor anchor
          cursor := toBlikuCursor state.getCursor
          block := state.mode == .visualBlock
        }
      else
        none
private def toBlikuCommandLine (state : ViE.EditorState) : Option Bliku.Tui.CommandLineState :=
  let text := state.inputState.commandBuffer
  match state.mode with
  | .command => some { leader := ":", text := text, cursorCol := text.length }
  | .searchForward => some { leader := "/", text := text, cursorCol := text.length }
  | .searchBackward => some { leader := "?", text := text, cursorCol := text.length }
  | _ => none
private def statusLine (state : ViE.EditorState) : String :=
  let ws := state.getCurrentWorkspace
  let buf := state.getActiveBuffer
  let fileName := buf.filename.getD "[No Name]"
  let eolMark := if buf.missingEol then " [noeol]" else ""
  s!"-- {state.mode} -- {fileName}{eolMark} [W:{ws.activeWindowId} B:{buf.id}] [{state.getCurrentWorkgroup.name}] {ws.name}"
private def toRenderInput (state : ViE.EditorState) : Bliku.Tui.RenderInput :=
  {
    selection := toBlikuSelection state
    commandLine := toBlikuCommandLine state
    messageLine := state.message
    statusLine := statusLine state
    overlay := state.floatingOverlay.map toBlikuOverlay
    completion := state.completionPopup.map toBlikuCompletion
    hideTerminalCursor :=
      state.mode != .command &&
      state.mode != .searchForward &&
      state.mode != .searchBackward &&
      state.floatingOverlay.isNone
  }

Deletion in ViE/BlikuAdapter.lean at line 220 [3.2460]
B:BD[3.5609] → [3.5609:5647]
```
  let wg := state.getCurrentWorkgroup
```
Deletion in ViE/BlikuAdapter.lean at line 221 [3.2460]
B:BD[3.5651] → [3.5651:5715]
```
    mode := toBlikuMode state.mode
    workgroupName := wg.name
```

Replacement in ViE/BlikuAdapter.lean at line 223 [3.2460]

B:BD[3.5756] → [3.5756:5938]

      layout := toBlikuLayout ws.layout
      activeWindowId := ws.activeWindowId
      floatingWindows := ws.floatingWindows
      floatingWindowOffsets := ws.floatingWindowOffsets

[3.5756]

[3.5938]

      desktop := toBlikuDesktop state

Deletion in ViE/BlikuAdapter.lean at line 226 [3.2460]

B:BD[3.5996] → [3.5996:6269]

    selectionStart := state.selectionStart.map toBlikuCursor
    message := state.message
    commandBuffer := state.inputState.commandBuffer
    floatingOverlay := state.floatingOverlay.map toBlikuOverlay
    completionPopup := state.completionPopup.map toBlikuCompletion

Replacement in ViE/BlikuAdapter.lean at line 240 [3.2460]

B:BD[3.6692] → [3.6692:6732]

  let model' ← Bliku.Tui.render model

[3.6692]

[3.6732]

  let input := toRenderInput state
  let model' ← Bliku.Tui.renderWith model input

Replacement in Test/Workspace.lean at line 74 [11.62930]

B:BD[6.90857] → [6.90857:90964]

  assertEqual "Workspace explorer opens in floating window" true (ws8.isFloatingWindow ws8.activeWindowId)

[6.90857]

[11.65688]

  assertEqual "Workspace explorer opens in regular window" false (ws8.isFloatingWindow ws8.activeWindowId)

Replacement in Test/Workspace.lean at line 153 [11.62930]

B:BD[12.8935] → [6.91334:91442]

    assertEqual "Workspace explorer preview window is floating" true (wsPrev.isFloatingWindow previewWinId)

[12.8935]

[6.91442]

    assertEqual "Workspace explorer preview window is regular" false (wsPrev.isFloatingWindow previewWinId)

Replacement in Test/Workspace.lean at line 155 [11.62930]

B:BD[6.91468] → [6.91468:91635]

      match s12c.getFloatingWindowBounds wsPrev.activeWindowId, s12c.getFloatingWindowBounds previewWinId with
      | some (et, el, eh, ew), some (pt, pl, ph, pw) =>

[6.91468]

[6.91635]

      match (ViE.Window.getAllWindowBounds wsPrev.layout (if s12c.windowHeight > 0 then s12c.windowHeight - 1 else 0) s12c.windowWidth).find? (fun (id, _, _, _, _) => id == wsPrev.activeWindowId),
            (ViE.Window.getAllWindowBounds wsPrev.layout (if s12c.windowHeight > 0 then s12c.windowHeight - 1 else 0) s12c.windowWidth).find? (fun (id, _, _, _, _) => id == previewWinId) with
      | some (_, et, el, eh, ew), some (_, pt, pl, ph, pw) =>

Replacement in Test/Workspace.lean at line 160 [11.62930]

B:BD[6.91728] → [6.91728:91823]

    assertEqual "Workspace explorer/preview floating pair is side-by-side" true pairSideBySide

[6.91728]

[12.8935]

    assertEqual "Workspace explorer/preview pair is side-by-side" true pairSideBySide

Replacement in Test/WorkgroupExplorer.lean at line 39 [11.75776]

B:BD[6.91938] → [6.91938:92045]

  assertEqual "Workgroup explorer opens in floating window" true (ws2.isFloatingWindow ws2.activeWindowId)

[6.91938]

[11.77134]

  assertEqual "Workgroup explorer opens in regular window" false (ws2.isFloatingWindow ws2.activeWindowId)

Replacement in Test/WorkgroupExplorer.lean at line 56 [11.75776]

B:BD[12.9749] → [6.92046:92154]

    assertEqual "Workgroup explorer preview window is floating" true (wsPrev.isFloatingWindow previewWinId)

[12.9749]

[6.92154]

    assertEqual "Workgroup explorer preview window is regular" false (wsPrev.isFloatingWindow previewWinId)

Replacement in Test/WorkgroupExplorer.lean at line 58 [11.75776]

B:BD[6.92180] → [6.92180:92343]

      match s2.getFloatingWindowBounds wsPrev.activeWindowId, s2.getFloatingWindowBounds previewWinId with
      | some (et, el, eh, ew), some (pt, pl, ph, pw) =>

[6.92180]

[6.92343]

      match (ViE.Window.getAllWindowBounds wsPrev.layout (if s2.windowHeight > 0 then s2.windowHeight - 1 else 0) s2.windowWidth).find? (fun (id, _, _, _, _) => id == wsPrev.activeWindowId),
            (ViE.Window.getAllWindowBounds wsPrev.layout (if s2.windowHeight > 0 then s2.windowHeight - 1 else 0) s2.windowWidth).find? (fun (id, _, _, _, _) => id == previewWinId) with
      | some (_, et, el, eh, ew), some (_, pt, pl, ph, pw) =>

Replacement in Test/WorkgroupExplorer.lean at line 63 [11.75776]

B:BD[6.92436] → [6.92436:92531]

    assertEqual "Workgroup explorer/preview floating pair is side-by-side" true pairSideBySide

[6.92436]

[12.9749]

    assertEqual "Workgroup explorer/preview pair is side-by-side" true pairSideBySide

Deletion in Test/SyntaxHighlight.lean at line 1 [7.23366]
B:BD[7.23366] → [7.23367:23388]
```
import ViE.UI.Syntax
```
Insertion in Test/SyntaxHighlight.lean at line 3 [7.23366]
[7.23427]
[7.23427]
```
import Bliku.Tui.Syntax
```

Replacement in Test/SyntaxHighlight.lean at line 14 [7.23366]

B:BD[7.23685] → [7.23685:23752]

  let spans := ViE.UI.Syntax.highlightLine (some "Main.lean") line

[7.23685]

[7.23752]

  let spans := Bliku.Tui.Syntax.highlightLine (some "Main.lean") line

Replacement in Test/SyntaxHighlight.lean at line 18 [7.23366]

B:BD[7.23938] → [7.23938:24305]

  assertEqual "Lean keyword style" (some ViE.UI.Syntax.leanKeywordStyle) (ViE.UI.Syntax.styleForByteRange spans defS defE)
  assertEqual "Lean number style" (some ViE.UI.Syntax.leanNumberStyle) (ViE.UI.Syntax.styleForByteRange spans numS numE)
  assertEqual "Lean comment style" (some ViE.UI.Syntax.leanCommentStyle) (ViE.UI.Syntax.styleForByteRange spans comS comE)

[7.23938]

[7.24305]

  assertEqual "Lean keyword style" (Bliku.Tui.Syntax.defaultPalette.faceFor .keyword)
    (Bliku.Tui.Syntax.faceForByteRange Bliku.Tui.Syntax.defaultPalette spans defS defE)
  assertEqual "Lean number style" (Bliku.Tui.Syntax.defaultPalette.faceFor .numberLiteral)
    (Bliku.Tui.Syntax.faceForByteRange Bliku.Tui.Syntax.defaultPalette spans numS numE)
  assertEqual "Lean comment style" (Bliku.Tui.Syntax.defaultPalette.faceFor .comment)
    (Bliku.Tui.Syntax.faceForByteRange Bliku.Tui.Syntax.defaultPalette spans comS comE)

Replacement in Test/SyntaxHighlight.lean at line 27 [7.23366]

B:BD[7.24382] → [7.24382:24449]

  let spans := ViE.UI.Syntax.highlightLine (some "README.md") line

[7.24382]

[7.24449]

  let spans := Bliku.Tui.Syntax.highlightLine (some "README.md") line

Replacement in Test/SyntaxHighlight.lean at line 30 [7.23366]

B:BD[7.24584] → [7.24584:24838]

  assertEqual "Markdown code style" (some ViE.UI.Syntax.markdownCodeStyle) (ViE.UI.Syntax.styleForByteRange spans codeS codeE)
  assertEqual "Markdown link style" (some ViE.UI.Syntax.markdownLinkStyle) (ViE.UI.Syntax.styleForByteRange spans linkS linkE)

[7.24584]

[7.24838]

  assertEqual "Markdown code style" (Bliku.Tui.Syntax.defaultPalette.faceFor .code)
    (Bliku.Tui.Syntax.faceForByteRange Bliku.Tui.Syntax.defaultPalette spans codeS codeE)
  assertEqual "Markdown link style" (Bliku.Tui.Syntax.defaultPalette.faceFor .link)
    (Bliku.Tui.Syntax.faceForByteRange Bliku.Tui.Syntax.defaultPalette spans linkS linkE)

Insertion in Test/ExplorerPreview.lean at line 5 [11.80497]
[11.80603]
[11.80603]
```
import ViE.BlikuAdapter
```

Replacement in Test/ExplorerPreview.lean at line 32 [11.80497]

B:BD[6.118733] → [6.118733:118825]

  assert "File explorer opens in floating window" (ws1.isFloatingWindow ws1.activeWindowId)

[6.118733]

[6.118825]

  assert "File explorer opens in regular window" (!ws1.isFloatingWindow ws1.activeWindowId)
  let model1 := ViE.BlikuAdapter.toModel s1
  let explorerClustered :=
    match model1.workspace.floatingClusters[0]? with
    | some cluster =>
        match cluster.root, cluster.sizePolicy with
        | .group gid, .multiPane => gid == buf.id
        | _, _ => false
    | none => false
  assert "Bliku adapter lifts explorer/preview into floating multi-pane cluster" explorerClustered

Replacement in Test/ExplorerPreview.lean at line 77 [11.80497]
B:BD[11.82030] → [6.119473:119502]
```
      let previewFloating :=
```
[11.82030]
[6.119502]
```
      let previewRegular :=
```

Replacement in Test/ExplorerPreview.lean at line 79 [11.80497]

B:BD[6.119544] → [6.119544:119610]

        | some wid => s1.getCurrentWorkspace.isFloatingWindow wid

[6.119544]

[6.119610]

        | some wid => !s1.getCurrentWorkspace.isFloatingWindow wid

Replacement in Test/ExplorerPreview.lean at line 81 [11.80497]

B:BD[6.119634] → [6.119634:119705]

      assert "Preview window opens in floating window" previewFloating

[6.119634]

[6.119705]

      assert "Preview window opens in regular window" previewRegular

Replacement in Test/ExplorerPreview.lean at line 85 [11.80497]

B:BD[6.119797] → [6.119797:120000]

          let ws1 := s1.getCurrentWorkspace
          match s1.getFloatingWindowBounds ws1.activeWindowId, s1.getFloatingWindowBounds wid with
          | some (et, el, eh, ew), some (pt, pl, ph, pw) =>

[6.119797]

[6.120000]

          let bounds := ViE.Window.getAllWindowBounds s1.getCurrentWorkspace.layout
            (if s1.windowHeight > 0 then s1.windowHeight - 1 else 0) s1.windowWidth
          match bounds.find? (fun (id, _, _, _, _) => id == s1.getCurrentWorkspace.activeWindowId),
                bounds.find? (fun (id, _, _, _, _) => id == wid) with
          | some (_, et, el, eh, ew), some (_, pt, pl, ph, pw) =>

Replacement in Test/ExplorerPreview.lean at line 93 [11.80497]

B:BD[6.120123] → [6.120123:120200]

      assert "Explorer/preview floating pair is side-by-side" pairSideBySide

[6.120123]

[11.82030]

      assert "Explorer/preview pair is side-by-side" pairSideBySide

Replacement in Test/ExplorerPreview.lean at line 137 [11.80497]

B:BD[6.120310] → [6.120310:120433]

      assert "Opening file from floating explorer leaves non-floating window" (!ws5b.isFloatingWindow ws5b.activeWindowId)

[6.120310]

[6.120433]

      assert "Opening file from explorer leaves regular window" (!ws5b.isFloatingWindow ws5b.activeWindowId)

Insertion in Main.lean at line 8 [5.134883]
[5.134995]
[5.134995]
```
  -- View
```

Insertion in Main.lean at line 11 [5.134883]

[8.37879]

[13.2355]


  -- Splits
  vSplitStr := "│"
  hSplitStr := "─"
  -- Cursor / selection / search
  searchHighlightStyle := (toBg Color.white) ++ (toFg Color.black)
  searchHighlightCursorStyle := (toBg Color.yellow) ++ (toFg Color.black)
  visualSelectionStyle := "\x1b[7m"
  cursorCharStyle := (toBg Color.white) ++ (toFg Color.black)
  cursorSpaceStyle := (toBg Color.white) ++ (toFg Color.black)
  -- Explorer / preview
  explorerPreviewSplitRatio := 0.5
  -- Editing

Insertion in Main.lean at line 28 [5.134883]
[13.2370]
[5.135021]
```
  -- Status line / terminal reset
```

Replacement in Main.lean at line 31 [5.134883]

B:BD[5.135088] → [6.121707:121756]

  --fileIcon := "File: "
  --dirIcon := "Dir : "

[5.135088]

[5.135133]

  resetStyle := ViE.Color.reset
  -- Explorer icons
  fileIcon := "📄 "
  dirIcon := "📁 "
  -- Search bloom cache
  searchBloomCacheMax := 1024
  searchBloomBuildLeafBits := true
  searchBloomBuildOnEdit := false
  -- History
  historyLimit := 200
  -- Examples:
  -- fileIcon := "File: "
  -- dirIcon := "Dir : "
  -- explorerPreviewSplitRatio := 0.62
  -- tabStop := 4
  -- showLineNumbers := false

Replacement in Main.lean at line 85 [5.134883]
B:BD[5.136077] → [2.8105:8128]
```
  ViE.start config args
```
[5.136077]
```
  ViE.start config args
```

Update ViE for Bliku clustered floating UI and direct syntax API

Dependencies

In channels

Change contents

Replacement in lake-manifest.json at line 8 [5.273]

File deletion: Syntax.lean

Deletion in ViE/UI/Window.lean at line 3 [6.1840]

Insertion in ViE/UI/Window.lean at line 4 [6.1840]

Replacement in ViE/UI/Window.lean at line 91 [6.1840]

Replacement in ViE/UI/Window.lean at line 129 [6.1840]

Replacement in ViE/UI/Window.lean at line 205 [6.1840]

Replacement in ViE/UI/Window.lean at line 227 [6.1840]

File deletion: Types.lean

File deletion: Markdown.lean

File deletion: Lean.lean

Insertion in ViE/Types.lean at line 129 [5.22248]

Replacement in ViE/State/Layout.lean at line 175 [5.42444]

Insertion in ViE/State/Config.lean at line 30 [5.53268]

Insertion in ViE/Command/Explorer.lean at line 20 [5.108658]

Replacement in ViE/Command/Explorer.lean at line 74 [5.108658]

Replacement in ViE/Command/Explorer.lean at line 79 [5.108658]

Insertion in ViE/Command/Explorer.lean at line 357 [5.108658]