#+TITLE: Isabelle-utils

The [[https://isabelle.in.tum.de/][Isabelle proof assistant]] is usually run inside a modified version of jedit
which enables correct rendering of mathematical symbols, display of current
subgoals, and even interactive tools like ~nitpick~ or ~sledgehammer~.

Unfortunately, jedit has its idiosyncrasies, and generally takes a while to
even start up at all.

This repo is an attempt to make working with isabelle more convenient /outside/
of jedit.

For now, it has two components:
 - a rust crate that converts Isabelle's notation for mathematical symbols to
   unicode (+ a small utility for use in shell scripts)
 - a little shell script (~isabat~) which behaves as a pretty-printing ~less~
   for .thy files, to make e.g. the AFP or HOL readable outside of
   jedit/rendered html files

* Installation
Using nix, just run ~nix-build~.

Without nix, build the ~isabelle2unicode~ crate, and make the resulting binary
available on your path. Also make sure you have ~bat~ installed.

In either case, place the ~isabelle.sublime-syntax~ file in bat's config dir
to make the highlighter work (follow the hints printed by ~isabat~ or take a
look at [[https://github.com/sharkdp/bat#adding-new-syntaxes--language-definitions][bat's readme]] for details).

* Credits
The ~symbols~ file is taken directly from Isabelle's latest release. Much of
the list of keywords given in the ~isabelle.sublime-syntax~ file was copied
from the output of ~isabelle vscode_grammar~.