src/Pure/General/symbol.scala
changeset 64612 08e4b1aeac50
parent 64477 8be21ca788ca
child 64615 fd0d6de380c6
equal deleted inserted replaced
64611:d72d63d05bdb 64612:08e4b1aeac50
   126       }
   126       }
   127     }
   127     }
   128 
   128 
   129   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
   129   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
   130 
   130 
   131   def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) =
       
   132   {
       
   133     var (line, column) = pos
       
   134     for (sym <- iterator(text)) {
       
   135       if (is_newline(sym)) { line += 1; column = 1 }
       
   136       else column += 1
       
   137     }
       
   138     (line, column)
       
   139   }
       
   140 
       
   141 
   131 
   142   /* decoding offsets */
   132   /* decoding offsets */
   143 
   133 
   144   object Index
   134   object Index
   145   {
   135   {