removed non-modular comment;
authorwenzelm
Thu, 01 Feb 2007 20:40:17 +0100
changeset 22227 7f88a6848fc2
parent 22226 699385e6cb45
child 22228 7c27195a4afc
removed non-modular comment;
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)) --|