src/Pure/General/yxml.scala
changeset 31469 40f815edbde4
parent 29563 4773c5c994dc
child 31521 73adb1fa8553
equal deleted inserted replaced
31468:b8267feaf342 31469:40f815edbde4
    15 
    15 
    16   private val X = '\5'
    16   private val X = '\5'
    17   private val Y = '\6'
    17   private val Y = '\6'
    18   private val X_string = X.toString
    18   private val X_string = X.toString
    19   private val Y_string = Y.toString
    19   private val Y_string = Y.toString
    20 
       
    21   def detect(source: CharSequence) = {
       
    22     source.length >= 2 &&
       
    23     source.charAt(0) == X &&
       
    24     source.charAt(1) == Y
       
    25   }
       
    26 
    20 
    27 
    21 
    28   /* iterate over chunks (resembles space_explode in ML) */
    22   /* iterate over chunks (resembles space_explode in ML) */
    29 
    23 
    30   private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] {
    24   private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] {