Email Gateway (Aug 18 2022 at 12:49): Email Gateway (Aug 18 2022 at 12:49):From: Gergely Buday <gbuday@gmail.com>
Makarius wrote:
Please excuse the ugly look-and-feel of XEmacs, we are trying hard to get
rid of it in the near future.
I'm using fedora 10, the built-in xemacs did not work, gnu emacs did.
What do you mean by getting rid of xemacs? Is the eclipse plugin on the way?
Email Gateway (Aug 18 2022 at 12:49):From: Makarius <makarius@sketis.net>
On Sat, 10 Jan 2009, Gergely Buday wrote:
Makarius wrote:
Please excuse the ugly look-and-feel of XEmacs, we are trying hard to get
rid of it in the near future.I'm using fedora 10, the built-in xemacs did not work, gnu emacs did.
This is also my experience: most xemacs packages of current Linux
distributions are unusable. Many people have switched to GNU Emacs 22 /
Gtk already.
What do you mean by getting rid of xemacs? Is the eclipse plugin on the
way?
First of all, the (unfinished) 4.0 branch of Proof General is for GNU
Emacs only, no longer XEmacs.
Concerning Eclipse, I have personally dismissed it altogether after
extensive comparison with alternatives, notably Netbeans 6.x (not 5.0 or
earlier).
Right now we are working on some new prover interface technology that is
meant to be "generic" to some extend -- it will work with usual Swing
things, and is implemented in Scala/JVM. Our main platform for
experiments is jEdit, which is quite nice and small enough to get things
done relatively quickly.
Makarius
Email Gateway (Aug 18 2022 at 12:49):From: Slawomir Kolodynski <skokodyn@yahoo.com>
Will it have support for mathematical notation (symbols) at
least on the level ProofGeneral/XEmacs provides?
Slawekk
Email Gateway (Aug 18 2022 at 12:49):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 12:49):From: Slawomir Kolodynski <skokodyn@yahoo.com>
You can consider JMathTeX ( http://jmathtex.sourceforge.net/index.html ). It is a GPL licensed library that can be used to display mathematics in Swing components.
Slawekk
Formalmath.org
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Last updated: May 03 2024 at 12:27 UTC