author | wenzelm |
Sat, 11 Aug 2012 17:40:33 +0200 | |
changeset 48769 | e3b7087bb923 |
parent 48768 | abc45de5bb22 |
child 48770 | 85eeb06ec1c4 |
--- a/src/Pure/PIDE/xml.ML Sat Aug 11 17:24:21 2012 +0200 +++ b/src/Pure/PIDE/xml.ML Sat Aug 11 17:40:33 2012 +0200 @@ -224,7 +224,7 @@ (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element")) (blanks |-- parse_document --| blanks))) (raw_explode s) of (x, []) => x - | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys)); + | (_, ys) => error ("XML parsing error: unprocessed input\n" ^ Symbol.beginning 100 ys)); end;