src/Pure/General/xml_data.scala
changeset 38355 8cb265fb12fe
parent 38269 cd6906d9199f
child 43698 91c4d7397f0e
     1.1 --- a/src/Pure/General/xml_data.scala	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/General/xml_data.scala	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -15,6 +15,13 @@
     1.4    class XML_Atom(s: String) extends Exception(s)
     1.5  
     1.6  
     1.7 +  private def make_long_atom(i: Long): String = i.toString
     1.8 +
     1.9 +  private def dest_long_atom(s: String): Long =
    1.10 +    try { java.lang.Long.parseLong(s) }
    1.11 +    catch { case e: NumberFormatException => throw new XML_Atom(s) }
    1.12 +
    1.13 +
    1.14    private def make_int_atom(i: Int): String = i.toString
    1.15  
    1.16    private def dest_int_atom(s: String): Int =
    1.17 @@ -71,6 +78,9 @@
    1.18      }
    1.19  
    1.20  
    1.21 +  def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
    1.22 +  def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
    1.23 +
    1.24    def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
    1.25    def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
    1.26