src/Pure/General/symbol.ML

   val DEL: symbol
   val space: symbol
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
   val is_symbolic: symbol -> bool
+  val is_symbolic_char: symbol -> bool
   val is_printable: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
   val stopper: symbol Scan.stopper

 
 fun is_char s = size s = 1;
 
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
 
+fun raw_symbolic s =
+  String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
+
 fun is_symbolic s =
-  String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
+  s <> "\\<open>" andalso s <> "\\<close>" andalso raw_symbolic s;
+
+val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
 
 fun is_printable s =
   if is_char s then ord space <= ord s andalso ord s <= ord "~"
-  else is_utf8 s orelse is_symbolic s;
+  else is_utf8 s orelse raw_symbolic s;
 
 
 (* input source control *)
 
 val eof = "";

 
 (* bump string -- treat as base 26 or base 1 numbers *)
 
 fun symbolic_end (_ :: "\\<^sub>" :: _) = true
   | symbolic_end ("'" :: ss) = symbolic_end ss
-  | symbolic_end (s :: _) = is_symbolic s
+  | symbolic_end (s :: _) = raw_symbolic s
   | symbolic_end [] = false;
 
 fun bump_init str =
   if symbolic_end (rev (sym_explode str)) then str ^ "'"
   else str ^ "a";