update readme

1 files changed, 33 insertions, 54 deletions

diff --git a/Readme.org b/Readme.org
index 5b6f8ba..8fcca3f 100644
--- a/Readme.org
+++ b/Readme.org
@@ -1,54 +1,33 @@
-#+TITLE: Isabelle-dump
-
-The [[https://isabelle.in.tum.de/][Isabelle proof assistant]] uses lots of mathematical symbols
-in its notation, yet still saves its theories as ASCII files,
-using lots of escape sequences, e.g. a simple lemma from set
-theory (taken from ~HOL/Set.thy~) might be written like this:
-
-#+begin_src
-lemma set_eq_iff: "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
-  by (auto intro:set_eqI)
-#+end_src
-
-Luckily, unicode contains a lot of symbols. Piped through
-~isabelle-dump~, it looks like this:
-
-#+begin_src
-lemma set_eq_iff: "A = B ⟷ (∀x. x ∈ A ⟷ x ∈ B)"
-   by (auto intro:set_eqI)
-#+end_src
-
-* Usage
-~isabelle-dump~ takes no arguments for now. Use it like this:
-
-#+begin_src sh
-cat /path/to/theory.thy | isabelle-dump | less
-#+end_src sh
-
-Since much of isabelle's syntax follows conventions derived from
-the ML language family, you can additionally get rudimentary
-syntax highlighting by using [[https://github.com/sharkdp/bat][bat]] with its SML highlighter:
-
-#+begin_src sh
-cat /path/to/theory.thy | isabelle-dump | bat -l sml
-#+end_src
-
-* Limitations
-For now, this assumes that each escape sequence stands on its
-own, and ignores things like superscript, which are a modifier
-(which will be printed as e.g. x⇧2 instead of the more correct x²
-– though sub/superscript in unicode [[https://en.wikipedia.org/wiki/Unicode_subscripts_and_superscripts][is a giant mess in general]]).
-
-It also only knows about escape sequences, and has no idea at all
-about proofs, functions, or any other bits of syntax.
-
-~isabelle-dump~ was written over some hours in which I also did
-other things, so don't be suprised if you manage to make it panic
-or otherwise fail for some input – for test purposes the entire
-HOL library was piped through it at least once, but there may
-still be some edge cases I haven't thought of.
-
-Lastly, it has a dependency closure including over 100 crates,
-which may be considered excessive [citation needed] for something
-that could also be implemented using only the standard liberay
-and nothing else. I mostly wanted to try working with [[https://softdevteam.github.io/grmtools/master/book/quickstart.html][grmtools]] ...
+#+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~.