Re: [isabelle] xemacs
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and