[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: pretty fonts in sources

How about giving the user control over fat- and normal strings?
For example, "a string" could strip out font info, while #"a 1string0"
could retain it.  The dispatch sequence #" is currently unused.  Of
course, there would still be an argument over which behavior should
be standard, and which should go under #".