allow Isabelle symbols within low-level ML source;

--- a/src/Pure/ML/ml_lex.ML	Wed Jun 10 11:12:06 2009 +0200
+++ b/src/Pure/ML/ml_lex.ML	Wed Jun 10 11:12:40 2009 +0200
@@ -247,7 +247,11 @@
   Symbol_Pos.source (Position.line 1) src
   |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
 
-val tokenize = Source.of_string #> source #> Source.exhaust;
+val tokenize =
+  Source.of_string #>
+  Symbol.source {do_recover = true} #>
+  source #>
+  Source.exhaust;
 
 fun read_antiq (syms, pos) =
   (Source.of_list syms

--- a/src/Pure/ML/ml_syntax.ML	Wed Jun 10 11:12:06 2009 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Wed Jun 10 11:12:40 2009 +0200
@@ -58,7 +58,7 @@
   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
 
 fun print_char s =
-  if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
+  if not (Symbol.is_char s) then s
   else if s = "\"" then "\\\""
   else if s = "\\" then "\\\\"
   else
@@ -68,7 +68,7 @@
       else "\\" ^ string_of_int c
     end;
 
-val print_string = quote o translate_string print_char;
+val print_string = quote o implode o map print_char o Symbol.explode;
 val print_strings = print_list print_string;
 
 val print_properties = print_list (print_pair print_string print_string);