equal
deleted
inserted
replaced
1 /* Title: Pure/General/length.scala |
|
2 Author: Makarius |
|
3 |
|
4 Text length wrt. encoding. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 trait Length |
|
11 { |
|
12 def apply(text: String): Int |
|
13 def offset(text: String, i: Int): Option[Text.Offset] |
|
14 } |
|
15 |
|
16 object Length extends Length |
|
17 { |
|
18 def apply(text: String): Int = text.length |
|
19 def offset(text: String, i: Int): Option[Text.Offset] = |
|
20 if (0 <= i && i <= text.length) Some(i) else None |
|
21 |
|
22 val encodings: List[(String, Length)] = |
|
23 List( |
|
24 "UTF-16" -> Length, |
|
25 "UTF-8" -> UTF8.Length, |
|
26 "codepoints" -> Codepoint.Length, |
|
27 "symbols" -> Symbol.Length) |
|
28 |
|
29 def encoding(name: String): Length = |
|
30 encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse |
|
31 error("Bad text length encoding: " + quote(name) + |
|
32 " (expected " + commas_quote(encodings.map(_._1)) + ")") |
|
33 } |
|