1.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon Nov 18 17:29:49 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Nov 18 17:30:28 1996 +0100
     1.3 @@ -186,6 +186,15 @@
     1.4        fun scan_delim_char ("'" :: c :: cs) =
     1.5              if is_blank c then raise LEXICAL_ERROR else (c, cs)
     1.6          | scan_delim_char ["'"] = err "trailing escape character"
     1.7 +        | scan_delim_char ("\\" :: "{" :: cs) =
     1.8 +            let
     1.9 +              val (ch_name, cs') = (scan_id -- $$ "}" >> #1) cs
    1.10 +                handle LEXICAL_ERROR => err "malformed symbolic char specification";
    1.11 +              val c =
    1.12 +                if ch_name mem SymbolFont.char_names then
    1.13 +                  SymbolFont.char ch_name
    1.14 +                else err ("unknown symbolic char name: " ^ quote ch_name);
    1.15 +            in (c, cs') end
    1.16          | scan_delim_char (chs as c :: cs) =
    1.17              if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
    1.18          | scan_delim_char [] = raise LEXICAL_ERROR;