tuned;

--- a/src/Pure/General/symbol.ML	Mon May 10 19:26:11 2004 +0200
+++ b/src/Pure/General/symbol.ML	Mon May 10 19:26:25 2004 +0200
@@ -35,7 +35,7 @@
   val is_blank: symbol -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
-  val beginning: symbol list -> string
+  val beginning: int -> symbol list -> string
   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
   val scan_id: string list -> string * string list
   val scan: string list -> symbol * string list
@@ -300,16 +300,16 @@
 
 (* scanning through symbols *)
 
-fun beginning raw_ss =
+fun beginning n raw_ss =
   let
     val (all_ss, _) = Library.take_suffix is_blank raw_ss;
-    val dots = if length all_ss > 10 then " ..." else "";
-    val (ss, _) = Library.take_suffix is_blank (Library.take (10, all_ss));
+    val dots = if length all_ss > n then " ..." else "";
+    val (ss, _) = Library.take_suffix is_blank (Library.take (n, all_ss));
   in implode (map (fn s => if is_blank s then space else s) ss) ^ dots end;
 
 fun scanner msg scan chs =
   let
-    fun err_msg cs = msg ^ ": " ^ beginning cs;
+    fun err_msg cs = msg ^ ": " ^ beginning 10 cs;
     val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan));
   in
     (case fin_scan chs of
@@ -327,18 +327,17 @@
 val scan_encoded_newline =
   $$ "\r" -- $$ "\n" >> K "\n" ||
   $$ "\r" >> K "\n" ||
-  Scan.optional ($$ "\\") "" -- $$ "\\"  -- $$ "<"  -- $$ "^" -- $$ "n"
-    -- $$ "e" -- $$ "w" -- $$ "l" -- $$ "i" -- $$ "n" -- $$ "e" -- $$ ">" >> K "\n";
+  Scan.optional ($$ "\\") "" -- Scan.list (explode "\\<^newline>") >> K "\n";
 
 fun raw_body c = ord space <= ord c andalso ord c <= ord "~" andalso c <> ">";
-val scan_raw = $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ $$ ":" ^^ (Scan.any raw_body >> implode);
+val scan_raw = Scan.list (explode "raw:") -- Scan.any raw_body >> (implode o op @);
 
 in
 
 val scan =
   scan_encoded_newline ||
   ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
-    !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
+    !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning 10 cs)
        (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">") ||
   Scan.one not_eof;
 

--- a/src/Pure/General/xml.ML	Mon May 10 19:26:11 2004 +0200
+++ b/src/Pure/General/xml.ML	Mon May 10 19:26:25 2004 +0200
@@ -1,12 +1,9 @@
 (*  Title:      Pure/General/xml.ML
     ID:         $Id$
-    Author:     Markus Wenzel, LMU Muenchen
-                Stefan Berghofer, TU Muenchen
+    Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Basic support for XML input and output.
-
-FIXME da: missing input raises FAIL (scan.ML), should give error message.
 *)
 
 signature XML =
@@ -51,13 +48,14 @@
 
 fun cdata s = cdata_open ^ s ^ cdata_close;
 
+
 (* elements *)
 
 datatype tree =
     Elem of string * (string * string) list * tree list
   | Text of string;
 
-fun attribute (a, x) = a ^ " = \"" ^ (text x) ^ "\"";
+fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
 
 fun element name atts cs =
   let val elem = space_implode " " (name :: map attribute atts) in
@@ -67,41 +65,41 @@
 
 fun string_of_tree (Elem (name, atts, ts)) =
       element name atts (map string_of_tree ts)
-  | string_of_tree (Text s) = s
-  
+  | string_of_tree (Text s) = s;
+
 val header = "<?xml version=\"1.0\"?>\n";
 
 
 (* parser *)
 
-fun err s (xs, _) = "XML parsing error: " ^ s ^ "\nfound:\n" ^
-  implode (take (100, xs));
+fun err s (xs, _) =
+  "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
 
-val scan_whspc = Scan.repeat ($$ " " || $$ "\n" || $$ "\t");
+val scan_whspc = Scan.any Symbol.is_blank;
 
-val literal = Scan.literal o Scan.make_lexicon o single o explode;
+fun scan_string s = Scan.list (Symbol.explode s) >> K s;
 
 val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
 
 val parse_chars = Scan.repeat1 (Scan.unless (scan_whspc -- $$ "<")
   (scan_special || Scan.one Symbol.not_eof)) >> implode;
 
-val parse_cdata = literal "<![CDATA[" |--
-  (Scan.repeat (Scan.unless (literal "]]>") (Scan.one Symbol.not_eof)) >>
-    implode) --| literal "]]>";
+val parse_cdata = scan_string "<![CDATA[" |--
+  (Scan.repeat (Scan.unless (scan_string "]]>") (Scan.one Symbol.not_eof)) >>
+    implode) --| scan_string "]]>";
 
 val parse_att =
   Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "\"" --
   (Scan.repeat (Scan.unless ($$ "\"")
     (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "\"";
 
-val parse_comment = literal "<!--" --
-  Scan.repeat (Scan.unless (literal "-->") (Scan.one Symbol.not_eof)) --
-  literal "-->";
+val parse_comment = scan_string "<!--" --
+  Scan.repeat (Scan.unless (scan_string "-->") (Scan.one Symbol.not_eof)) --
+  scan_string "-->";
 
-val parse_pi = literal "<?" |--
-  Scan.repeat (Scan.unless (literal "?>") (Scan.one Symbol.not_eof)) --|
-  literal "?>";
+val parse_pi = scan_string "<?" |--
+  Scan.repeat (Scan.unless (scan_string "?>") (Scan.one Symbol.not_eof)) --|
+  scan_string "?>";
 
 fun parse_content xs =
   ((Scan.optional (scan_whspc |-- parse_chars >> (single o Text)) [] --
@@ -117,14 +115,14 @@
   ($$ "<" |-- Symbol.scan_id --
     Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
       !! (err "Expected > or />")
-        (   literal "/>" >> K []
+        (scan_string "/>" >> K []
          || $$ ">" |-- parse_content --|
             !! (err ("Expected </" ^ s ^ ">"))
-              (literal ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
+              (scan_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
     (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
 
 val parse_document =
-  Scan.option (literal "<!DOCTYPE" -- scan_whspc |--
+  Scan.option (scan_string "<!DOCTYPE" -- scan_whspc |--
     (Scan.repeat (Scan.unless ($$ ">")
       (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
   parse_elem;
@@ -132,8 +130,7 @@
 fun tree_of_string s =
   (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
       (scan_whspc |-- parse_elem --| scan_whspc))) (Symbol.explode s) of
-     (x, []) => x
-   | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^
-       implode (take (100, ys))));
+    (x, []) => x
+  | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
 
 end;