changeset 55551 | 4a5f65df29fa |
parent 48996 | a8bad1369ada |
child 55554 | d77090e07000 |
--- a/src/Pure/PIDE/yxml.scala Tue Feb 18 16:34:02 2014 +0100 +++ b/src/Pure/PIDE/yxml.scala Tue Feb 18 17:03:12 2014 +0100 @@ -120,7 +120,7 @@ /* failsafe parsing */ private def markup_broken(source: CharSequence) = - XML.elem(Markup.Broken.name, List(XML.Text(source.toString))) + XML.Elem(Markup.Broken, List(XML.Text(source.toString))) def parse_body_failsafe(source: CharSequence): XML.Body = {