* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
the scanner
* output functions default_output and xsymbols_output
only print one "\" for symbols (to be consistent with the scanner).

--- a/src/Pure/General/symbol.ML	Tue Apr 13 20:31:55 2004 +0200
+++ b/src/Pure/General/symbol.ML	Tue Apr 13 23:08:12 2004 +0200
@@ -59,7 +59,9 @@
   string, may be of the following form:
     (a) ASCII symbols: a
     (b) printable symbols: \<ident>
-    (c) control symbols: \<^ctrlident>
+    (c) control symbols: \<^ident>
+    (d) raw control symbols: \<^raw...>, where "..." may be any printable
+        character excluding ">"
 
   output is subject to the print_mode variable (default: verbatim),
   actual interpretation in display is up to front-end tools;
@@ -207,11 +209,12 @@
 
 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 =
   $$ "\\" ^^ $$ "<" ^^
     !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
-       ((($$ "^" ^^ scan_ctrlid) || scan_id) ^^ $$ ">") ||
+       ((($$ "^" ^^ (scan_rawctrlid || scan_id)) || scan_id) ^^ $$ ">") ||
   Scan.one not_eof;
 
 (* source *)
@@ -260,9 +263,8 @@
       Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
    Scan.one not_eof) >> implode;
 
-fun default_output s =
-  if not (exists_string (equal "\\") s) then string_size s
-  else string_size (fst (Scan.finite stopper escape (explode s)));
+
+val default_output = string_size
 
 fun default_indent (_: string, k) = spaces k;
 
@@ -290,7 +292,9 @@
 
 fun output_width x = #1 (get_mode ()) x;
 val output = #1 o output_width;
-val plain_output = #1 o default_output;
+fun plain_output s =   
+  if not (exists_string (equal "\\") s) then s
+  else fst (Scan.finite stopper escape (explode s));
 
 fun indent x = #2 (get_mode ()) x;
 

--- a/src/Pure/proof_general.ML	Tue Apr 13 20:31:55 2004 +0200
+++ b/src/Pure/proof_general.ML	Tue Apr 13 23:08:12 2004 +0200
@@ -48,7 +48,7 @@
 fun xsymbols_output s =
   if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
     let val syms = Symbol.explode s
-    in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end
+    in (s, real (Symbol.length syms)) end
   else (s, real (size s));
 
 fun pgml_output (s, len) =