diff --git a/Colorized.lean b/Colorized.lean index 0ee84f9..9b377d7 100644 --- a/Colorized.lean +++ b/Colorized.lean @@ -7,6 +7,7 @@ to change the foreground and background colors, as well as to apply various text inductive Section | Foreground | Background + deriving BEq, Inhabited, Ord, DecidableEq, Repr /-- The `Color` type represents different color options available for text. -/ inductive Color @@ -18,19 +19,35 @@ inductive Color | Magenta | Cyan | White + | BrightBlack + | BrightRed + | BrightGreen + | BrightYellow + | BrightBlue + | BrightMagenta + | BrightCyan + | BrightWhite | Default + deriving BEq, Inhabited, Ord, DecidableEq, Repr -instance : Repr Color where - reprPrec - | Color.Black, _ => "0" - | Color.Red, _ => "1" - | Color.Green, _ => "2" - | Color.Yellow, _ => "3" - | Color.Blue, _ => "4" - | Color.Magenta, _ => "5" - | Color.Cyan, _ => "6" - | Color.White, _ => "7" - | Color.Default, _ => "9" +@[inline] private def colorCode : Color -> Int + | Color.Black => 30 + | Color.Red => 31 + | Color.Green => 32 + | Color.Yellow => 33 + | Color.Blue => 34 + | Color.Magenta => 35 + | Color.Cyan => 36 + | Color.White => 37 + | Color.BrightBlack => 90 + | Color.BrightRed => 91 + | Color.BrightGreen => 92 + | Color.BrightYellow => 93 + | Color.BrightBlue => 94 + | Color.BrightMagenta => 95 + | Color.BrightCyan => 96 + | Color.BrightWhite => 97 + | Color.Default => 39 /-- The `Style` type represents different text styles that can be applied. -/ inductive Style @@ -42,18 +59,63 @@ inductive Style | SlowBlink | ColoredNormal | Reverse + | Strikethrough + | DoubleUnderline + deriving BEq, Inhabited, Ord, DecidableEq, Repr -instance : Repr Style where - reprPrec - | Style.Normal, _ => "0" - | Style.Bold, _ => "1" - | Style.Faint, _ => "2" - | Style.Italic, _ => "3" - | Style.Underline, _ => "4" - | Style.SlowBlink, _ => "5" - | Style.ColoredNormal, _ => "6" - | Style.Reverse, _ => "7" +@[inline] private def styleCode : Style -> Nat + | Style.Normal => 0 + | Style.Bold => 1 + | Style.Faint => 2 + | Style.Italic => 3 + | Style.Underline => 4 + | Style.SlowBlink => 5 + | Style.ColoredNormal => 6 + | Style.Reverse => 7 + | Style.Strikethrough => 9 + | Style.DoubleUnderline => 21 +/-- Cursor movement and screen control operations -/ +inductive CursorOp + | Up (n : Nat) + | Down (n : Nat) + | Forward (n : Nat) + | Back (n : Nat) + | NextLine (n : Nat) + | PreviousLine (n : Nat) + | Position (row col : Nat) + | HorizontalAbsolute (n : Nat) + | SavePosition + | RestorePosition + | HideCursor + | ShowCursor + deriving BEq, Inhabited, Ord, DecidableEq, Repr + +@[inline] private def cursorOpCode : CursorOp -> String + | CursorOp.Up n => s!"{n}A" + | CursorOp.Down n => s!"{n}B" + | CursorOp.Forward n => s!"{n}C" + | CursorOp.Back n => s!"{n}D" + | CursorOp.NextLine n => s!"{n}E" + | CursorOp.PreviousLine n => s!"{n}F" + | CursorOp.HorizontalAbsolute n => s!"{n}G" + | CursorOp.Position x y => s!"{x};{y}H" + | CursorOp.SavePosition => "s" + | CursorOp.RestorePosition => "u" + | CursorOp.HideCursor => "?25l" + | CursorOp.ShowCursor => "?25h" + +/-- Screen erasing operations -/ +inductive EraseOp + | ToEnd + | FromBeginning + | Entire + deriving BEq, Inhabited, Ord, DecidableEq, Repr + +@[inline] private def eraseOpCode : EraseOp -> Nat + | EraseOp.ToEnd => 0 + | EraseOp.FromBeginning => 1 + | EraseOp.Entire => 2 /-- The `Colorized` class defines an interface for colorizing and styling text. It provides methods for applying color to the foreground or background, and for applying different text styles. @@ -64,19 +126,27 @@ class Colorized (α : Type) where bgColor := colorize Section.Background color := colorize Section.Foreground +/-- Cursor control class -/ +class CursorControl (α : Type) where + cursor : CursorOp → α + eraseScreen : EraseOp → α + eraseLine : EraseOp → α + /-- Constant string representing the beginning of an ANSI escape sequence. -/ -private def const := "\x1b[" +@[inline] private def const := "\x1b[" /-- Constant string for resetting text formatting. -/ -private def reset := "\x1b[0m" - -instance : Colorized String where - colorize sec col str := - let sectionNum := - match sec with - | Section.Foreground => "9" - | Section.Background => "4" - s!"{const}{sectionNum}{repr col}m{str}{reset}" - - style sty str := - s!"{const}{repr sty}m{str}{reset}" +@[inline] private def reset := "\x1b[0m" + +@[inline] private def colorSectionCode : Section → Color → Int + | Section.Foreground, c => colorCode c + | Section.Background, c => colorCode c + 10 + +@[inline] instance : Colorized String where + colorize sec col str := s!"{const}{colorSectionCode sec col}m{str}{reset}" + style sty str := s!"{const}{styleCode sty}m{str}{reset}" + +@[inline] instance : CursorControl String where + cursor op := s!"{const}{cursorOpCode op}" + eraseScreen param := s!"{const}{eraseOpCode param}J" + eraseLine param := s!"{const}{eraseOpCode param}K" diff --git a/Example.lean b/Example.lean index 09024c1..5dc114f 100644 --- a/Example.lean +++ b/Example.lean @@ -1,12 +1,96 @@ -import «Colorized» +import Colorized open Colorized def main : IO Unit := do - -- | Simple style - IO.println (Colorized.style Style.Underline "Hello, world!") + -- Basic styles + IO.println (Colorized.style Style.Bold "Bold text") + IO.println (Colorized.style Style.Italic "Italic text") + IO.println (Colorized.style Style.Underline "Underlined text") + IO.println (Colorized.style Style.Strikethrough "Strikethrough text") + IO.println (Colorized.style Style.Faint "Faint text") + IO.println (Colorized.style Style.SlowBlink "Blinking text") + IO.println (Colorized.style Style.Reverse "Reversed text") + IO.println (Colorized.style Style.DoubleUnderline "Double underlined text") - -- | Simple color - IO.println (Colorized.color Color.Cyan "Hello, world!") + -- Standard colors (foreground) + IO.println (Colorized.color Color.Red "Red text") + IO.println (Colorized.color Color.Green "Green text") + IO.println (Colorized.color Color.Blue "Blue text") + IO.println (Colorized.color Color.Yellow "Yellow text") + IO.println (Colorized.color Color.Magenta "Magenta text") + IO.println (Colorized.color Color.Cyan "Cyan text") + IO.println (Colorized.color Color.White "White text") + IO.println (Colorized.color Color.Black "Black text") - -- | Combine style and color - IO.println (Colorized.color Color.Magenta (Colorized.style Style.Underline "Hello, world!")) + -- Bright colors + IO.println (Colorized.color Color.BrightRed "Bright red text") + IO.println (Colorized.color Color.BrightGreen "Bright green text") + IO.println (Colorized.color Color.BrightBlue "Bright blue text") + IO.println (Colorized.color Color.BrightYellow "Bright yellow text") + IO.println (Colorized.color Color.BrightMagenta "Bright magenta text") + IO.println (Colorized.color Color.BrightCyan "Bright cyan text") + IO.println (Colorized.color Color.BrightWhite "Bright white text") + IO.println (Colorized.color Color.BrightBlack "Bright black text") + + -- Background colors + IO.println (Colorized.bgColor Color.Red "Red background") + IO.println (Colorized.bgColor Color.Green "Green background") + IO.println (Colorized.bgColor Color.Blue "Blue background") + IO.println (Colorized.bgColor Color.BrightYellow "Bright yellow background") + + -- Combined style and color + IO.println (Colorized.color Color.Red (Colorized.style Style.Bold "Bold red text")) + IO.println (Colorized.color Color.Green (Colorized.style Style.Italic "Italic green text")) + IO.println (Colorized.color Color.Blue (Colorized.style Style.Underline "Underlined blue text")) + IO.println (Colorized.bgColor Color.Yellow (Colorized.color Color.Black "Black on yellow")) + + -- Nested combinations + IO.println (Colorized.bgColor Color.BrightBlue + (Colorized.color Color.BrightWhite + (Colorized.style Style.Bold "Bold white on bright blue"))) + + -- Cursor operations + IO.print (CursorControl.cursor (α := String) (CursorOp.Up 2)) + IO.print "Moved up 2 lines" + IO.print (CursorControl.cursor (α := String) (CursorOp.Down 2)) + IO.println "" + + IO.print (CursorControl.cursor (α := String) (CursorOp.Forward 10)) + IO.print "Moved forward" + IO.print (CursorControl.cursor (α := String) (CursorOp.Back 10)) + IO.println "" + + IO.print (CursorControl.cursor (α := String) (CursorOp.Position 5 10)) + IO.print "At position (5,10)" + IO.println "" + + -- Save/restore position + IO.print (CursorControl.cursor (α := String) CursorOp.SavePosition) + IO.print "Position saved" + IO.print (CursorControl.cursor (α := String) (CursorOp.Forward 20)) + IO.print "Moved forward" + IO.print (CursorControl.cursor (α := String) CursorOp.RestorePosition) + IO.println "Back to saved position" + + -- Hide/show cursor + IO.print (CursorControl.cursor (α := String) CursorOp.HideCursor) + IO.print "Cursor hidden (wait 1 sec)" + -- In real usage, you'd add a delay here + IO.print (CursorControl.cursor (α := String) CursorOp.ShowCursor) + IO.println "Cursor shown" + + -- Erase operations + IO.print "This line will be partially erased" + IO.print (CursorControl.eraseLine (α := String) EraseOp.ToEnd) + IO.println "" + + IO.print "Clearing screen in 3 seconds..." + -- In real usage, you'd add a delay here + IO.print (CursorControl.eraseScreen (α := String) EraseOp.Entire) + + -- Test edge cases + IO.println (Colorized.color Color.Default "Default color") + IO.println (Colorized.bgColor Color.Default "Default background") + IO.println (Colorized.style Style.Normal "Normal style (reset)") + + IO.println "All tests completed!" diff --git a/lakefile.lean b/lakefile.lean index fd62503..819ad46 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,11 +1,11 @@ import Lake open Lake DSL -package «Colorized» where +package Colorized where -- add package configuration options here @[default_target] -lean_lib «Colorized» where +lean_lib Colorized where -- add library configuration options here lean_exe «example» where