--- a/src/Pure/General/symbol.scala Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/General/symbol.scala Wed Dec 28 17:10:09 2016 +0100
@@ -130,11 +130,11 @@
def length(text: CharSequence): Int = iterator(text).length
- object Length extends isabelle.Length
+ object Length extends Text.Length
{
def apply(text: String): Int = length(text)
def offset(text: String, i: Int): Option[Text.Offset] =
- if (i <= 0 || iterator(text).forall(s => s.length == 1)) isabelle.Length.offset(text, i)
+ if (i <= 0 || iterator(text).forall(s => s.length == 1)) Text.Length.offset(text, i)
else if (i <= length(text)) Some(iterator(text).take(i).mkString.length)
else None
}