4kusto/vie - Change FAVK3BZP62D4KKDVNGX323UOVRPCW2NFLAHTVYBGQHRJSDI24XCQC

Split Bliku out of ViE as an independent TUI packagew

Created by 4kusto on March 6, 2026

FAVK3BZP62D4KKDVNGX323UOVRPCW2NFLAHTVYBGQHRJSDI24XCQC

Dependencies

In channels

main

Change contents

File deletion: lakefile.toml
BF:BFD[3.1] → [4.66:103]
BF:BFD[4.103] → [4.104:104]
B:BD[4.104] → [4.105:161]
∅:D[5.20] → [4.161:188]
B:BD[4.161] → [4.161:188]
∅:D[6.28] → [4.188:229]
B:BD[4.188] → [4.188:229]
B:BD[4.229] → [6.29:71]
B:BD[6.71] → [7.1245:1298]
B:BD[4.188] → [6.0:28]
B:BD[4.161] → [8.0:22]
∅:D[8.22] → [5.0:20]
B:BD[4.161] → [5.0:20]
```
name = "vie"
version = "0.1.0"
defaultTargets = ["vie"]
[[lean_lib]]
name = "ViE"
[[lean_exe]]
name = "vie"
root = "Main"
[[lean_exe]]
name = "test"
root = "Test"
[[lean_exe]]
name = "bench"
root = "Test.Benchmark"
[[lean_lib]]
name = "Test"
buildType = "release"
testDriver = "test"
```

Replacement in lake-manifest.json at line 3 [4.273]

B:BD[4.329] → [4.329:365]

 "packages": [],
 "name": "editor",

[4.329]

[4.365]

 "packages":
 [{"url": "https://github.com/4kusto/bliku",
   "type": "git",
   "subDir": null,
   "scope": "",
   "rev": "2836947f0090b29b45b4f012db0a274fb2ac8aee",
   "name": "bliku",
   "manifestFile": "lake-manifest.json",
   "inputRev": null,
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "vie",

Insertion in ViE/UI/Syntax.lean at line 4 [9.2903]
[2.109]
[9.2942]
```
import Bliku.Tui.Syntax
```

Replacement in ViE/UI/Syntax.lean at line 8 [9.2903]

B:BD[9.8803] → [9.8803:8935]

B:BD[9.8935] → [2.110:190]

def highlightLine (filename : Option String) (line : String) : Array Span :=
  match detectLanguage filename with
  | .plain => #[]
  | .lean => highlightLeanLine line
  | .markdown => highlightMarkdownLine line

[9.8803]

[9.9348]

abbrev highlightLine := Bliku.Tui.Syntax.highlightLine

Replacement in ViE/UI/Syntax/Types.lean at line 1 [2.246]
B:BD[2.246] → [2.247:285]
```
import ViE.Color
import ViE.UI.Search
```
[2.246]
[2.285]
```
import Bliku.Tui.Syntax.Types
```

Replacement in ViE/UI/Syntax/Types.lean at line 5 [2.246]

B:BD[2.311] → [2.311:400]

inductive Language where
  | plain
  | lean
  | markdown
  deriving Repr, BEq, Inhabited

[2.311]

[2.400]

abbrev Language := Bliku.Tui.Syntax.Language
abbrev Span := Bliku.Tui.Syntax.Span

Replacement in ViE/UI/Syntax/Types.lean at line 8 [2.246]

B:BD[2.401] → [2.401:505]

structure Span where
  startByte : Nat
  endByte : Nat
  style : String
  deriving Repr, BEq, Inhabited

[2.401]

[2.505]

abbrev leanKeywordStyle := Bliku.Tui.Syntax.leanKeywordStyle
abbrev leanCommentStyle := Bliku.Tui.Syntax.leanCommentStyle
abbrev leanStringStyle := Bliku.Tui.Syntax.leanStringStyle
abbrev leanNumberStyle := Bliku.Tui.Syntax.leanNumberStyle

Replacement in ViE/UI/Syntax/Types.lean at line 13 [2.246]

B:BD[2.506] → [2.506:809]

def leanKeywordStyle : String := ViE.Color.toFg ViE.Color.Color.brightBlue
def leanCommentStyle : String := ViE.Color.toFg ViE.Color.Color.brightBlack
def leanStringStyle : String := ViE.Color.toFg ViE.Color.Color.brightGreen
def leanNumberStyle : String := ViE.Color.toFg ViE.Color.Color.brightMagenta

[2.506]

[2.809]

abbrev markdownHeadingStyle := Bliku.Tui.Syntax.markdownHeadingStyle
abbrev markdownCodeStyle := Bliku.Tui.Syntax.markdownCodeStyle
abbrev markdownLinkStyle := Bliku.Tui.Syntax.markdownLinkStyle
abbrev markdownEmphasisStyle := Bliku.Tui.Syntax.markdownEmphasisStyle

Replacement in ViE/UI/Syntax/Types.lean at line 18 [2.246]

B:BD[2.810] → [2.810:1733]

def markdownHeadingStyle : String := ViE.Color.toFg ViE.Color.Color.brightCyan
def markdownCodeStyle : String := ViE.Color.toFg ViE.Color.Color.brightYellow
def markdownLinkStyle : String := ViE.Color.toFg ViE.Color.Color.brightBlue
def markdownEmphasisStyle : String := ViE.Color.toFg ViE.Color.Color.brightMagenta
def detectLanguage (filename : Option String) : Language :=
  match filename with
  | none => .plain
  | some name =>
      if name.endsWith ".lean" then .lean
      else if name.endsWith ".md" || name.endsWith ".markdown" then .markdown
      else .plain
def styleForByteRange (spans : Array Span) (byteStart byteEnd : Nat) : Option String :=
  let rec loop (i : Nat) : Option String :=
    if i >= spans.size then
      none
    else
      let s := spans[i]!
      if ViE.UI.overlapsByteRange (s.startByte, s.endByte) byteStart byteEnd then
        some s.style
      else
        loop (i + 1)
  loop 0

[2.810]

[2.1733]

abbrev detectLanguage := Bliku.Tui.Syntax.detectLanguage
abbrev styleForByteRange := Bliku.Tui.Syntax.styleForByteRange

Insertion in ViE/UI/Syntax/Markdown.lean at line 2 [2.1791]
[2.1819]
[2.1819]
```
import Bliku.Tui.Syntax.Markdown
```

Replacement in ViE/UI/Syntax/Markdown.lean at line 6 [2.1791]

B:BD[2.1845] → [2.1845:3924]

private def isMarkdownHeading (bytes : ByteArray) : Bool := Id.run do
  let n := bytes.size
  let mut i := 0
  while i < n && bytes[i]! == 32 do
    i := i + 1
  if i >= n || bytes[i]! != 35 then
    return false
  let mut j := i
  while j < n && bytes[j]! == 35 do
    j := j + 1
  return j < n && bytes[j]! == 32
private def isMarkdownFence (bytes : ByteArray) : Bool :=
  (bytes.size >= 3 && bytes[0]! == 96 && bytes[1]! == 96 && bytes[2]! == 96) ||
  (bytes.size >= 3 && bytes[0]! == 126 && bytes[1]! == 126 && bytes[2]! == 126)
def highlightMarkdownLine (line : String) : Array Span := Id.run do
  let bytes := line.toUTF8
  let n := bytes.size
  if isMarkdownHeading bytes then
    return #[{ startByte := 0, endByte := n, style := markdownHeadingStyle }]
  if isMarkdownFence bytes then
    return #[{ startByte := 0, endByte := n, style := markdownCodeStyle }]
  let mut spans : Array Span := #[]
  let mut i := 0
  while i < n do
    if bytes[i]! == 96 then
      let mut j := i + 1
      while j < n && bytes[j]! != 96 do
        j := j + 1
      if j < n then
        spans := spans.push { startByte := i, endByte := j + 1, style := markdownCodeStyle }
        i := j + 1
      else
        i := i + 1
    else if bytes[i]! == 91 then
      let mut j := i + 1
      while j < n && bytes[j]! != 93 do
        j := j + 1
      if j + 1 < n && bytes[j]! == 93 && bytes[j + 1]! == 40 then
        let mut k := j + 2
        while k < n && bytes[k]! != 41 do
          k := k + 1
        if k < n then
          spans := spans.push { startByte := i, endByte := k + 1, style := markdownLinkStyle }
          i := k + 1
        else
          i := i + 1
      else
        i := i + 1
    else if bytes[i]! == 42 || bytes[i]! == 95 then
      let delim := bytes[i]!
      let mut j := i + 1
      while j < n && bytes[j]! != delim do
        j := j + 1
      if j < n && j > i + 1 then
        spans := spans.push { startByte := i, endByte := j + 1, style := markdownEmphasisStyle }
        i := j + 1
      else
        i := i + 1
    else
      i := i + 1
  return spans

[2.1845]

[2.3924]

abbrev highlightMarkdownLine := Bliku.Tui.Syntax.highlightMarkdownLine

Insertion in ViE/UI/Syntax/Lean.lean at line 2 [2.3978]
[2.4006]
[2.4006]
```
import Bliku.Tui.Syntax.Lean
```

Deletion in ViE/UI/Syntax/Lean.lean at line 5 [2.3978]

B:BD[2.4031] → [2.4031:4860]


private def isAsciiLower (n : Nat) : Bool := 97 <= n && n <= 122
private def isAsciiUpper (n : Nat) : Bool := 65 <= n && n <= 90
private def isAsciiDigit (n : Nat) : Bool := 48 <= n && n <= 57
private def isIdentStart (b : UInt8) : Bool :=
  let n := b.toNat
  isAsciiLower n || isAsciiUpper n || n == 95
private def isIdentCont (b : UInt8) : Bool :=
  let n := b.toNat
  isIdentStart b || isAsciiDigit n || n == 39
private def leanKeywords : Array String := #[
  "abbrev", "axiom", "by", "class", "constant", "def", "deriving", "do",
  "else", "end", "example", "from", "have", "if", "import", "in", "inductive",
  "instance", "let", "match", "mutual", "namespace", "open", "opaque", "private",
  "protected", "set_option", "show", "structure", "syntax", "termination_by",
  "theorem", "unsafe", "variable", "where", "with"
]

Replacement in ViE/UI/Syntax/Lean.lean at line 6 [2.3978]

B:BD[2.4861] → [2.4861:5027]

def highlightLeanLine (line : String) : Array Span := Id.run do
  let bytes := line.toUTF8
  let n := bytes.size
  let mut spans : Array Span := #[]
  let mut i := 0

[2.4861]

[2.5027]

abbrev highlightLeanLine := Bliku.Tui.Syntax.highlightLeanLine

Deletion in ViE/UI/Syntax/Lean.lean at line 8 [2.3978]

B:BD[2.5028] → [2.5028:6698]

  while i < n do
    let b := bytes[i]!
    if b == 34 then
      let mut j := i + 1
      let mut escaped := false
      let mut closed := false
      while j < n && !closed do
        let c := bytes[j]!
        if escaped then
          escaped := false
          j := j + 1
        else if c == 92 then
          escaped := true
          j := j + 1
        else if c == 34 then
          closed := true
          j := j + 1
        else
          j := j + 1
      spans := spans.push { startByte := i, endByte := j, style := leanStringStyle }
      i := j
    else if i + 1 < n && bytes[i]! == 45 && bytes[i + 1]! == 45 then
      spans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }
      i := n
    else if i + 1 < n && bytes[i]! == 47 && bytes[i + 1]! == 45 then
      spans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }
      i := n
    else if isAsciiDigit b.toNat then
      let mut j := i + 1
      while j < n do
        let c := bytes[j]!.toNat
        if isAsciiDigit c || c == 95 || c == 46 || c == 120 || c == 111 || c == 98 ||
           (65 <= c && c <= 70) || (97 <= c && c <= 102) then
          j := j + 1
        else
          break
      spans := spans.push { startByte := i, endByte := j, style := leanNumberStyle }
      i := j
    else if isIdentStart b then
      let mut j := i + 1
      while j < n && isIdentCont (bytes[j]!) do
        j := j + 1
      let tok := String.fromUTF8! (bytes.extract i j)
      if leanKeywords.contains tok then
        spans := spans.push { startByte := i, endByte := j, style := leanKeywordStyle }
      i := j
    else
      i := i + 1
  return spans

Insertion in ViE/UI/Search.lean at line 2 [10.13324]
[10.13350]
[10.13350]
```
import Bliku.Tui.Search
```

Replacement in ViE/UI/Search.lean at line 7 [10.13324]

B:BD[10.13378] → [10.13378:13445]

B:BD[10.13445] → [11.0:102]

∅:D[11.102] → [10.13545:13619]

B:BD[10.13545] → [10.13545:13619]

B:BD[10.13619] → [11.103:118]

/-- Find all occurrences of a byte pattern within a byte array. -/
def findAllMatchesBytes (haystack : ByteArray) (needle : ByteArray) : Array (Nat × Nat) := Id.run do
  let n := needle.size
  let h := haystack.size
  if n == 0 || h < n then
    return #[]

[10.13378]

[11.118]

abbrev findAllMatchesBytes := Bliku.Tui.findAllMatchesBytes
abbrev overlapsByteRange := Bliku.Tui.overlapsByteRange
abbrev activeMatchRange := Bliku.Tui.activeMatchRange

Deletion in ViE/UI/Search.lean at line 11 [10.13324]

B:BD[11.119] → [11.119:407]

∅:D[11.407] → [10.14014:14587]

B:BD[10.14014] → [10.14014:14587]

  let limit := h - n + 1
  let mut out : Array (Nat × Nat) := #[]
  for i in [0:limit] do
    let mut matched := true
    for j in [0:n] do
      if matched && haystack[i + j]! != needle[j]! then
        matched := false
    if matched then
      out := out.push (i, i + n)
  return out
def overlapsByteRange (r : Nat × Nat) (byteStart byteEnd : Nat) : Bool :=
  let (s, e) := r
  byteStart < e && byteEnd > s
def activeMatchRange (hitRanges : Array (Nat × Nat)) (cursorByte : Option Nat) : Option (Nat × Nat) :=
  match cursorByte with
  | none => none
  | some cb =>
      let rec loop (i : Nat) : Option (Nat × Nat) :=
        if i >= hitRanges.size then
          none
        else
          let m := hitRanges[i]!
          let (s, e) := m
          if s <= cb && cb < e then
            some m
          else
            loop (i + 1)
      loop 0

Insertion in ViE/UI/Primitives.lean at line 3 [10.25098]
[10.25135]
[10.25135]
```
import Bliku.Tui.Primitives
```

Replacement in ViE/UI/Primitives.lean at line 8 [10.25098]

B:BD[10.25163] → [10.25163:25366]

B:BD[10.25540] → [10.25540:25541]

B:BD[10.25701] → [10.25701:25796]

/-- Pad a string on the left with spaces until it reaches the given width. -/
def leftPad (s : String) (width : Nat) : String :=
  if s.length >= width then s
  else "".pushn ' ' (width - s.length) ++ s
structure Rect where
  row : Nat
  col : Nat
  height : Nat
  width : Nat
  deriving Inhabited

[10.25163]

[10.25796]

abbrev leftPad := Bliku.Tui.leftPad
abbrev Rect := Bliku.Tui.Rect

Insertion in ViE/Types.lean at line 126 [4.22248]

[12.6751]

[13.8660]

  visualSelectionStyle : String
  cursorCharStyle : String
  cursorSpaceStyle : String

Insertion in ViE/State/Config.lean at line 27 [4.53268]

[12.23045]

[13.18751]

  visualSelectionStyle := "\x1b[7m"
  cursorCharStyle := (ViE.Color.toBg .white) ++ (ViE.Color.toFg .black)
  cursorSpaceStyle := (ViE.Color.toBg .white) ++ (ViE.Color.toFg .black)

Replacement in ViE/App.lean at line 5 [4.125244]
B:BD[4.125299] → [4.125299:125313]
```
import ViE.UI
```
[4.125299]
[4.125313]
```
import Bliku.Tui
import ViE.BlikuAdapter
```
Replacement in ViE/App.lean at line 121 [4.125244]
B:BD[11.36797] → [11.36797:36823]
```
      ViE.UI.render state
```
[11.36797]
[4.126317]
```
      ViE.BlikuAdapter.render state
```

Split Bliku out of ViE as an independent TUI packagew

Dependencies

In channels

Change contents

File deletion: lakefile.toml

Replacement in lake-manifest.json at line 3 [4.273]

Insertion in ViE/UI/Syntax.lean at line 4 [9.2903]

Replacement in ViE/UI/Syntax.lean at line 8 [9.2903]

Replacement in ViE/UI/Syntax/Types.lean at line 1 [2.246]

Replacement in ViE/UI/Syntax/Types.lean at line 5 [2.246]

Replacement in ViE/UI/Syntax/Types.lean at line 8 [2.246]

Replacement in ViE/UI/Syntax/Types.lean at line 13 [2.246]

Replacement in ViE/UI/Syntax/Types.lean at line 18 [2.246]

Insertion in ViE/UI/Syntax/Markdown.lean at line 2 [2.1791]

Replacement in ViE/UI/Syntax/Markdown.lean at line 6 [2.1791]

Insertion in ViE/UI/Syntax/Lean.lean at line 2 [2.3978]

Deletion in ViE/UI/Syntax/Lean.lean at line 5 [2.3978]

Replacement in ViE/UI/Syntax/Lean.lean at line 6 [2.3978]

Deletion in ViE/UI/Syntax/Lean.lean at line 8 [2.3978]

Insertion in ViE/UI/Search.lean at line 2 [10.13324]

Replacement in ViE/UI/Search.lean at line 7 [10.13324]

Deletion in ViE/UI/Search.lean at line 11 [10.13324]

Insertion in ViE/UI/Primitives.lean at line 3 [10.25098]

Replacement in ViE/UI/Primitives.lean at line 8 [10.25098]

Insertion in ViE/Types.lean at line 126 [4.22248]

Insertion in ViE/State/Config.lean at line 27 [4.53268]

Replacement in ViE/App.lean at line 5 [4.125244]

Replacement in ViE/App.lean at line 121 [4.125244]