structure Unicode.UCDStreamextends Substring : Type

Stream type for Unicode Character Database (UCD) files

Unicode data files are semicolon ; (U+003B) separated fields, except for Unihan files and a few others that are tab (U+0009) separated. White spaces around field values are not significant. Line comments are prefixed with a number sign # (U+0023).

• str : String
• startPos : String.Pos
• stopPos : String.Pos
• isUnihan : Bool

  isUnihan is true if the records are tab separated

def Unicode.instInhabitedUCDStream.default : UCDStream

Equations

• Unicode.instInhabitedUCDStream.default = { toSubstring := default, isUnihan := default }

instance Unicode.instInhabitedUCDStream : Inhabited UCDStream

Equations

• Unicode.instInhabitedUCDStream = { default := Unicode.instInhabitedUCDStream.default }

def Unicode.UCDStream.ofSubstring (str : Substring) : UCDStream

Make a UCDStream from a substring

Equations

• Unicode.UCDStream.ofSubstring str = { toSubstring := str }

def Unicode.UCDStream.ofString (str : String) : UCDStream

Make a UCDStream from a string

Equations

• Unicode.UCDStream.ofString str = { str := str, startPos := 0, stopPos := str.endPos }

def Unicode.UCDStream.ofFile (path : System.FilePath) : IO UCDStream

Make a UCDStream from a file

Equations

• Unicode.UCDStream.ofFile path = Unicode.UCDStream.ofString <$> IO.FS.readFile path

partial def Unicode.UCDStream.nextLine? (stream : UCDStream) : Option (Substring × UCDStream)

Get the next line from the UCDStream

Line comments are stripped and blank lines are skipped.

def Unicode.UCDStream.next? (stream : UCDStream) : Option (Array Substring × UCDStream)

Get the next record from the UCDStream

Spaces around field values are trimmed.

Equations

• One or more equations did not get rendered due to their size.

instance Unicode.UCDStream.instStreamArraySubstring : Stream UCDStream (Array Substring)

Equations

• Unicode.UCDStream.instStreamArraySubstring = { next? := Unicode.UCDStream.next? }