src/Pure/PIDE/yxml.scala
changeset 80486 24290f18ceb1
parent 80480 972f7a4cdc0e
child 80487 e25c6d4c219c
equal deleted inserted replaced
80485:71aaa7e65d20 80486:24290f18ceb1
    17   val X_byte: Byte = 5
    17   val X_byte: Byte = 5
    18   val Y_byte: Byte = 6
    18   val Y_byte: Byte = 6
    19 
    19 
    20   val X = X_byte.toChar
    20   val X = X_byte.toChar
    21   val Y = Y_byte.toChar
    21   val Y = Y_byte.toChar
    22 
       
    23   val is_X: Char => Boolean = _ == X
       
    24   val is_Y: Char => Boolean = _ == Y
       
    25 
    22 
    26   val X_string: String = X.toString
    23   val X_string: String = X.toString
    27   val Y_string: String = Y.toString
    24   val Y_string: String = Y.toString
    28   val XY_string: String = X_string + Y_string
    25   val XY_string: String = X_string + Y_string
    29   val XYX_string: String = XY_string + X_string
    26   val XYX_string: String = XY_string + X_string