*To*: Slawomir Kolodynski <skokodyn at yahoo.com>*Subject*: Re: [isabelle] xemacs*From*: Makarius <makarius at sketis.net>*Date*: Sat, 10 Jan 2009 23:20:25 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <506088.7892.qm@web30807.mail.mud.yahoo.com>*References*: <506088.7892.qm@web30807.mail.mud.yahoo.com>

On Sat, 10 Jan 2009, Slawomir Kolodynski wrote: > > Right now we are working on some new prover interface technology > > Will it have support for mathematical notation (symbols) at least on the > level ProofGeneral/XEmacs provides? Basically yes, although some details will be different. First of all, native Isabelle symbols like \<forall> will remain as is -- they provide an infinite store of symbols. Note that the usual set of "standard" symbols is just a convention. E.g. one can expect \<forall> to look like \forall in LaTeX, while being able to invent new symbols as required for your application. For the JVM platform, we already have a basic translation scheme to use unicode as a poor-man's rendering mechanism for Isabelle text. One could even imagine an "isabelle" encoding for JVM that does the job seamlessly when reading/writing files. Having standard conformant unicode code-points in memory is fine, but actual display on the screen is still not fully settled. One cannot really count on having the usual mathematical glyphs available on the fonts being installed on a given system. Until the Stix fonts come out in maybe 5 more years :-) we have our own homegrown unicode font, based on TeX glyhps + Bitstream Vera (still ugly, but much less ugly than Emacs/XSymbols). Input methods for mathematical symbols are yet another thing. On jEdit it is reasonable easy to use either "abbreviations" or context-sensitive "completion". E.g. you type something like ==> and get the unicode version of \<Longrightarrow> as expected. You can also copy-paste these things then do a jEdit hypersearch over the file-system, for example. (This won't work with Emacs/XSymbol, of course.) If you know about more advanced input tools for mathematics for the Swing platform, I would be interested to hear about it. Of course it needs to be free software. Makarius

**Follow-Ups**:**Re: [isabelle] xemacs***From:*Slawomir Kolodynski

**References**:**Re: [isabelle] xemacs***From:*Slawomir Kolodynski

- Previous by Date: Re: [isabelle] xemacs
- Next by Date: Re: [isabelle] xemacs
- Previous by Thread: Re: [isabelle] xemacs
- Next by Thread: Re: [isabelle] xemacs
- Cl-isabelle-users January 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list