Add scan_comment_whspc to skip space and comments in PGIP stream

--- a/src/Pure/General/xml.ML	Wed Aug 18 11:44:17 2004 +0200
+++ b/src/Pure/General/xml.ML	Wed Aug 18 16:02:11 2004 +0200
@@ -18,6 +18,7 @@
   val parse_content: string list -> tree list * string list
   val parse_elem: string list -> tree * string list
   val parse_document: string list -> (string option * tree) * string list
+  val scan_comment_whspc : string list -> unit * string list
   val tree_of_string: string -> tree
 end;
 
@@ -112,6 +113,9 @@
   Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
   Scan.this_string "-->";
 
+val scan_comment_whspc = 
+    (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
+
 val parse_pi = Scan.this_string "<?" |--
   Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.not_eof)) --|
   Scan.this_string "?>";