4kusto/bliku - Change RUDXLEMLJLTDEPQVWE72AQRMMMLUX33XOTUKZKQTUOM2QELLIQAQC

Add UTF-8-safe renderer syntax highlighting with generic token kinds

Created by 4kusto on March 6, 2026

RUDXLEMLJLTDEPQVWE72AQRMMMLUX33XOTUKZKQTUOM2QELLIQAQC

Dependencies

In channels

main

Change contents

Insertion in lakefile.lean at line 7 [2.104]
[2.162]
```
lean_exe bliku_test where
  root := `BlikuTest
```

File addition: BlikuTest.lean (----------)

[3.1]

import Bliku
open Bliku.Tui
private def mkWorkspace : WorkspaceView :=
  {
    name := "test"
    layout := .window 0 { bufferId := 0, cursor := { row := 0, col := 0 }, scrollRow := 0, scrollCol := 0 }
    activeWindowId := 0
  }
private def mkModel (mode : Mode := .normal) (selectionStart : Option Cursor := none) : Model :=
  {
    mode := mode
    workgroupName := "wg"
    workspace := mkWorkspace
    buffers := #[]
    selectionStart := selectionStart
    message := ""
    commandBuffer := ""
    config := {
      resetStyle := "[/]"
      visualSelectionStyle := "[SEL]"
      cursorCharStyle := "[CUR]"
      cursorSpaceStyle := "[CUR]"
    }
  }
private def assertEq [ToString α] [BEq α] (name : String) (actual expected : α) : IO Unit := do
  if actual != expected then
    throw <| IO.userError s!"{name} failed\nexpected: {expected}\nactual:   {actual}"
private def utf8ByteOffsetTest : IO Unit := do
  let buf : BufferState :=
    {
      id := 0
      filename := none
      lines := #["あdef"]
      syntaxState := {
        lineSpans := #[(0, #[{ startByte := 3, endByte := 6, kind := .custom "test" }])]
        paletteOverrides := { custom := [("test", { fg := some (.ansi 196) })] }
      }
    }
  let rendered := renderVisibleLine (mkModel) buf 0 0 0 4 (some { row := 1, col := 0 })
  assertEq "utf8-byte-offset" rendered "あ\x1b[38;5;196mdef[/]"
private def builtinLeanHighlightTest : IO Unit := do
  let buf : BufferState :=
    {
      id := 0
      filename := some "Main.lean"
      lines := #["def あ := 1"]
    }
  let rendered := renderVisibleLine (mkModel) buf 0 0 0 20 none
  assertEq "builtin-lean-highlight" rendered "\x1b[38;5;12mdef[/] あ := \x1b[38;5;13m1[/]"
private def cursorSelectionPriorityTest : IO Unit := do
  let model := mkModel .visual (some { row := 0, col := 0 })
  let buf : BufferState :=
    {
      id := 0
      filename := none
      lines := #["abc"]
      syntaxState := {
        lineSpans := #[(0, #[{ startByte := 0, endByte := 3, kind := .custom "test" }])]
        paletteOverrides := { custom := [("test", { fg := some (.ansi 46) })] }
      }
    }
  let rendered := renderVisibleLine model buf 0 0 0 3 (some { row := 0, col := 1 })
  assertEq "cursor-selection-priority" rendered "[SEL]a[/][CUR]b[/]\x1b[38;5;46mc[/]"
def main : IO Unit := do
  utf8ByteOffsetTest
  builtinLeanHighlightTest
  cursorSelectionPriorityTest
  IO.println "bliku-test: ok"

Insertion in Bliku/Tui/Syntax/Types.lean at line 9 [2.8034]

[2.8145]

  deriving Repr, BEq, Inhabited
inductive Color where
  | ansi (code : Nat)
  | rgb (r g b : Nat)
  deriving Repr, BEq, Inhabited
structure Face where
  fg : Option Color := none
  bg : Option Color := none
  bold : Bool := false
  italic : Bool := false
  underline : Bool := false

Insertion in Bliku/Tui/Syntax/Types.lean at line 24 [2.8034]

[2.8178]

inductive HighlightKind where
  | keyword
  | comment
  | stringLiteral
  | numberLiteral
  | heading
  | code
  | link
  | emphasis
  | custom (name : String)
  deriving Repr, BEq, Inhabited
structure LanguageProfile where
  language : Language
  supportedKinds : Array HighlightKind := #[]
  deriving Repr, BEq, Inhabited

Replacement in Bliku/Tui/Syntax/Types.lean at line 44 [2.8034]

B:BD[2.8233] → [2.8233:8250]

  style : String

[2.8233]

[2.8250]

  kind : HighlightKind
  deriving Repr, BEq, Inhabited
structure Palette where
  keyword : Option Face := none
  comment : Option Face := none
  stringLiteral : Option Face := none
  numberLiteral : Option Face := none
  heading : Option Face := none
  code : Option Face := none
  link : Option Face := none
  emphasis : Option Face := none
  custom : List (String × Face) := []

Replacement in Bliku/Tui/Syntax/Types.lean at line 59 [2.8034]

B:BD[2.8283] → [2.8283:8480]

-- ANSI bright colors.
def leanKeywordStyle : String := "\x1b[94m"
def leanCommentStyle : String := "\x1b[90m"
def leanStringStyle : String := "\x1b[92m"
def leanNumberStyle : String := "\x1b[95m"

[2.8283]

[2.8480]

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"

Replacement in Bliku/Tui/Syntax/Types.lean at line 63 [2.8034]

B:BD[2.8481] → [2.8481:8668]

def markdownHeadingStyle : String := "\x1b[96m"
def markdownCodeStyle : String := "\x1b[93m"
def markdownLinkStyle : String := "\x1b[94m"
def markdownEmphasisStyle : String := "\x1b[95m"

[2.8481]

[2.8668]

def Face.toAnsi (face : Face) : String := Id.run do
  let 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 then
    parts := parts.push "\x1b[1m"
  if face.italic then
    parts := parts.push "\x1b[3m"
  if face.underline then
    parts := parts.push "\x1b[4m"
  return String.intercalate "" parts.toList
private def mergeFace (base : Option Face) (override : Option Face) : Option Face :=
  match base, override with
  | none, none => none
  | some face, none => some face
  | none, some face => some face
  | some baseFace, some overrideFace =>
      some {
        fg := overrideFace.fg.orElse (fun _ => baseFace.fg)
        bg := overrideFace.bg.orElse (fun _ => baseFace.bg)
        bold := baseFace.bold || overrideFace.bold
        italic := baseFace.italic || overrideFace.italic
        underline := baseFace.underline || overrideFace.underline
      }

Insertion in Bliku/Tui/Syntax/Types.lean at line 93 [2.8034]

[2.8669]

def Palette.merge (base overrides : Palette) : Palette :=
  {
    keyword := mergeFace base.keyword overrides.keyword
    comment := mergeFace base.comment overrides.comment
    stringLiteral := mergeFace base.stringLiteral overrides.stringLiteral
    numberLiteral := mergeFace base.numberLiteral overrides.numberLiteral
    heading := mergeFace base.heading overrides.heading
    code := mergeFace base.code overrides.code
    link := mergeFace base.link overrides.link
    emphasis := mergeFace base.emphasis overrides.emphasis
    custom := overrides.custom ++ base.custom
  }
def defaultPalette : Palette :=
  {
    keyword := some { fg := some (.ansi 12) }
    comment := some { fg := some (.ansi 8) }
    stringLiteral := some { fg := some (.ansi 10) }
    numberLiteral := some { fg := some (.ansi 13) }
    heading := some { fg := some (.ansi 14) }
    code := some { fg := some (.ansi 11) }
    link := some { fg := some (.ansi 12) }
    emphasis := some { fg := some (.ansi 13) }
  }
def Palette.faceFor (palette : Palette) : HighlightKind → Option Face
  | .keyword => palette.keyword
  | .comment => palette.comment
  | .stringLiteral => palette.stringLiteral
  | .numberLiteral => palette.numberLiteral
  | .heading => palette.heading
  | .code => palette.code
  | .link => palette.link
  | .emphasis => palette.emphasis
  | .custom name => palette.custom.find? (fun (n, _) => n == name) |>.map Prod.snd
def profileFor : Language → LanguageProfile
  | .plain => { language := .plain }
  | .lean => {
      language := .lean
      supportedKinds := #[.keyword, .comment, .stringLiteral, .numberLiteral]
    }
  | .markdown => {
      language := .markdown
      supportedKinds := #[.heading, .code, .link, .emphasis]
    }

Replacement in Bliku/Tui/Syntax/Types.lean at line 148 [2.8034]

B:BD[2.8926] → [2.8926:9058]

def styleForByteRange (spans : Array Span) (byteStart byteEnd : Nat) : Option String :=
  let rec loop (i : Nat) : Option String :=

[2.8926]

[2.9058]

def faceForByteRange (palette : Palette) (spans : Array Span) (byteStart byteEnd : Nat) : Option Face :=
  let rec loop (i : Nat) : Option Face :=

Replacement in Bliku/Tui/Syntax/Types.lean at line 155 [2.8034]
B:BD[2.9216] → [2.9216:9237]
```
        some s.style
```
[2.9216]
[2.9237]
```
        palette.faceFor s.kind
```

Replacement in Bliku/Tui/Syntax/Markdown.lean at line 25 [2.9339]

B:BD[2.10085] → [2.10085:10163]

    return #[{ startByte := 0, endByte := n, style := markdownHeadingStyle }]

[2.10085]

[2.10163]

    return #[{ startByte := 0, endByte := n, kind := .heading }]

Replacement in Bliku/Tui/Syntax/Markdown.lean at line 27 [2.9339]

B:BD[2.10195] → [2.10195:10270]

    return #[{ startByte := 0, endByte := n, style := markdownCodeStyle }]

[2.10195]

[2.10270]

    return #[{ startByte := 0, endByte := n, kind := .code }]

Replacement in Bliku/Tui/Syntax/Markdown.lean at line 37 [2.9339]

B:BD[2.10473] → [2.10473:10566]

        spans := spans.push { startByte := i, endByte := j + 1, style := markdownCodeStyle }

[2.10473]

[2.10566]

        spans := spans.push { startByte := i, endByte := j + 1, kind := .code }

Replacement in Bliku/Tui/Syntax/Markdown.lean at line 50 [2.9339]

B:BD[2.10910] → [2.10910:11005]

          spans := spans.push { startByte := i, endByte := k + 1, style := markdownLinkStyle }

[2.10910]

[2.11005]

          spans := spans.push { startByte := i, endByte := k + 1, kind := .link }

Replacement in Bliku/Tui/Syntax/Markdown.lean at line 62 [2.9339]

B:BD[2.11291] → [2.11291:11388]

        spans := spans.push { startByte := i, endByte := j + 1, style := markdownEmphasisStyle }

[2.11291]

[2.11388]

        spans := spans.push { startByte := i, endByte := j + 1, kind := .emphasis }

Replacement in Bliku/Tui/Syntax/Lean.lean at line 48 [2.11535]

B:BD[2.13053] → [2.13053:13138]

      spans := spans.push { startByte := i, endByte := j, style := leanStringStyle }

[2.13053]

[2.13138]

      spans := spans.push { startByte := i, endByte := j, kind := .stringLiteral }

Replacement in Bliku/Tui/Syntax/Lean.lean at line 51 [2.11535]

B:BD[2.13220] → [2.13220:13306]

      spans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }

[2.13220]

[2.13306]

      spans := spans.push { startByte := i, endByte := n, kind := .comment }

Replacement in Bliku/Tui/Syntax/Lean.lean at line 54 [2.11535]

B:BD[2.13388] → [2.13388:13474]

      spans := spans.push { startByte := i, endByte := n, style := leanCommentStyle }

[2.13388]

[2.13474]

      spans := spans.push { startByte := i, endByte := n, kind := .comment }

Replacement in Bliku/Tui/Syntax/Lean.lean at line 65 [2.11535]

B:BD[2.13802] → [2.13802:13887]

      spans := spans.push { startByte := i, endByte := j, style := leanNumberStyle }

[2.13802]

[2.13887]

      spans := spans.push { startByte := i, endByte := j, kind := .numberLiteral }

Replacement in Bliku/Tui/Syntax/Lean.lean at line 73 [2.11535]

B:BD[2.14118] → [2.14118:14206]

        spans := spans.push { startByte := i, endByte := j, style := leanKeywordStyle }

[2.14118]

[2.14206]

        spans := spans.push { startByte := i, endByte := j, kind := .keyword }

Insertion in Bliku/Tui/Render.lean at line 6 [2.15512]
[2.15639]
[2.15639]
```
import Bliku.Tui.Syntax
```

Insertion in Bliku/Tui/Render.lean at line 11 [2.15512]

[2.15685]


structure VisibleCell where
  text : String
  col : Nat
  startByte : Nat
  endByte : Nat
  deriving Repr, Inhabited

Replacement in Bliku/Tui/Render.lean at line 19 [2.15512]

B:BD[2.15686] → [2.15686:15812]

private def renderLineSlice (line : String) (scrollCol width : Nat) : String :=
  ((line.drop scrollCol).take width).toString

[2.15686]

[2.15812]

private def collectVisibleCells (line : String) (scrollCol width : Nat) : Array VisibleCell := Id.run do
  let mut out : Array VisibleCell := #[]
  let mut bytePos := 0
  let mut col := 0
  for ch in line.toList do
    let nextByte := bytePos + ch.utf8Size
    if scrollCol <= col && col < scrollCol + width then
      out := out.push {
        text := ch.toString
        col := col
        startByte := bytePos
        endByte := nextByte
      }
    bytePos := nextByte
    col := col + 1
  out

Insertion in Bliku/Tui/Render.lean at line 36 [2.15512]

[2.15813]

private def lineDisplayLength (line : String) : Nat :=
  line.toList.length

Insertion in Bliku/Tui/Render.lean at line 41 [2.15512]

[2.15909]


private def getExternalSyntaxLine (buf : BufferState) (lineIdx : Nat) : Array Syntax.Span :=
  match buf.syntaxState.lineSpans.find? (fun (row, _) => row == lineIdx) with
  | some (_, spans) => spans
  | none => #[]
private def syntaxPaletteFor (m : Model) (buf : BufferState) : Syntax.Palette :=
  Syntax.Palette.merge m.config.syntaxPalette buf.syntaxState.paletteOverrides
private def syntaxSpansForLine (buf : BufferState) (lineIdx : Nat) (line : String) : Array Syntax.Span :=
  let builtin := Syntax.highlightLine buf.filename line
  let external := getExternalSyntaxLine buf lineIdx
  external ++ builtin

Replacement in Bliku/Tui/Render.lean at line 83 [2.15512]

B:BD[2.16998] → [2.16998:17150]

private def styleVisibleLine
    (m : Model) (windowId lineIdx scrollCol : Nat) (visible : String) (windowCursor : Option Cursor) : String := Id.run do

[2.16998]

[2.17150]

def renderVisibleLine
    (m : Model) (buf : BufferState) (windowId lineIdx scrollCol availableWidth : Nat)
    (windowCursor : Option Cursor) : String := Id.run do

Insertion in Bliku/Tui/Render.lean at line 89 [2.15512]

[2.17353]

  let line := getBufferLine buf lineIdx
  let visibleCells := collectVisibleCells line scrollCol availableWidth
  let syntaxSpans := syntaxSpansForLine buf lineIdx line
  let syntaxPalette := syntaxPaletteFor m buf

Replacement in Bliku/Tui/Render.lean at line 95 [2.15512]

B:BD[2.17435] → [2.17435:17532]

  let chars := visible.toList
  let mut i := 0
  for ch in chars do
    let col := scrollCol + i

[2.17435]

[2.17532]

  for cell in visibleCells do

Insertion in Bliku/Tui/Render.lean at line 97 [2.15512]
[2.17552]
[2.17552]
```
      windowCursor.isSome &&
```
Replacement in Bliku/Tui/Render.lean at line 100 [2.15512]
B:BD[2.17630] → [2.17630:17653]
```
      col == activeCol
```
[2.17630]
[2.17653]
```
      cell.col == activeCol
```

Replacement in Bliku/Tui/Render.lean at line 103 [2.15512]

B:BD[2.17716] → [2.17716:17868]

        if ch == ' ' then some m.config.cursorSpaceStyle else some m.config.cursorCharStyle
      else if isInSelection m selectionCur lineIdx col then

[2.17716]

[2.17868]

        if cell.text == " " then some m.config.cursorSpaceStyle else some m.config.cursorCharStyle
      else if isInSelection m selectionCur lineIdx cell.col then

Replacement in Bliku/Tui/Render.lean at line 107 [2.15512]

B:BD[2.17922] → [2.17922:17935]

        none

[2.17922]

[2.17935]

        (Syntax.faceForByteRange syntaxPalette syntaxSpans cell.startByte cell.endByte).map Syntax.Face.toAnsi

Replacement in Bliku/Tui/Render.lean at line 116 [2.15512]
B:BD[2.18210] → [2.18210:18257]
```
    out := out.push ch.toString
    i := i + 1
```
[2.18210]
[2.18257]
```
    out := out.push cell.text
```

Replacement in Bliku/Tui/Render.lean at line 123 [2.15512]

B:BD[2.18471] → [2.18471:18569]

    (visible : String) (lineToDraw : String) (windowCursor : Option Cursor) : String := Id.run do

[2.18471]

[2.18569]

    (line : String) (lineToDraw : String) (windowCursor : Option Cursor) : String := Id.run do

Replacement in Bliku/Tui/Render.lean at line 128 [2.15512]

B:BD[2.18772] → [2.18772:18810]

  let visLen := visible.toList.length

[2.18772]

[2.18810]

  let visLen := lineDisplayLength line - scrollCol |> min availableWidth

Replacement in Bliku/Tui/Render.lean at line 152 [2.15512]

B:BD[2.19850] → [2.19850:20162]

      let visible := renderLineSlice (getBufferLine buf lineIdx) view.scrollCol availableWidth
      let styled := styleVisibleLine m windowId lineIdx view.scrollCol visible windowCursor
      let lineToDraw := appendCursorOnBlankCell m windowId lineIdx view.scrollCol availableWidth visible styled windowCursor

[2.19850]

[2.20162]

      let line := getBufferLine buf lineIdx
      let styled := renderVisibleLine m buf windowId lineIdx view.scrollCol availableWidth windowCursor
      let lineToDraw := appendCursorOnBlankCell m windowId lineIdx view.scrollCol availableWidth line styled windowCursor

Insertion in Bliku/Tui/Model.lean at line 2 [2.32574]
[2.32599]
[2.32599]
```
import Bliku.Tui.Syntax.Types
```

Insertion in Bliku/Tui/Model.lean at line 25 [2.32574]

[2.33025]


structure BufferSyntaxState where
  lineSpans : Array (Nat × Array Syntax.Span) := #[]
  paletteOverrides : Syntax.Palette := {}
  deriving Repr, Inhabited

Insertion in Bliku/Tui/Model.lean at line 36 [2.32574]
[2.33144]
[2.33144]
```
  syntaxState : BufferSyntaxState := {}
```
Insertion in Bliku/Tui/Model.lean at line 72 [2.32574]
[2.34047]
[2.34047]
```
  syntaxPalette : Syntax.Palette := Syntax.defaultPalette
```