proper handling of lines terminated by CRLF or CR;

--- a/src/Pure/General/symbol.ML	Wed Apr 14 12:19:16 2004 +0200
+++ b/src/Pure/General/symbol.ML	Wed Apr 14 13:25:51 2004 +0200
@@ -214,6 +214,7 @@
 
 (* scan *)
 
+val scan_newline = ($$ "\r" ^^ $$ "\n" || $$ "\r") >> K "\n";
 val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
 val scan_rawctrlid = 
     $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ $$ ":" ^^ (Scan.any is_ctrl_letter >> implode);
@@ -223,8 +224,10 @@
   ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
     !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
        ((($$ "^" ^^ (scan_rawctrlid || scan_id)) || scan_id) ^^ $$ ">") ||
+  scan_newline ||
   Scan.one not_eof;
 
+
 (* source *)
 
 val recover = Scan.any ((not o is_blank) andf not_eof) >> K [malformed];
@@ -235,13 +238,14 @@
 
 (* explode *)
 
-fun no_syms [] = true
-  | no_syms ("\\" :: "<" :: _) = false
-  | no_syms (_ :: cs) = no_syms cs;
+fun no_explode [] = true
+  | no_explode ("\\" :: "<" :: _) = false
+  | no_explode ("\r" :: _) = false
+  | no_explode (_ :: cs) = no_explode cs;
 
 fun sym_explode str =
   let val chs = explode str in
-    if no_syms chs then chs     (*tune trivial case*)
+    if no_explode chs then chs
     else the (Scan.read stopper (Scan.repeat scan) chs)
   end;