Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] First public release of my VIm-Interface for I...

Email Gateway (Aug 18 2022 at 12:33):

From: Jens-Wolfhard Schicke <drahflow@gmx.de>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi,

as a die hard VIm-User who wanted to use Isabelle/HOL for his diploma thesis,
I have (with some help from Timothy Burke) produced the following file:

http://jens.schicke.hvf-bs.net/data/isabelle-vim.tbz2

While not as elaborate as XSymbols+ProofGeneral, I use it for the proof work of
my thesis and find it comfortable enough.

A mini-HowTo is contained in the above archive.

Features:

• • Unicode math symbols for display
• • Insert mappings for said unicode symbols
• • Perl-script hack to connect a VIm window to a stateful Isabelle instance
• • minimal and non-exact syntax highlighting
• • trivial to install, should work with any current VIm version (I didn't test though)

Best Regards,
Jens-Wolfhard Schicke
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)

iEYEARECAAYFAkj8QR0ACgkQzhchXT4RR5BnzgCgipHgQ+KXD1oEFDzm8DFCcakC
RmQAnRNNnJ5Liw5pTenycUKPeWDmh6uE
=3poD
-----END PGP SIGNATURE-----

Email Gateway (Aug 18 2022 at 12:33):

From: Makarius <makarius@sketis.net>
Although I am not a user of vi, I've had a brief look at it.

Concerning unicode rendering of Isabelle symbols, you might be interested
in the semi-official table
http://isabelle.in.tum.de/repos/isabelle/file/tip/etc/symbols

Also see the still somewhat experimental IsabelleMono font at
http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/isabelle-fonts/ which is
also based on Vera, but fills most mathematical code points with glyphs
from Computer Modern (TeX).

In your "isabelle" script, did you actually mean to invoke the tty
interface, which includes a readline wrapper (if configured)? A raw
process with Isabelle/Isar toplevel can be started like this:

isabelle-process -I

Makarius

Last updated: May 03 2024 at 08:18 UTC