[isabelle] Unicode (Was: Update on I3P)



Dear Holger,

Am Dienstag, den 20.07.2010, 15:03 +0200 schrieb Holger Gast:
> >  * Using the IsabelleText TrueType font that comes with Isabelle-2009-2,
> > I can not display a few special characters, especially \<guillemotleft>,
> > \<guillemotright> and \<one>. These are shown as a black square. Is that
> > a problem with i3p, the font, or something else?
> >  * Calligraphic math (e.g. \<F>) is shown as "\<F>". A unicode codepoint
> > is available for that: U+2131 SCRIPT CAPITAL F. Could this be improved?
> Thanks for pointing this out; these issues are fixed.
> 
> Also, I have taken the opportunity to add to the theory editor
> an auto-completion box which pops up when you start typing a symbol
> name with \<... and can also be triggered as usual by Ctrl-space.
> 
> Those who have already installed I3P, just use "check for updates".
> 
> Thanks to Makarius for pointing out that there is an official stable
> mapping from symbol encodings to Unicode characters.

I’m not sure what happened, but it seems it broke somehow: I tried to
edit this file:
http://isabelle.in.tum.de/repos/AFP/file/tip/thys/Free-Groups/Isomorphisms.thy
and i3p would fail at \<Z> and \<one> (but not at \<F>). The error
message at \<Z> is:

Inner lexical error at: 𝒵, mult = op +, one = 0::int ⦈
Failed to parse proposition
At command "abbreviation".

so there is clearly some encoding problem. Notice that \<F> and \<Z>
have quite different code points:
\<F>                    code: 0x002131  font: Isabelle
\<Z>                    code: 0x01d4b5  font: Isabelle

All this is on Debian Linux, using a UTF8 locale and with Isabelle
2009-2.


A similar, but not i3p specific, problem is that Isabelle views \<cdot>
as U+22C5 DOT OPERATOR. I have · (U+00B7 MIDDLE DOT) on my keyboard¹,
which causes a lexical error in Isabelle as well. As I hope that never
ever people would want to define · and ⋅ differently in Isabelle, would
it be possible to accept both U+00B7 and U+22C5 for \<cdot>?


Thanks,
Joachim


¹ using this xmodmap line:
keycode  60 = period colon period colon periodcentered division periodcentered


-- 
Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.