# HG changeset patch # User wenzelm # Date 1232142851 -3600 # Node ID 736bf7117153ae162af69270ceea01257ae0229d # Parent 7402322256b04b03ec10826bddb1833d5ea47842 added parse_body_failsafe; diff -r 7402322256b0 -r 736bf7117153 src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Fri Jan 16 21:24:33 2009 +0100 +++ b/src/Pure/General/yxml.scala Fri Jan 16 22:54:11 2009 +0100 @@ -109,12 +109,21 @@ case _ => err("multiple results") } + + /* failsafe parsing */ + + private def markup_failsafe(source: CharSequence) = + XML.Elem (Markup.BAD, Nil, + List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>")))) + + def parse_body_failsafe(source: CharSequence) = { + try { parse_body(source) } + catch { case _: RuntimeException => List(markup_failsafe(source)) } + } + def parse_failsafe(source: CharSequence) = { try { parse(source) } - catch { - case _: RuntimeException => XML.Elem (Markup.BAD, Nil, - List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>")))) - } + catch { case _: RuntimeException => markup_failsafe(source) } } }