Init.System.Uri

Decode %HH escapings in the given string. Note that sometimes a consecutive sequence of multiple escapings can represent a utf-8 encoded sequence for a single unicode code point and these will also be decoded correctly.

Instances For

source

def System.Uri.UriEscape.decodeUri.hexDigitToUInt8? (c : UInt8) :

Option UInt8

Instances For

source

def System.Uri.UriEscape.rfc3986ReservedChars :

List Char

Instances For

source

def System.Uri.UriEscape.uriEscapeAsciiChar (c : Char) :

String

Equations

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

Instances For

source

def System.Uri.UriEscape.uriEscapeAsciiChar.uInt8ToHex (c : UInt8) :

String

Equations

System.Uri.UriEscape.uriEscapeAsciiChar.uInt8ToHex c = (hexDigitRepr (c / 16).toNat ++ hexDigitRepr (c % 16).toNat).toUpper

Instances For

source

def System.Uri.escapeUri (uri : String) :

String

Replaces special characters in the given Uri with %HH Uri escapings.

Equations

System.Uri.escapeUri uri = String.foldl (fun (s : String) (c : Char) => s ++ System.Uri.UriEscape.uriEscapeAsciiChar c) "" uri

Instances For

source

def System.Uri.unescapeUri (s : String) :

String

Replaces all %HH Uri escapings in the given string with their corresponding unicode code points. Note that sometimes a consecutive sequence of multiple escapings can represent a utf-8 encoded sequence for a single unicode code point and these will also be decoded correctly.

Instances For

source

def System.Uri.pathToUri (fname : System.FilePath) :

String

Convert the given FilePath to a "file:///encodedpath" Uri.

Instances For

source

def System.Uri.fileUriToPath? (uri : String) :

Option System.FilePath

Convert the given uri to a FilePath stripping the 'file://' prefix, ignoring the optional host name.

Equations

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

Instances For