# HG changeset patch
# User wenzelm
# Date 1081941951 -7200
# Node ID 980da32f46175d873ff7264963f2fc87c72ec7fc
# Parent  c53396af770e6449e8308ad09433fb9cc9da67b2
proper handling of lines terminated by CRLF or CR;

diff -r c53396af770e -r 980da32f4617 src/Pure/General/symbol.ML
--- 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;