# HG changeset patch
# User schirmer
# Date 1081930108 -7200
# Node ID 7612d19d5638ecae81c8e1914f7e00a8d40d6d22
# Parent  726f6761c5629e23a00f962fb464f6736030d331
bugfix for \<^raw...> scanner

diff -r 726f6761c562 -r 7612d19d5638 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Apr 14 09:53:25 2004 +0200
+++ b/src/Pure/General/symbol.ML	Wed Apr 14 10:08:28 2004 +0200
@@ -208,8 +208,8 @@
 (* scan *)
 
 val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
-val scan_ctrlid = Scan.one is_letter ^^ (Scan.any is_ctrl_letter >> implode);
-val scan_rawctrlid = $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ scan_ctrlid;
+val scan_rawctrlid = 
+    $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ (Scan.any is_ctrl_letter >> implode);
 
 val scan =
   $$ "\\" ^^ $$ "<" ^^