chore(library/init/data/string/basic): remove broken lineColumn obsoleted by FileMap
This commit is contained in:
parent
8cb387e599
commit
f22c17e94b
3 changed files with 0 additions and 23 deletions
|
|
@ -257,17 +257,6 @@ def prevn : Iterator → Nat → Iterator
|
|||
| it, i+1 => prevn it.prev i
|
||||
end Iterator
|
||||
|
||||
private partial def lineColumnAux (s : String) : Pos → Nat × Nat → Nat × Nat
|
||||
| i, r@(line, col) =>
|
||||
if atEnd s i then r
|
||||
else
|
||||
let c := s.get i;
|
||||
if c = '\n' then lineColumnAux (s.next i) (line+1, 0)
|
||||
else lineColumnAux (s.next i) (line, col+1)
|
||||
|
||||
def lineColumn (s : String) (pos : Pos) : Nat × Nat :=
|
||||
lineColumnAux s 0 (1, 0)
|
||||
|
||||
partial def offsetOfPosAux (s : String) (pos : Pos) : Pos → Nat → Nat
|
||||
| i, offset =>
|
||||
if i == pos || s.atEnd i then offset
|
||||
|
|
|
|||
|
|
@ -7,9 +7,3 @@
|
|||
#eval "αβcc".mkIterator.next.next.pos
|
||||
#eval "αβcc".mkIterator.next.setCurr 'a'
|
||||
#eval "αβcd".mkIterator.toEnd.pos
|
||||
#eval "ab\n\nfoo bla".lineColumn 0
|
||||
#eval "ab\n\nfoo bla".lineColumn 1
|
||||
#eval "ab\n\nfoo bla".lineColumn 2
|
||||
#eval "ab\n\nfoo bla".lineColumn 3
|
||||
#eval "ab\n\nfoo bla".lineColumn 8
|
||||
#eval "ab\n\nfoo bla".lineColumn 100
|
||||
|
|
|
|||
|
|
@ -7,9 +7,3 @@
|
|||
4
|
||||
(String.Iterator.mk "αacc" 2)
|
||||
6
|
||||
(3, 7)
|
||||
(3, 7)
|
||||
(3, 7)
|
||||
(3, 7)
|
||||
(3, 7)
|
||||
(3, 7)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue