[gathering-options] Arrow symbol

[Mark Thornton]

On 24/06/11 22:03, David M. Lloyd wrote:
> To save others the trouble here are the obvious unicode arrows
>> Use ?
>>      {x ?  x + 1}
>>      (x) ?  {x + 1}
>>
>> Use ?
>>      {x ?  x + 1}
>>      (x) ?  {x + 1}
>>
>> (with a larger arrow font size)
>>      {x?   x + 1}
>>      (x)?   {x + 1}
>>
>>
>>
>> Doesn't look that good in the font/size shown above
> This came across as:
>
> Content-Type: text/plain; charset="us-ascii"
>
> So can't really tell what you were after.  But I can say that there are
> dozens of Unicode arrows... possibly thousands of Unicode candidates all
> told.  I'm not sure it's wise to open that particular can of worms.
>
The original email contained both ascii and a text/html parts. The html 
encoding used character entities as shown below. I guess this is another 
example of why we aren't ready for unicode in the language itself.

     <pre wrap=""><font size="+1">Use&#8614;
   {x&#8614;  x + 1}
   (x)&#8614;  {x + 1}

Use&#10236;
   {x&#10236;  x + 1}
   (x)&#10236;  {x + 1}</font>

(with a larger arrow font size)
<font size="+1">   {x<font size="+2">&#10236;</font>   x + 1}
   (x)<font size="+2">&#10236;</font>   {x + 1}</font>


Regards,
Mark Thornton