Legacy string functions

This file contains String functions which have since been replaced by different functions and will be deprecated in the future.

@[irreducible, specialize #[]]

def String.splitAux (s : String) (p : Char → Bool) (b i : Pos.Raw) (r : List String) : List String

@[inline]

def String.splitToList (s : String) (p : Char → Bool) : List String

Splits a string at each character for which p returns true.

The characters that satisfy p are not included in any of the resulting strings. If multiple characters in a row satisfy p, then the resulting list will contain empty strings.

This is a legacy function. Use String.split instead.

Examples:

• "coffee tea water".split (·.isWhitespace) = ["coffee", "tea", "water"]
• "coffee tea water".split (·.isWhitespace) = ["coffee", "", "tea", "", "water"]
• "fun x =>\n x + 1\n".split (· == '\n') = ["fun x =>", " x + 1", ""]

@[irreducible]

def String.splitOnAux (s sep : String) (b i j : Pos.Raw) (r : List String) : List String

Auxiliary for splitOn. Preconditions:

• sep is not empty
• b <= i are indexes into s
• j is an index into sep, and not at the end

It represents the state where we have currently parsed some split parts into r (in reverse order), b is the beginning of the string / the end of the previous match of sep, and the first j bytes of sep match the bytes i-j .. i of s.

@[inline]

def String.splitOn (s : String) (sep : String := " ") : List String

Splits a string s on occurrences of the separator string sep. The default separator is " ".

When sep is empty, the result is [s]. When sep occurs in overlapping patterns, the first match is taken. There will always be exactly n+1 elements in the returned list if there were n non-overlapping matches of sep in the string. The separators are not included in the returned substrings.

This is a legacy function. Use String.split instead.

Examples:

• "here is some text ".splitOn = ["here", "is", "some", "text", ""]
• "here is some text ".splitOn "some" = ["here is ", " text "]
• "here is some text ".splitOn "" = ["here is some text "]
• "ababacabac".splitOn "aba" = ["", "bac", "c"]