src/Pure/General/symbol.scala

 
 package isabelle
 
 import scala.collection.mutable
 import scala.util.matching.Regex
+import scala.annotation.tailrec
 
 
 object Symbol
 {
   type Symbol = String

       }
     }
 
   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
 
+  def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) =
+  {
+    var (line, column) = pos
+    for (sym <- iterator(text)) {
+      if (is_physical_newline(sym)) { line += 1; column = 1 }
+      else column += 1
+    }
+    (line, column)
+  }
+
 
   /* decoding offsets */
 
   class Index(text: CharSequence)
   {

     }
     def decode(sym1: Int): Int =
     {
       val sym = sym1 - 1
       val end = index.length
-      def bisect(a: Int, b: Int): Int =
+      @tailrec def bisect(a: Int, b: Int): Int =
       {
         if (a < b) {
           val c = (a + b) / 2
           if (sym < index(c).sym) bisect(a, c)
           else if (c + 1 == end || sym < index(c + 1).sym) c