in src/main/kotlin/org/arend/search/ArendWordScanner.kt [43:84]
protected fun stripWords(
processor: Processor<in WordOccurrence>,
tokenText: CharSequence,
from: Int,
to: Int,
kind: WordOccurrence.Kind,
occurrence: WordOccurrence
): Boolean {
var index = from
ScanWordsLoop@ while (true) {
while (true) {
if (index == to) break@ScanWordsLoop
var ch = tokenText[index]
while (ch == '\\') {
do {
index++
if (index == to) break@ScanWordsLoop
ch = tokenText[index]
} while (ch in 'a'..'z' || ch in 'A'..'Z' || ch == '-' || ch in '0'..'9')
}
if (isArendIdentifierStart(ch)) {
break
}
index++
}
val wordStart = index
while (true) {
index++
if (index == to) break
val c = tokenText[index]
if (!isArendIdentifierPart(c)) break
}
val wordEnd = index
occurrence.init(tokenText, wordStart, wordEnd, kind)
if (!processor.process(occurrence)) return false
}
return true
}