src/Pure/General/yxml.scala
changeset 27960 65b10d8ef0c6
parent 27946 ec706ad37564
child 27971 57dc3bd6f841
equal deleted inserted replaced
27959:d6a4d7b013f7 27960:65b10d8ef0c6
    14 
    14 
    15   /* chunk markers */
    15   /* chunk markers */
    16 
    16 
    17   private val X = '\5'
    17   private val X = '\5'
    18   private val Y = '\6'
    18   private val Y = '\6'
       
    19   private val X_string = X.toString
    19   private val Y_string = Y.toString
    20   private val Y_string = Y.toString
    20 
    21 
    21   def detect(source: CharSequence) = {
    22   def detect(source: CharSequence) = {
    22     source.length >= 2 &&
    23     source.length >= 2 &&
    23     source.charAt(0) == X &&
    24     source.charAt(0) == X &&
   108     parse_body(source) match {
   109     parse_body(source) match {
   109       case List(result) => result
   110       case List(result) => result
   110       case Nil => XML.Text("")
   111       case Nil => XML.Text("")
   111       case _ => err("multiple results")
   112       case _ => err("multiple results")
   112     }
   113     }
       
   114 
       
   115   def parse_failsafe(source: CharSequence) = {
       
   116     try { parse(source) }
       
   117     catch {
       
   118       case e: BadYXML => XML.Elem (Markup.MALFORMED, Nil,
       
   119         List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
       
   120     }
       
   121   }
       
   122 
   113 }
   123 }