DZFBJ6N3AUGLLLO5BKMLKW7D2ZRBQ2N3GDSY22TTWLSSFZUVLC2AC private def floatingClusterLayoutTest : IO Unit := dolet layout : Bliku.PaneLayout :=.hsplit(.pane 0 { contentId := 0, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 })(.group 100 <|.vsplit(.pane 1 { contentId := 1, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 })(.pane 2 { contentId := 2, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 })0.5)0.5let desktop : Bliku.DesktopLayout := {layout := layoutactivePaneId := 2floating := {clusters := #[{ root := .group 100, rowOffset := 1, colOffset := 2 }]}}let ws : WorkspaceView := { name := "test", desktop := desktop }assertEq "floating-cluster-pane-1" (ws.isFloatingWindow 1) trueassertEq "floating-cluster-pane-2" (ws.isFloatingWindow 2) trueassertEq "floating-cluster-pane-0" (ws.isFloatingWindow 0) falselet extracted := layout.extractFloatingRoot (.group 100) |>.map Bliku.PaneLayout.getPaneIdsassertEq "floating-cluster-extract" extracted (some [1, 2])let removed := layout.removeFloatingRoot (.group 100) |>.map Bliku.PaneLayout.getPaneIdsassertEq "floating-cluster-remove" removed (some [0])private def floatingSizePolicyTest : IO Unit := dolet defaultBounds :=Bliku.computeFloatingClusterBounds 50 160 0 { root := .pane 1, sizePolicy := .default }let multiBounds :=Bliku.computeFloatingClusterBounds 50 160 0 { root := .group 100, sizePolicy := .multiPane }let customBounds :=Bliku.computeFloatingClusterBounds 50 160 0 {root := .group 200sizePolicy := .custom {width := .fixed 120height := .ratio 0.5minWidth := some 80maxHeight := some 30}}let some (_, _, defaultH, defaultW) := defaultBounds| throw <| IO.userError "default bounds missing"let some (_, _, multiH, multiW) := multiBounds| throw <| IO.userError "multi bounds missing"let some (_, _, customH, customW) := customBounds| throw <| IO.userError "custom bounds missing"assertEq "floating-size-multipane-wider" (decide (multiW > defaultW)) trueassertEq "floating-size-multipane-taller" (decide (multiH > defaultH)) trueassertEq "floating-size-custom-width" customW 120assertEq "floating-size-custom-height" customH 24private def floatingChromeBoxTest : IO Unit := dolet box := Bliku.Widget.renderFloatingChromeBox{ kind := .bordered, title := some "Explorer" }16 4"[A]" "[I]" "[/]"trueassertEq "floating-chrome-line-count" box.lines.size 4assertEq "floating-chrome-inset-top" box.insetTop 1assertEq "floating-chrome-inset-left" box.insetLeft 1assertEq "floating-chrome-top-line" box.lines[0]! "[A]┌ Explorer ────┐[/]"private def rectSafeLineRenderTest : IO Unit := dolet buf : BufferState := {id := 0filename := nonelines := #["abc"]}let rendered := renderVisibleLineInRect mkModel {} buf 0 0 0 5 noneassertEq "rect-safe-line-render" rendered "abc "assertEq "rect-safe-line-no-clear" (rendered.contains '\x1b' && rendered.contains 'K') falseprivate def eofMarkerPlacementTest : IO Unit := dolet marker := renderEmptyLineMarkerInRect { emptyLineMarker := "・" } 6assertEq "eof-marker-placement" marker "・ "
import Bliku.Decorationnamespace Bliku.Widgetopen Blikustructure TextViewProps wherelines : Array StringscrollCol : Nat := 0byteDecorations : Array ByteDecoration := #[]cellDecorations : Array CellDecoration := #[]cursor : Option CursorDecoration := noneresetStyle : String := "\x1b[0m"deriving Inhabitedstructure VisibleCell wheretext : Stringcol : NatstartByte : NatendByte : Natderiving Repr, Inhabitedprivate def collectVisibleCells (line : String) (scrollCol width : Nat) : Array VisibleCell := Id.run dolet mut out : Array VisibleCell := #[]let mut bytePos := 0let mut col := 0for ch in line.toList dolet nextByte := bytePos + ch.utf8Sizeif scrollCol <= col && col < scrollCol + width thenout := out.push {text := ch.toStringcol := colstartByte := bytePosendByte := nextByte}bytePos := nextBytecol := col + 1outprivate def lineDisplayLength (line : String) : Nat :=line.toList.lengthprivate def faceForByteRange(decos : Array ByteDecoration) (row byteStart byteEnd : Nat) : Option String :=let rec loop (i : Nat) (best : Option ByteDecoration) : Option String :=if i >= decos.size thenbest.map ByteDecoration.styleelselet deco := decos[i]!let best' :=if deco.row == row && byteStart < deco.endByte && byteEnd > deco.startByte thenmatch best with| none => some deco| some current => if current.priority <= deco.priority then some deco else bestelsebestloop (i + 1) best'loop 0 noneprivate def faceForCell(decos : Array CellDecoration) (row col : Nat) : Option String :=let rec loop (i : Nat) (best : Option CellDecoration) : Option String :=if i >= decos.size thenbest.map CellDecoration.styleelselet deco := decos[i]!let best' :=if deco.row == row && deco.startCol <= col && col < deco.endCol thenmatch best with| none => some deco| some current => if current.priority <= deco.priority then some deco else bestelsebestloop (i + 1) best'loop 0 nonedef renderVisibleLine (props : TextViewProps) (row width : Nat) : String := Id.run dolet line := props.lines[row]?.getD ""let visibleCells := collectVisibleCells line props.scrollCol widthlet mut out : Array String := #[]let mut activeStyle : Option String := nonefor cell in visibleCells dolet desiredStyle : Option String :=match props.cursor with| some cur =>if cur.row == row && cur.col == cell.col thensome (if cell.text == " " then cur.spaceStyle else cur.charStyle)else(faceForCell props.cellDecorations row cell.col).orElse(fun _ => faceForByteRange props.byteDecorations row cell.startByte cell.endByte)| none =>(faceForCell props.cellDecorations row cell.col).orElse(fun _ => faceForByteRange props.byteDecorations row cell.startByte cell.endByte)if desiredStyle != activeStyle thenmatch activeStyle with| some _ => out := out.push props.resetStyle| none => pure ()match desiredStyle with| some style => out := out.push style| none => pure ()activeStyle := desiredStyleout := out.push cell.textif activeStyle.isSome thenout := out.push props.resetStylereturn String.intercalate "" out.toListdef appendCursorOnBlankCell (props : TextViewProps) (row width : Nat) (lineToDraw : String) : String := Id.run dolet some cur := props.cursor | return lineToDrawif cur.row != row || cur.col < props.scrollCol thenreturn lineToDrawlet line := props.lines[row]?.getD ""let visCol := cur.col - props.scrollCollet visLen := min width (lineDisplayLength line - props.scrollCol)if visCol < visLen || visCol >= width thenreturn lineToDrawlet padCount := visCol - visLenreturn lineToDraw ++ ("".pushn ' ' padCount) ++ cur.spaceStyle ++ " " ++ props.resetStyleend Bliku.Widget
namespace Bliku.Widgetstructure PromptProps whereleader : String := ""text : String := ""cursorCol : Nat := 0deriving Repr, Inhabiteddef renderPrompt (props : PromptProps) : String :=props.leader ++ props.textdef promptCursorCol (props : PromptProps) : Nat :=props.leader.length + props.cursorColend Bliku.Widget
namespace Bliku.Widgetstructure PopupProps wheretitle : String := ""lines : Array String := #[]maxWidth : Nat := 0borderCorner : String := "+"borderHorizontal : Char := '-'borderVertical : String := "|"deriving Inhabitedstructure PopupBox wherelines : Array StringinnerWidth : NattitleRows : NatcontentRows : Natderiving Inhabiteddef renderPopupBox (props : PopupProps) : PopupBox := Id.run dolet lines := if props.lines.isEmpty then #[""] else props.lineslet titleText := if props.title.isEmpty then "" else s!"[{props.title}]"let titleRows := if titleText.isEmpty then 0 else 1let naturalWidthContent := lines.foldl (fun acc ln => max acc ln.length) 0let naturalWidth := max naturalWidthContent titleText.lengthlet innerWidth := max 1 (if props.maxWidth > 0 then min props.maxWidth naturalWidth else naturalWidth)let border := props.borderCorner ++ "".pushn props.borderHorizontal (innerWidth + 2) ++ props.borderCornerlet mut out : Array String := #[border]if titleRows == 1 thenlet clipped := (titleText.take innerWidth).toStringlet pad := if clipped.length < innerWidth then "".pushn ' ' (innerWidth - clipped.length) else ""out := out.push s!"{props.borderVertical} {clipped}{pad} {props.borderVertical}"for raw in lines dolet clipped := (raw.take innerWidth).toStringlet pad := if clipped.length < innerWidth then "".pushn ' ' (innerWidth - clipped.length) else ""out := out.push s!"{props.borderVertical} {clipped}{pad} {props.borderVertical}"out := out.push borderreturn { lines := out, innerWidth := innerWidth, titleRows := titleRows, contentRows := lines.size }end Bliku.Widget
namespace Bliku.Widgetstructure ListItem wherelabel : Stringderiving Repr, Inhabitedstructure ListProps whereitems : Array ListItemselected : Nat := 0maxVisible : Nat := 8width : Nat := 0borderLeft : String := "|"borderRight : String := "|"borderFill : Char := '-'selectedStyle : String := "\x1b[7m"resetStyle : String := "\x1b[0m"deriving Inhabitedstructure ListBox wherelines : Array Stringwidth : Natheight : Natderiving Inhabiteddef renderListBox (props : ListProps) : ListBox := Id.run doif props.items.isEmpty thenreturn { lines := #[], width := 0, height := 0 }let visibleCount := min props.maxVisible props.items.sizelet labels := props.items.extract 0 visibleCount |>.map ListItem.labellet naturalW := labels.foldl (fun acc s => max acc s.length) 0let innerWidth := max 1 (if props.width == 0 then naturalW else props.width)let border := props.borderLeft ++ "".pushn props.borderFill innerWidth ++ props.borderRightlet selected := if props.selected < visibleCount then props.selected else 0let mut out : Array String := #[border]for i in [0:visibleCount] dolet label := (labels[i]!.take innerWidth).toStringlet pad := if label.length < innerWidth then "".pushn ' ' (innerWidth - label.length) else ""let body :=if i == selected thenprops.selectedStyle ++ label ++ pad ++ props.resetStyleelselabel ++ padout := out.push (props.borderLeft ++ body ++ props.borderRight)out := out.push borderreturn { lines := out, width := innerWidth + props.borderLeft.length + props.borderRight.length, height := out.size }end Bliku.Widget
import Bliku.Layoutnamespace Bliku.Widgetstructure ChromeBox wherelines : Array StringinsetTop : Nat := 0insetLeft : Nat := 0insetBottom : Nat := 0insetRight : Nat := 0deriving Inhabiteddef renderFloatingChromeBox(chrome : Bliku.FloatingChrome)(width height : Nat)(activeStyle inactiveStyle resetStyle : String)(isActive : Bool) : ChromeBox := Id.run doif chrome.kind == .none || width < 2 || height < 2 thenreturn { lines := #[] }let style := if isActive then activeStyle else inactiveStylelet title := chrome.title.getD ""let topFill := if width > 2 then width - 2 else 0let rawTop := if title.isEmpty then "".pushn '─' topFill elselet core := s!" {title} "let clipped := (core.take topFill).toStringclipped ++ "".pushn '─' (topFill - clipped.length)let top := style ++ "┌" ++ rawTop ++ "┐" ++ resetStylelet middle := style ++ "│" ++ resetStyle ++ "".pushn ' ' (width - 2) ++ style ++ "│" ++ resetStylelet bottom := style ++ "└" ++ "".pushn '─' topFill ++ "┘" ++ resetStylelet mut lines : Array String := #[top]for _ in [0:height - 2] dolines := lines.push middlelines := lines.push bottomreturn {lines := linesinsetTop := 1insetLeft := 1insetBottom := 1insetRight := 1}end Bliku.Widget
def WorkspaceView.floatingWindows (ws : WorkspaceView) : List Nat :=(ws.desktop.floating.getClusters ws.layout).foldl(fun acc cluster =>match ws.layout.extractFloatingRoot cluster.root with| some subtree => acc ++ subtree.getPaneIds| none => acc)[]def WorkspaceView.floatingWindowOffsets (ws : WorkspaceView) : List (Nat × Int × Int) :=(ws.desktop.floating.getClusters ws.layout).foldl(fun acc cluster =>match cluster.root with| .pane wid => (wid, cluster.rowOffset, cluster.colOffset) :: acc| .group _ => acc)[]def WorkspaceView.floatingClusters (ws : WorkspaceView) : Array Bliku.FloatingCluster :=ws.desktop.floating.getClusters ws.layout
match l with| .window wid v => if wid == id then some v else none| .hsplit left right _ => (left.findView id).orElse (fun _ => right.findView id)| .vsplit top bottom _ => (top.findView id).orElse (fun _ => bottom.findView id)
Bliku.PaneLayout.findView l id
let rec go (node : Layout) : Layout × Bool :=match node with| .window wid v =>if wid == id then (.window wid (f v), true) else (node, false)| .hsplit left right ratio =>let (left', foundLeft) := go leftif foundLeft then(.hsplit left' right ratio, true)elselet (right', foundRight) := go right(.hsplit left' right' ratio, foundRight)| .vsplit top bottom ratio =>let (top', foundTop) := go topif foundTop then(.vsplit top' bottom ratio, true)elselet (bottom', foundBottom) := go bottom(.vsplit top' bottom' ratio, foundBottom)(go l).1
Bliku.PaneLayout.updateView l id f
match l with| .window wid _ => if wid == id then none else some l| .hsplit left right ratio =>match left.remove id with| none => some right| some left' =>match right.remove id with| none => some left'| some right' => some (.hsplit left' right' ratio)| .vsplit top bottom ratio =>match top.remove id with| none => some bottom| some top' =>match bottom.remove id with| none => some top'| some bottom' => some (.vsplit top' bottom' ratio)
Bliku.PaneLayout.remove l id
let rec traverse (node : Layout) (r c h w : Nat) (acc : List (Nat × Nat × Nat × Nat × Nat)) :=match node with| .window id _ => (id, r, c, h, w) :: acc| .hsplit left right ratio =>let leftW := (Float.ofNat w * ratio).toUInt64.toNatlet acc' := traverse left r c h leftW acctraverse right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0) acc'| .vsplit top bottom ratio =>let topH := (Float.ofNat h * ratio).toUInt64.toNatlet acc' := traverse top r c topH w acctraverse bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w acc'traverse l 0 0 h w []
l.getAllPaneBounds h w
if i >= ids.size then noneelse if ids[i]! == windowId then some ielse loop (i + 1)
if i >= clusters.size thennoneelsematch ws.layout.extractFloatingRoot clusters[i]!.root with| some subtree =>if subtree.getPaneIds.contains windowId then some i else loop (i + 1)| none => loop (i + 1)
let availableRows := if rows > 1 then rows - 1 else rowsif availableRows < 6 || cols < 16 thennoneelselet hMax := availableRows - 2let wMax := cols - 4let h := min hMax (max 8 ((availableRows * 3) / 5))let w := min wMax (max 24 ((cols * 3) / 5))let topBase := (availableRows - h) / 2let leftBase := (cols - w) / 2let top := min (availableRows - h) (topBase + idx)let left := min (cols - w) (leftBase + (2 * idx))some (top, left, h, w)
Bliku.computeFloatingClusterBounds rows cols idx { root := .pane idx }def computeFloatingClusterBounds (rows cols idx : Nat) (cluster : Bliku.FloatingCluster) : Option (Nat × Nat × Nat × Nat) :=Bliku.computeFloatingClusterBounds rows cols idx cluster
| some (top, left, h, w) =>let (rowOff, colOff) := ws.getFloatingWindowOffset windowIdlet toNatNonNeg (v : Int) := if v < 0 then 0 else Int.toNat vlet availableRows := if windowHeight > 1 then windowHeight - 1 else windowHeightlet maxTop := if availableRows > h then availableRows - h else 0let maxLeft := if windowWidth > w then windowWidth - w else 0let rawTop := Int.ofNat top + rowOfflet rawLeft := Int.ofNat left + colOfflet top' := min maxTop (toNatNonNeg rawTop)let left' := min maxLeft (toNatNonNeg rawLeft)some (top', left', h, w)
| some cluster =>match computeFloatingClusterBounds windowHeight windowWidth idx cluster with| none => none| some (top, left, h, w) =>let (rowOff, colOff) := (cluster.rowOffset, cluster.colOffset)let toNatNonNeg (v : Int) := if v < 0 then 0 else Int.toNat vlet availableRows := if windowHeight > 1 then windowHeight - 1 else windowHeightlet maxTop := if availableRows > h then availableRows - h else 0let maxLeft := if windowWidth > w then windowWidth - w else 0let rawTop := Int.ofNat top + rowOfflet rawLeft := Int.ofNat left + colOfflet top' := min maxTop (toNatNonNeg rawTop)let left' := min maxLeft (toNatNonNeg rawLeft)some (top', left', h, w)
inductive Color where| ansi (code : Nat)| rgb (r g b : Nat)deriving Repr, BEq, Inhabitedstructure Face wherefg : Option Color := nonebg : Option Color := nonebold : Bool := falseitalic : Bool := falseunderline : Bool := falsederiving Repr, BEq, Inhabited
abbrev Color := Bliku.Colorabbrev Face := Bliku.Face
private def colorToAnsi (channel : String) : Color → String| .ansi code => s!"\x1b[{channel};5;{code}m"| .rgb r g b => s!"\x1b[{channel};2;{r};{g};{b}m"def Face.toAnsi (face : Face) : String := Id.run dolet mut parts : Array String := #[]match face.fg with| some color => parts := parts.push (colorToAnsi "38" color)| none => pure ()match face.bg with| some color => parts := parts.push (colorToAnsi "48" color)| none => pure ()if face.bold thenparts := parts.push "\x1b[1m"if face.italic thenparts := parts.push "\x1b[3m"if face.underline thenparts := parts.push "\x1b[4m"return String.intercalate "" parts.toList
import Bliku.Tui.Windowimport Bliku.Tui.Modelnamespace Bliku.Tuistructure SelectionState whereanchor : Cursorcursor : Cursorblock : Bool := falsederiving Repr, Inhabitedstructure CommandLineState whereleader : Stringtext : StringcursorCol : Nat := 0deriving Repr, Inhabitedstructure OverlayView wheretitle : Stringlines : Array StringmaxWidth : Nat := 0cursorRow : Nat := 0cursorCol : Nat := 0deriving Repr, Inhabitedstructure CompletionView whereitems : Array CompletionItemselected : Nat := 0anchorRow : NatanchorCol : Natderiving Repr, Inhabitedstructure WindowChrome wherestatusLine : String := ""deriving Repr, Inhabitedstructure RenderInput whereselection : Option SelectionState := nonecommandLine : Option CommandLineState := nonemessageLine : String := ""statusLine : String := ""overlay : Option OverlayView := nonecompletion : Option CompletionView := nonehideTerminalCursor : Bool := falsederiving Inhabitedend Bliku.Tui
private def collectVisibleCells (line : String) (scrollCol width : Nat) : Array VisibleCell := Id.run dolet mut out : Array VisibleCell := #[]let mut bytePos := 0let mut col := 0for ch in line.toList dolet nextByte := bytePos + ch.utf8Sizeif scrollCol <= col && col < scrollCol + width thenout := out.push {text := ch.toStringcol := colstartByte := bytePosendByte := nextByte}bytePos := nextBytecol := col + 1
private def charDisplayWidth (ch : Char) : Nat :=let n := ch.toNatif(0x1100 <= n && n <= 0x115F) ||(0x2329 <= n && n <= 0x232A) ||(0x2E80 <= n && n <= 0xA4CF) ||(0xAC00 <= n && n <= 0xD7A3) ||(0xF900 <= n && n <= 0xFAFF) ||(0xFE10 <= n && n <= 0xFE19) ||(0xFE30 <= n && n <= 0xFE6F) ||(0xFF00 <= n && n <= 0xFF60) ||(0xFFE0 <= n && n <= 0xFFE6)then 2 else 1private def lineDisplayLength (line : String) : Nat :=line.toList.foldl (fun acc ch => acc + charDisplayWidth ch) 0private def takeDisplayWidth (s : String) (width : Nat) : String := Id.run dolet mut out := ""let mut used := 0for ch in s.toList dolet chWidth := charDisplayWidth chif used + chWidth <= width thenout := out.push chused := used + chWidth
private def lineDisplayLength (line : String) : Nat :=line.toList.length
private def padPlainLine (s : String) (width : Nat) : String :=let clipped := takeDisplayWidth s widthlet clippedWidth := lineDisplayLength clippedlet pad := if clippedWidth < width then "".pushn ' ' (width - clippedWidth) else ""clipped ++ pad
private def getBufferLine (buf : BufferState) (row : Nat) : String :=buf.lines[row]?.getD ""
def renderEmptyLineMarkerInRect (config : UiConfig) (width : Nat) : String :=padPlainLine config.emptyLineMarker widthprivate def renderedWindowLineWidth(line : String) (scrollCol availableWidth : Nat) (windowCursor : Option Cursor) : Nat :=let lineLen := lineDisplayLength linelet visibleLen := if lineLen > scrollCol then min availableWidth (lineLen - scrollCol) else 0match windowCursor with| some cur =>if cur.col >= scrollCol thenlet visCol := cur.col - scrollColif visibleLen <= visCol && visCol < availableWidth thenvisCol + 1elsevisibleLenelsevisibleLen| none => visibleLen
private def isVisualMode (mode : Mode) : Bool :=mode == .visual || mode == .visualBlock
private def byteDecorationsForLine (m : Model) (buf : BufferState) (lineIdx : Nat) (line : String) : Array ByteDecoration :=let palette := syntaxPaletteFor m buf(syntaxSpansForLine buf lineIdx line).foldl (fun acc span =>match Syntax.Palette.faceFor palette span.kind with| some face =>acc.push {row := lineIdxstartByte := span.startByteendByte := span.endBytepriority := 10style := face.toAnsi}| none => acc) #[]
private def isInSelection (m : Model) (cur : Cursor) (row col : Nat) : Bool :=if !isVisualMode m.mode thenfalse
private def isInSelection (selection : SelectionState) (row col : Nat) : Bool :=if selection.block thenlet minRow := min selection.anchor.row selection.cursor.rowlet maxRow := max selection.anchor.row selection.cursor.rowlet minCol := min selection.anchor.col selection.cursor.collet maxCol := max selection.anchor.col selection.cursor.colrow >= minRow && row <= maxRow && col >= minCol && col <= maxCol
match m.selectionStart with| none => false| some start =>if m.mode == .visualBlock thenlet minRow := min start.row cur.rowlet maxRow := max start.row cur.rowlet minCol := min start.col cur.collet maxCol := max start.col cur.colrow >= minRow && row <= maxRow && col >= minCol && col <= maxCol
let (p1, p2) := normalizeCursorRange selection.anchor selection.cursorif row < p1.row || row > p2.row then falseelse if row > p1.row && row < p2.row then trueelse if p1.row == p2.row then col >= p1.col && col <= p2.colelse if row == p1.row then col >= p1.colelse if row == p2.row then col <= p2.colelse falseprivate def selectionDecorationsForLine(config : UiConfig) (selection : Option SelectionState) (lineIdx scrollCol availableWidth : Nat) : Array CellDecoration := Id.run dolet some selection := selection | return #[]let mut startCol : Option Nat := nonelet mut endCol := scrollColfor col in [scrollCol:scrollCol + availableWidth] doif isInSelection selection lineIdx col thenif startCol.isNone thenstartCol := some colendCol := col + 1match startCol with| some start =>#[{row := lineIdxstartCol := startendCol := endColpriority := 100style := config.visualSelectionStyle}]| none => #[]private def cursorDecorationForLine(m : Model) (windowId lineIdx : Nat) (windowCursor : Option Cursor) : Option CursorDecoration :=match windowCursor with| some cur =>if windowId == m.workspace.activeWindowId && lineIdx == cur.row thensome {row := lineIdxcol := cur.colcharStyle := m.config.cursorCharStylespaceStyle := m.config.cursorSpaceStyle}
let (p1, p2) := normalizeCursorRange start curif row < p1.row || row > p2.row then falseelse if row > p1.row && row < p2.row then trueelse if p1.row == p2.row then col >= p1.col && col <= p2.colelse if row == p1.row then col >= p1.colelse if row == p2.row then col <= p2.colelse false
none| none => none
(m : Model) (buf : BufferState) (windowId lineIdx scrollCol availableWidth : Nat)(windowCursor : Option Cursor) : String := Id.run dolet activeRow := windowCursor.map (fun c => c.row) |>.getD 0let activeCol := windowCursor.map (fun c => c.col) |>.getD 0let selectionCur := windowCursor.getD { row := lineIdx, col := scrollCol }
(m : Model) (input : RenderInput) (buf : BufferState) (windowId lineIdx scrollCol availableWidth : Nat)(windowCursor : Option Cursor) : String :=
let visibleCells := collectVisibleCells line scrollCol availableWidthlet syntaxSpans := syntaxSpansForLine buf lineIdx linelet syntaxPalette := syntaxPaletteFor m buflet mut out : Array String := #[]let mut activeStyle : Option String := nonefor cell in visibleCells dolet isCursor :=windowCursor.isSome &&windowId == m.workspace.activeWindowId &&lineIdx == activeRow &&cell.col == activeCollet desiredStyle : Option String :=if isCursor thenif cell.text == " " then some m.config.cursorSpaceStyle else some m.config.cursorCharStyleelse if isInSelection m selectionCur lineIdx cell.col thensome m.config.visualSelectionStyleelse(Syntax.faceForByteRange syntaxPalette syntaxSpans cell.startByte cell.endByte).map Syntax.Face.toAnsiif desiredStyle != activeStyle thenmatch activeStyle with| some _ => out := out.push m.config.resetStyle| none => pure ()match desiredStyle with| some stl => out := out.push stl| none => pure ()activeStyle := desiredStyleout := out.push cell.textif activeStyle.isSome thenout := out.push m.config.resetStylereturn String.intercalate "" out.toList
let props : Bliku.Widget.TextViewProps := {lines := #[line]scrollCol := scrollColbyteDecorations := (byteDecorationsForLine m buf lineIdx line).map (fun deco => { deco with row := 0 })cellDecorations := (selectionDecorationsForLine m.config input.selection lineIdx scrollCol availableWidth).map (fun deco =>{ deco with row := 0 })cursor := (cursorDecorationForLine m windowId lineIdx windowCursor).map (fun deco => { deco with row := 0 })resetStyle := m.config.resetStyle}let styled := Bliku.Widget.renderVisibleLine props 0 availableWidthBliku.Widget.appendCursorOnBlankCell props 0 availableWidth styled
private def appendCursorOnBlankCell(m : Model) (windowId lineIdx scrollCol availableWidth : Nat)(line : String) (lineToDraw : String) (windowCursor : Option Cursor) : String := Id.run dolet some cur := windowCursor | return lineToDrawif windowId != m.workspace.activeWindowId || lineIdx != cur.row || cur.col < scrollCol thenreturn lineToDrawlet visCol := cur.col - scrollCollet visLen := lineDisplayLength line - scrollCol |> min availableWidthif visCol < visLen || visCol >= availableWidth thenreturn lineToDrawlet padCount := visCol - visLenreturn lineToDraw ++ ("".pushn ' ' padCount) ++ m.config.cursorSpaceStyle ++ " " ++ m.config.resetStyle
def renderVisibleLineInRect(m : Model) (input : RenderInput) (buf : BufferState) (windowId lineIdx scrollCol availableWidth : Nat)(windowCursor : Option Cursor) : String :=let line := getBufferLine buf lineIdxlet rendered := renderVisibleLine m input buf windowId lineIdx scrollCol availableWidth windowCursorlet occupied := renderedWindowLineWidth line scrollCol availableWidth windowCursorlet pad := if occupied < availableWidth then "".pushn ' ' (availableWidth - occupied) else ""rendered ++ pad
private def renderWindow (m : Model) (windowId : Nat) (view : ViewState) (rect : Rect) : (Array String × Option (Nat × Nat)) := Id.run do
private def renderWindow (m : Model) (input : RenderInput) (windowId : Nat) (view : ViewState) (rect : Rect) : (Array String × Option (Nat × Nat)) := Id.run do
let line := getBufferLine buf lineIdxlet styled := renderVisibleLine m buf windowId lineIdx view.scrollCol availableWidth windowCursorlet lineToDraw := appendCursorOnBlankCell m windowId lineIdx view.scrollCol availableWidth line styled windowCursorout := out.push lineToDraw
out := out.push (renderVisibleLineInRect m input buf windowId lineIdx view.scrollCol availableWidth windowCursor)
let fileName := buf.filename.getD "[No Name]"let modeStr := if windowId == m.workspace.activeWindowId then s!"-- {m.mode} --" else "--"let eolMark := if buf.missingEol then " [noeol]" else ""let statusStr := s!"{modeStr} {fileName}{eolMark} [W:{windowId} B:{view.bufferId}] [{m.workgroupName}] {m.workspace.name}"
private def renderLayout (m : Model) (l : Layout) (r c h w : Nat) : (Array String × Option (Nat × Nat)) := Id.run do
private def renderLayout (m : Model) (input : RenderInput) (l : Layout) (r c h w : Nat) (skipFloating : Bool := true) : (Array String × Option (Nat × Nat)) := Id.run do
let ids := ws.getFloatingWindowIdsfor i in [0:ids.size] dolet wid := ids[i]!match ws.layout.findView wid, getFloatingWindowBounds ws m.windowHeight m.windowWidth wid with| some view, some (top, left, h, w) =>let (buf, cur) := renderWindow m wid view { row := top, col := left, height := h, width := w }out := out ++ bufif wid == ws.activeWindowId thenactiveCur := cur
let clusters := ws.floatingClustersfor i in [0:clusters.size] dolet cluster := clusters[i]!match ws.layout.extractFloatingRoot cluster.root,computeFloatingClusterBounds m.windowHeight m.windowWidth i cluster with| some subtree, some (baseTop, baseLeft, h, w) =>let toNatNonNeg (v : Int) := if v < 0 then 0 else Int.toNat vlet availableRows := if m.windowHeight > 1 then m.windowHeight - 1 else m.windowHeightlet maxTop := if availableRows > h then availableRows - h else 0let maxLeft := if m.windowWidth > w then m.windowWidth - w else 0let top := min maxTop (toNatNonNeg (Int.ofNat baseTop + cluster.rowOffset))let left := min maxLeft (toNatNonNeg (Int.ofNat baseLeft + cluster.colOffset))let isActive := subtree.getPaneIds.contains ws.activeWindowIdlet chromeBox := Bliku.Widget.renderFloatingChromeBoxcluster.chrome w hm.config.floatingChromeActiveStylem.config.floatingChromeInactiveStylem.config.resetStyleisActiveif !chromeBox.lines.isEmpty thenfor j in [0:chromeBox.lines.size] doout := out.push (moveCursorStr (top + j) left)out := out.push chromeBox.lines[j]!let innerTop := top + chromeBox.insetToplet innerLeft := left + chromeBox.insetLeftlet innerH := h - chromeBox.insetTop - chromeBox.insetBottomlet innerW := w - chromeBox.insetLeft - chromeBox.insetRightif innerH > 0 && innerW > 0 thenlet (buf, cur) := renderLayout m input subtree innerTop innerLeft innerH innerW falseout := out ++ bufif isActive thenactiveCur := cur
if m.mode == .command || m.mode == .searchForward || m.mode == .searchBackward thenbuffer := buffer.push (moveCursorStr (rows - 1) (1 + m.commandBuffer.length))
if let some prompt := input.commandLine thenbuffer := buffer.push (moveCursorStr (rows - 1) (Bliku.Widget.promptCursorCol { leader := prompt.leader, text := prompt.text, cursorCol := prompt.cursorCol }))
match m.mode with| .command => s!":{m.commandBuffer}"| .searchForward => s!"/{m.commandBuffer}"| .searchBackward => s!"?{m.commandBuffer}"| _ => if floatMsg then "" else plain
match input.commandLine with| some cmd => Bliku.Widget.renderPrompt { leader := cmd.leader, text := cmd.text, cursorCol := cmd.cursorCol }| none => if floatMsg then input.statusLine else plain
let lines := if overlay.lines.isEmpty then #[""] else overlay.lineslet titleText := if overlay.title.isEmpty then "" else s!"[{overlay.title}]"let titleRows := if titleText.isEmpty then 0 else 1let naturalWidthContent := lines.foldl (fun acc ln => max acc ln.length) 0let naturalWidth := max naturalWidthContent titleText.length
let box := Bliku.Widget.renderPopupBox { title := overlay.title, lines := overlay.lines, maxWidth := overlay.maxWidth }
let targetWidth := if overlay.maxWidth > 0 then overlay.maxWidth else naturalWidthlet innerWidth := max 1 (min targetWidth maxInnerWidth)let maxContentRows := if availableRows > titleRows + 2 then availableRows - titleRows - 2 else 0
let innerWidth := max 1 (min box.innerWidth maxInnerWidth)let maxContentRows := if availableRows > box.titleRows + 2 then availableRows - box.titleRows - 2 else 0
let lines := if overlay.lines.isEmpty then #[""] else overlay.lineslet titleText := if overlay.title.isEmpty then "" else s!"[{overlay.title}]"let border := "+" ++ "".pushn '-' (layout.innerWidth + 2) ++ "+"
let popup := Bliku.Widget.renderPopupBox { title := overlay.title, lines := overlay.lines, maxWidth := layout.innerWidth }
out := out.push (moveCursorStr layout.top layout.left)out := out.push borderif layout.titleRows == 1 thenout := out.push (moveCursorStr (layout.top + 1) layout.left)let clipped := (titleText.take layout.innerWidth).toStringlet pad := if clipped.length < layout.innerWidth then "".pushn ' ' (layout.innerWidth - clipped.length) else ""out := out.push s!"| {clipped}{pad} |"for i in [0:layout.contentRows] dolet raw := lines[i]?.getD ""let clipped := (raw.take layout.innerWidth).toStringlet pad := if clipped.length < layout.innerWidth then "".pushn ' ' (layout.innerWidth - clipped.length) else ""let row := layout.top + 1 + layout.titleRows + iout := out.push (moveCursorStr row layout.left)out := out.push s!"| {clipped}{pad} |"out := out.push (moveCursorStr (layout.top + layout.contentRows + layout.titleRows + 1) layout.left)out := out.push border
for i in [0:popup.lines.size] doout := out.push (moveCursorStr (layout.top + i) layout.left)out := out.push popup.lines[i]!
def renderCompletionPopup (_rows cols : Nat) (m : Model) (cursorPos : Option (Nat × Nat)) : Array String := Id.run dolet some popup := m.completionPopup | return #[]
def renderCompletionPopup (_rows cols : Nat) (config : UiConfig) (popup : CompletionView) (cursorPos : Option (Nat × Nat)) : Array String := Id.run do
if popup.items.isEmpty then return #[]let visibleMax := min 8 popup.items.sizelet labels := popup.items.extract 0 visibleMax |>.map (fun it => it.label)let naturalW := labels.foldl (fun acc s => max acc s.length) 0let innerWidth := max 8 (min 48 naturalW)let boxWidth := innerWidth + 2
let items := popup.items.map (fun it => Bliku.Widget.ListItem.mk it.label)let borderCh := if config.hSplitStr.isEmpty then '-' else config.hSplitStr.toList[0]!let box := Bliku.Widget.renderListBox {items := itemsselected := popup.selectedmaxVisible := 8borderLeft := config.vSplitStrborderRight := config.vSplitStrborderFill := borderChselectedStyle := "\x1b[7m"resetStyle := config.resetStyle}if box.lines.isEmpty thenreturn #[]
let left := if cursorCol + boxWidth < cols then cursorCol else (cols - boxWidth)let borderCh := if m.config.hSplitStr.isEmpty then '-' else m.config.hSplitStr.toList[0]!let hline := "".pushn borderCh innerWidthlet border := m.config.vSplitStr ++ hline ++ m.config.vSplitStr
let left := if cursorCol + box.width < cols then cursorCol else (cols - box.width)
out := out.push (moveCursorStr top left)out := out.push borderlet selected := if popup.selected < visibleMax then popup.selected else 0for i in [0:visibleMax] dolet label := (labels[i]!.take innerWidth).toStringlet pad := if label.length < innerWidth then "".pushn ' ' (innerWidth - label.length) else ""out := out.push (moveCursorStr (top + 1 + i) left)out := out.push m.config.vSplitStrif i == selected thenout := out.push "\x1b[7m"out := out.push labelout := out.push padout := out.push m.config.resetStyleelseout := out.push labelout := out.push padout := out.push m.config.vSplitStrout := out.push (moveCursorStr (top + visibleMax + 1) left)out := out.push border
for i in [0:box.lines.size] doout := out.push (moveCursorStr (top + i) left)out := out.push box.lines[i]!
inductive Mode where| normal| insert| command| searchForward| searchBackward| visual| visualBlockderiving Repr, BEq, Inhabitedinstance : ToString Mode wheretoString| .normal => "NORMAL"| .insert => "INSERT"| .command => "COMMAND"| .searchForward => "SEARCH"| .searchBackward => "SEARCH"| .visual => "VISUAL"| .visualBlock => "VISUAL BLOCK"
namespace Blikuinductive Color where| ansi (code : Nat)| rgb (r g b : Nat)deriving Repr, BEq, Inhabitedstructure Face wherefg : Option Color := nonebg : Option Color := nonebold : Bool := falseitalic : Bool := falseunderline : Bool := falsederiving Repr, BEq, Inhabitedstructure Theme wherefaces : List (String × Face) := []deriving Repr, BEq, Inhabitedprivate def colorToAnsi (channel : String) : Color → String| .ansi code => s!"\x1b[{channel};5;{code}m"| .rgb r g b => s!"\x1b[{channel};2;{r};{g};{b}m"def Face.toAnsi (face : Face) : String := Id.run dolet mut parts : Array String := #[]match face.fg with| some color => parts := parts.push (colorToAnsi "38" color)| none => pure ()match face.bg with| some color => parts := parts.push (colorToAnsi "48" color)| none => pure ()if face.bold thenparts := parts.push "\x1b[1m"if face.italic thenparts := parts.push "\x1b[3m"if face.underline thenparts := parts.push "\x1b[4m"return String.intercalate "" parts.toListend Bliku
namespace Blikustructure Cursor whererow : Natcol : Natderiving Repr, BEq, Inhabitedstructure PaneView wherecontentId : Natcursor : CursorscrollRow : NatscrollCol : Natderiving Repr, Inhabitedinductive FloatingRootRef where| pane (id : Nat)| group (id : Nat)deriving Repr, BEq, Inhabitedinductive FloatingAxisSize where| auto| fixed (value : Nat)| ratio (value : Float)deriving Repr, BEq, Inhabitedstructure FloatingSizeSpec wherewidth : FloatingAxisSize := .autoheight : FloatingAxisSize := .autominWidth : Option Nat := noneminHeight : Option Nat := nonemaxWidth : Option Nat := nonemaxHeight : Option Nat := nonederiving Repr, BEq, Inhabitedinductive FloatingSizePolicy where| default| multiPane| custom (spec : FloatingSizeSpec)deriving Repr, BEq, Inhabitedinductive FloatingChromeKind where| none| borderedderiving Repr, BEq, Inhabitedstructure FloatingChrome wherekind : FloatingChromeKind := .nonetitle : Option String := nonederiving Repr, BEq, Inhabitedinductive PaneLayout where| pane (id : Nat) (view : PaneView)| group (id : Nat) (body : PaneLayout)| hsplit (left right : PaneLayout) (ratio : Float)| vsplit (top bottom : PaneLayout) (ratio : Float)deriving Repr, Inhabitedstructure FloatingCluster whereroot : FloatingRootRefrowOffset : Int := 0colOffset : Int := 0sizePolicy : FloatingSizePolicy := .defaultchrome : FloatingChrome := {}deriving Repr, BEq, Inhabitedstructure FloatingPaneState whereclusters : Array FloatingCluster := #[]deriving Inhabitedstructure DesktopLayout wherelayout : PaneLayoutactivePaneId : Natfloating : FloatingPaneState := {}deriving Inhabiteddef PaneLayout.findView (l : PaneLayout) (id : Nat) : Option PaneView :=match l with| .pane wid v => if wid == id then some v else none| .group _ body => body.findView id| .hsplit left right _ => (left.findView id).orElse (fun _ => right.findView id)| .vsplit top bottom _ => (top.findView id).orElse (fun _ => bottom.findView id)def PaneLayout.updateView (l : PaneLayout) (id : Nat) (f : PaneView → PaneView) : PaneLayout :=let rec go (node : PaneLayout) : PaneLayout × Bool :=match node with| .pane wid v =>if wid == id then (.pane wid (f v), true) else (node, false)| .group gid body =>let (body', found) := go body(.group gid body', found)| .hsplit left right ratio =>let (left', foundLeft) := go leftif foundLeft then(.hsplit left' right ratio, true)elselet (right', foundRight) := go right(.hsplit left' right' ratio, foundRight)| .vsplit top bottom ratio =>let (top', foundTop) := go topif foundTop then(.vsplit top' bottom ratio, true)elselet (bottom', foundBottom) := go bottom(.vsplit top' bottom' ratio, foundBottom)(go l).1def PaneLayout.remove (l : PaneLayout) (id : Nat) : Option PaneLayout :=match l with| .pane wid _ => if wid == id then none else some l| .group gid body =>if gid == id thennoneelsebody.remove id |>.map (PaneLayout.group gid)| .hsplit left right ratio =>match left.remove id with| none => some right| some left' =>match right.remove id with| none => some left'| some right' => some (.hsplit left' right' ratio)| .vsplit top bottom ratio =>match top.remove id with| none => some bottom| some top' =>match bottom.remove id with| none => some top'| some bottom' => some (.vsplit top' bottom' ratio)def PaneLayout.getPaneIds (l : PaneLayout) : List Nat :=match l with| .pane id _ => [id]| .group _ body => body.getPaneIds| .hsplit left right _ => left.getPaneIds ++ right.getPaneIds| .vsplit top bottom _ => top.getPaneIds ++ bottom.getPaneIdsdef PaneLayout.containsFloatingRoot (l : PaneLayout) (root : FloatingRootRef) : Bool :=match l, root with| .pane id _, .pane target => id == target| .group id _, .group target => id == target| .group _ body, root => body.containsFloatingRoot root| .hsplit left right _, root => left.containsFloatingRoot root || right.containsFloatingRoot root| .vsplit top bottom _, root => top.containsFloatingRoot root || bottom.containsFloatingRoot root| _, _ => falsedef PaneLayout.extractFloatingRoot (l : PaneLayout) (root : FloatingRootRef) : Option PaneLayout :=match l, root with| .pane id _, .pane target => if id == target then some l else none| .group id _, .group target => if id == target then some l else none| .group _ body, root => body.extractFloatingRoot root| .hsplit left right _, root => (left.extractFloatingRoot root).orElse (fun _ => right.extractFloatingRoot root)| .vsplit top bottom _, root => (top.extractFloatingRoot root).orElse (fun _ => bottom.extractFloatingRoot root)| _, _ => nonedef PaneLayout.removeFloatingRoot (l : PaneLayout) (root : FloatingRootRef) : Option PaneLayout :=match l, root with| .pane id _, .pane target => if id == target then none else some l| .group id _, .group target => if id == target then none else some l| .group gid body, root =>body.removeFloatingRoot root |>.map (PaneLayout.group gid)| .hsplit left right ratio, root =>match left.removeFloatingRoot root with| none => some right| some left' =>match right.removeFloatingRoot root with| none => some left'| some right' => some (.hsplit left' right' ratio)| .vsplit top bottom ratio, root =>match top.removeFloatingRoot root with| none => some bottom| some top' =>match bottom.removeFloatingRoot root with| none => some top'| some bottom' => some (.vsplit top' bottom' ratio)| _, _ => some ldef PaneLayout.getAllPaneBounds (l : PaneLayout) (h w : Nat) : List (Nat × Nat × Nat × Nat × Nat) :=let rec traverse (node : PaneLayout) (r c h w : Nat) (acc : List (Nat × Nat × Nat × Nat × Nat)) :=match node with| .pane id _ => (id, r, c, h, w) :: acc| .group _ body => traverse body r c h w acc| .hsplit left right ratio =>let leftW := (Float.ofNat w * ratio).toUInt64.toNatlet acc' := traverse left r c h leftW acctraverse right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0) acc'| .vsplit top bottom ratio =>let topH := (Float.ofNat h * ratio).toUInt64.toNatlet acc' := traverse top r c topH w acctraverse bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w acc'traverse l 0 0 h w []private def clampSize (value fallback minValue maxValue : Nat) : Nat :=max minValue (min maxValue (if value == 0 then fallback else value))private def resolveAxisSize (available fallback minValue maxValue : Nat) : FloatingAxisSize → Nat| .auto => clampSize fallback fallback minValue maxValue| .fixed value => clampSize value fallback minValue maxValue| .ratio ratio =>let value := (Float.ofNat available * ratio).toUInt64.toNatclampSize value fallback minValue maxValueprivate def defaultFloatingSizeSpec : FloatingSizeSpec :={width := .ratio 0.6height := .ratio 0.6minWidth := some 24minHeight := some 8}private def multiPaneFloatingSizeSpec : FloatingSizeSpec :={width := .ratio 0.8height := .ratio 0.7minWidth := some 60minHeight := some 16}private def sizeSpecForPolicy : FloatingSizePolicy → FloatingSizeSpec| .default => defaultFloatingSizeSpec| .multiPane => multiPaneFloatingSizeSpec| .custom spec => specdef computeFloatingClusterBounds (rows cols idx : Nat) (cluster : FloatingCluster) : Option (Nat × Nat × Nat × Nat) :=let availableRows := if rows > 1 then rows - 1 else rowsif availableRows < 6 || cols < 16 thennoneelselet spec := sizeSpecForPolicy cluster.sizePolicylet hMax := availableRows - 2let wMax := cols - 4let defaultH := max 8 ((availableRows * 3) / 5)let defaultW := max 24 ((cols * 3) / 5)let minH := spec.minHeight.getD 1let minW := spec.minWidth.getD 1let maxH := spec.maxHeight.map (min hMax) |>.getD hMaxlet maxW := spec.maxWidth.map (min wMax) |>.getD wMaxlet h := resolveAxisSize availableRows defaultH minH maxH spec.heightlet w := resolveAxisSize cols defaultW minW maxW spec.widthlet topBase := (availableRows - h) / 2let leftBase := (cols - w) / 2let top := min (availableRows - h) (topBase + idx)let left := min (cols - w) (leftBase + (2 * idx))some (top, left, h, w)def FloatingPaneState.getClusters (layout : PaneLayout) (floating : FloatingPaneState) : Array FloatingCluster :=floating.clusters.foldl (fun acc cluster =>if layout.containsFloatingRoot cluster.root then acc.push cluster else acc) #[]def FloatingPaneState.clusterForPane? (layout : PaneLayout) (floating : FloatingPaneState) (paneId : Nat) : Option FloatingCluster :=let clusters := floating.getClusters layoutlet rec loop (i : Nat) : Option FloatingCluster :=if i >= clusters.size thennoneelselet cluster := clusters[i]!match layout.extractFloatingRoot cluster.root with| some subtree =>if subtree.getPaneIds.contains paneId then some cluster else loop (i + 1)| none => loop (i + 1)loop 0end Bliku
import Bliku.Stylenamespace Blikustructure ByteDecoration whererow : NatstartByte : NatendByte : Natpriority : Nat := 0style : Stringderiving Repr, BEq, Inhabitedstructure CellDecoration whererow : NatstartCol : NatendCol : Natpriority : Nat := 0style : Stringderiving Repr, BEq, Inhabitedstructure CursorDecoration whererow : Natcol : NatcharStyle : StringspaceStyle : Stringpriority : Nat := 1000deriving Repr, BEq, Inhabitedend Bliku