tuned message;
authorwenzelm
Sat, 11 Aug 2012 17:40:33 +0200
changeset 48769 e3b7087bb923
parent 48768 abc45de5bb22
child 48770 85eeb06ec1c4
tuned message;
src/Pure/PIDE/xml.ML
--- 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;