src/Pure/PIDE/yxml.scala
changeset 45666 d83797ef0d2d
parent 44698 0385292321a0
child 45667 546d78f0d81f
     1.1 --- a/src/Pure/PIDE/yxml.scala	Mon Nov 28 20:39:08 2011 +0100
     1.2 +++ b/src/Pure/PIDE/yxml.scala	Mon Nov 28 22:05:32 2011 +0100
     1.3 @@ -118,18 +118,18 @@
     1.4  
     1.5    /* failsafe parsing */
     1.6  
     1.7 -  private def markup_malformed(source: CharSequence) =
     1.8 -    XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
     1.9 +  private def markup_broken(source: CharSequence) =
    1.10 +    XML.elem(Markup.Broken.name, List(XML.Text(source.toString)))
    1.11  
    1.12    def parse_body_failsafe(source: CharSequence): XML.Body =
    1.13    {
    1.14      try { parse_body(source) }
    1.15 -    catch { case ERROR(_) => List(markup_malformed(source)) }
    1.16 +    catch { case ERROR(_) => List(markup_broken(source)) }
    1.17    }
    1.18  
    1.19    def parse_failsafe(source: CharSequence): XML.Tree =
    1.20    {
    1.21      try { parse(source) }
    1.22 -    catch { case ERROR(_) => markup_malformed(source) }
    1.23 +    catch { case ERROR(_) => markup_broken(source) }
    1.24    }
    1.25  }