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 
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





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