# HG changeset patch
# User wenzelm
# Date 1170358817 -3600
# Node ID 7f88a6848fc2e4e47c850633af8939602a61224c
# Parent  699385e6cb45b0e8c73aedb1ddafe06b36a1e93d
removed non-modular comment;

diff -r 699385e6cb45 -r 7f88a6848fc2 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Thu Feb 01 13:41:19 2007 +0100
+++ b/src/Pure/General/xml.ML	Thu Feb 01 20:40:17 2007 +0100
@@ -28,7 +28,6 @@
   val parse_elem: string list -> tree * string list
   val parse_document: string list -> (string option * tree) * string list
   val tree_of_string: string -> tree
-  (* scanner for stream parser in proof_general.ML *)
   val scan_comment_whspc : string list -> unit * string list
 end;
 
@@ -84,8 +83,8 @@
 
 datatype tree =
     Elem of string * attributes * tree list
-  | Text of string      
-  | Rawtext of string;  
+  | Text of string
+  | Rawtext of string;
 
 type content = tree list
 
@@ -140,8 +139,8 @@
   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 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)) --|