initial commit

16 files changed, 1699 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..e420ee4
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+target/*
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 0000000..2f0d1ca
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,464 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+[[package]]
+name = "aho-corasick"
+version = "0.7.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1e37cfd5e7657ada45f742d6e99ca5788580b5c529dc78faf11ece6dc702656f"
+dependencies = [
+ "memchr",
+]
+
+[[package]]
+name = "autocfg"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a"
+
+[[package]]
+name = "bincode"
+version = "1.3.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b1f45e9417d87227c7a56d22e471c6206462cba514c7590c09aff4cf6d1ddcad"
+dependencies = [
+ "serde",
+]
+
+[[package]]
+name = "bitflags"
+version = "1.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693"
+
+[[package]]
+name = "cactus"
+version = "1.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf034765b7d19a011c6d619e880582bf95e8186b580e6fab56589872dd87dcf5"
+
+[[package]]
+name = "cfg-if"
+version = "0.1.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4785bdd1c96b2a846b2bd7cc02e86b6b3dbf14e7e53446c4f54c92a361040822"
+
+[[package]]
+name = "cfg-if"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
+
+[[package]]
+name = "cfgrammar"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c63bd74c5d141c1ff743fad7e1c56e50d934131f503b048324b0eb68549376d8"
+dependencies = [
+ "indexmap",
+ "lazy_static",
+ "num-traits",
+ "regex",
+ "serde",
+ "vob",
+]
+
+[[package]]
+name = "chrono"
+version = "0.4.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "670ad68c9088c2a963aaa298cb369688cf3f9465ce5e2d4ca10e6e0098a1ce73"
+dependencies = [
+ "libc",
+ "num-integer",
+ "num-traits",
+ "time",
+ "winapi",
+]
+
+[[package]]
+name = "filetime"
+version = "0.2.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1d34cfa13a63ae058bfa601fe9e313bbdb3746427c1459185464ce0fcf62e1e8"
+dependencies = [
+ "cfg-if 1.0.0",
+ "libc",
+ "redox_syscall",
+ "winapi",
+]
+
+[[package]]
+name = "fnv"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
+
+[[package]]
+name = "getopts"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5"
+dependencies = [
+ "unicode-width",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.9.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7afe4a420e3fe79967a00898cc1f4db7c8a49a9333a29f8a4bd76a253d5cd04"
+
+[[package]]
+name = "indexmap"
+version = "1.6.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "824845a0bf897a9042383849b02c1bc219c2383772efcd5c6f9766fa4b81aef3"
+dependencies = [
+ "autocfg",
+ "hashbrown",
+]
+
+[[package]]
+name = "isabelle-dump"
+version = "0.1.0"
+dependencies = [
+ "cfgrammar",
+ "lrlex",
+ "lrpar",
+ "symbolmacro",
+]
+
+[[package]]
+name = "lazy_static"
+version = "1.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
+
+[[package]]
+name = "libc"
+version = "0.2.97"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "12b8adadd720df158f4d70dfe7ccc6adb0472d7c55ca83445f6a5ab3e36f8fb6"
+
+[[package]]
+name = "lrlex"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cccc0ee64acad6ea2e83d152de81c845523a8eedbed67cad6ebeec7058e87c1a"
+dependencies = [
+ "getopts",
+ "lazy_static",
+ "lrpar",
+ "num-traits",
+ "regex",
+ "try_from",
+]
+
+[[package]]
+name = "lrpar"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "56b920e6cef1188595dc4e6e3ffcc9a81ffc9801af5582df49fa3ade23350f71"
+dependencies = [
+ "bincode",
+ "cactus",
+ "cfgrammar",
+ "filetime",
+ "indexmap",
+ "lazy_static",
+ "lrtable",
+ "num-traits",
+ "packedvec",
+ "regex",
+ "serde",
+ "static_assertions",
+ "vergen",
+ "vob",
+]
+
+[[package]]
+name = "lrtable"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "48212e9df591939f87311b824ff21ea93310f8ec2b06459139bdbd7feb067ad2"
+dependencies = [
+ "cfgrammar",
+ "fnv",
+ "num-traits",
+ "serde",
+ "sparsevec",
+ "static_assertions",
+ "try_from",
+ "vob",
+]
+
+[[package]]
+name = "memchr"
+version = "2.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b16bd47d9e329435e309c58469fe0791c2d0d1ba96ec0954152a5ae2b04387dc"
+
+[[package]]
+name = "num-integer"
+version = "0.1.44"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d2cc698a63b549a70bc047073d2949cce27cd1c7b0a4a862d08a8031bc2801db"
+dependencies = [
+ "autocfg",
+ "num-traits",
+]
+
+[[package]]
+name = "num-traits"
+version = "0.2.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9a64b1ec5cda2586e284722486d802acf1f7dbdc623e2bfc57e65ca1cd099290"
+dependencies = [
+ "autocfg",
+]
+
+[[package]]
+name = "packedvec"
+version = "1.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "330ecfcb0ad33d2e3fb49bc09742dab081112272c8252c5b5bf760f96d8d2b7f"
+dependencies = [
+ "num-traits",
+ "serde",
+]
+
+[[package]]
+name = "pest"
+version = "2.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "10f4872ae94d7b90ae48754df22fd42ad52ce740b8f370b03da4835417403e53"
+dependencies = [
+ "ucd-trie",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0d8caf72986c1a598726adc988bb5984792ef84f5ee5aa50209145ee8077038"
+dependencies = [
+ "unicode-xid",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c3d0b9745dc2debf507c8422de05d7226cc1f0644216dfdfead988f9b1ab32a7"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "redox_syscall"
+version = "0.2.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5ab49abadf3f9e1c4bc499e8845e152ad87d2ad2d30371841171169e9d75feee"
+dependencies = [
+ "bitflags",
+]
+
+[[package]]
+name = "regex"
+version = "1.5.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d07a8629359eb56f1e2fb1652bb04212c072a87ba68546a04065d525673ac461"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-syntax"
+version = "0.6.25"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b"
+
+[[package]]
+name = "rustc_version"
+version = "0.3.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0dfe2087c51c460008730de8b57e6a320782fbfb312e1f4d520e6c6fae155ee"
+dependencies = [
+ "semver 0.11.0",
+]
+
+[[package]]
+name = "rustc_version"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bfa0f585226d2e68097d4f95d113b15b83a82e819ab25717ec0590d9584ef366"
+dependencies = [
+ "semver 1.0.3",
+]
+
+[[package]]
+name = "semver"
+version = "0.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f301af10236f6df4160f7c3f04eec6dbc70ace82d23326abad5edee88801c6b6"
+dependencies = [
+ "semver-parser",
+]
+
+[[package]]
+name = "semver"
+version = "1.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5f3aac57ee7f3272d8395c6e4f502f434f0e289fcd62876f70daa008c20dcabe"
+
+[[package]]
+name = "semver-parser"
+version = "0.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "00b0bef5b7f9e0df16536d3961cfb6e84331c065b4066afb39768d0e319411f7"
+dependencies = [
+ "pest",
+]
+
+[[package]]
+name = "serde"
+version = "1.0.126"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec7505abeacaec74ae4778d9d9328fe5a5d04253220a85c4ee022239fc996d03"
+dependencies = [
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_derive"
+version = "1.0.126"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "963a7dbc9895aeac7ac90e74f34a5d5261828f79df35cbed41e10189d3804d43"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "sparsevec"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a182a1fc36753f8a2e3eea04cc3cd28065d2949cbda1e3a453cd183dace42bbb"
+dependencies = [
+ "num-traits",
+ "packedvec",
+ "serde",
+ "vob",
+]
+
+[[package]]
+name = "static_assertions"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f"
+
+[[package]]
+name = "symbolmacro"
+version = "0.1.0"
+
+[[package]]
+name = "syn"
+version = "1.0.73"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f71489ff30030d2ae598524f61326b902466f72a0fb1a8564c001cc63425bcc7"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-xid",
+]
+
+[[package]]
+name = "time"
+version = "0.1.44"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6db9e6914ab8b1ae1c260a4ae7a49b6c5611b40328a735b21862567685e73255"
+dependencies = [
+ "libc",
+ "wasi",
+ "winapi",
+]
+
+[[package]]
+name = "try_from"
+version = "0.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "283d3b89e1368717881a9d51dad843cc435380d8109c9e47d38780a324698d8b"
+dependencies = [
+ "cfg-if 0.1.10",
+]
+
+[[package]]
+name = "ucd-trie"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "56dee185309b50d1f11bfedef0fe6d036842e3fb77413abef29f8f8d1c5d4c1c"
+
+[[package]]
+name = "unicode-width"
+version = "0.1.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9337591893a19b88d8d87f2cec1e73fad5cdfd10e5a6f349f498ad6ea2ffb1e3"
+
+[[package]]
+name = "unicode-xid"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8ccb82d61f80a663efe1f787a51b16b5a51e3314d6ac365b08639f52387b33f3"
+
+[[package]]
+name = "vergen"
+version = "3.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e7141e445af09c8919f1d5f8a20dae0b20c3b57a45dee0d5823c6ed5d237f15a"
+dependencies = [
+ "bitflags",
+ "chrono",
+ "rustc_version 0.4.0",
+]
+
+[[package]]
+name = "vob"
+version = "2.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8af6d79df9ae93c259d5d076bad5741c3dd650bc10a13dd83704b0c29a280f15"
+dependencies = [
+ "num-traits",
+ "rustc_version 0.3.3",
+ "serde",
+]
+
+[[package]]
+name = "wasi"
+version = "0.10.0+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1a143597ca7c7793eff794def352d41792a93c481eb1042423ff7ff72ba2c31f"
+
+[[package]]
+name = "winapi"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
+dependencies = [
+ "winapi-i686-pc-windows-gnu",
+ "winapi-x86_64-pc-windows-gnu",
+]
+
+[[package]]
+name = "winapi-i686-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
+
+[[package]]
+name = "winapi-x86_64-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..4e1b615
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,2 @@
+[workspace]
+members = ["isabelle-dump", "symbolmacro"]
diff --git a/Readme.org b/Readme.org
new file mode 100644
index 0000000..5b6f8ba
--- /dev/null
+++ b/Readme.org
@@ -0,0 +1,54 @@
+#+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]] ...
diff --git a/isabelle-dump/Cargo.lock b/isabelle-dump/Cargo.lock
new file mode 100644
index 0000000..2f0d1ca
--- /dev/null
+++ b/isabelle-dump/Cargo.lock
@@ -0,0 +1,464 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+[[package]]
+name = "aho-corasick"
+version = "0.7.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1e37cfd5e7657ada45f742d6e99ca5788580b5c529dc78faf11ece6dc702656f"
+dependencies = [
+ "memchr",
+]
+
+[[package]]
+name = "autocfg"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a"
+
+[[package]]
+name = "bincode"
+version = "1.3.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b1f45e9417d87227c7a56d22e471c6206462cba514c7590c09aff4cf6d1ddcad"
+dependencies = [
+ "serde",
+]
+
+[[package]]
+name = "bitflags"
+version = "1.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693"
+
+[[package]]
+name = "cactus"
+version = "1.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf034765b7d19a011c6d619e880582bf95e8186b580e6fab56589872dd87dcf5"
+
+[[package]]
+name = "cfg-if"
+version = "0.1.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4785bdd1c96b2a846b2bd7cc02e86b6b3dbf14e7e53446c4f54c92a361040822"
+
+[[package]]
+name = "cfg-if"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
+
+[[package]]
+name = "cfgrammar"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c63bd74c5d141c1ff743fad7e1c56e50d934131f503b048324b0eb68549376d8"
+dependencies = [
+ "indexmap",
+ "lazy_static",
+ "num-traits",
+ "regex",
+ "serde",
+ "vob",
+]
+
+[[package]]
+name = "chrono"
+version = "0.4.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "670ad68c9088c2a963aaa298cb369688cf3f9465ce5e2d4ca10e6e0098a1ce73"
+dependencies = [
+ "libc",
+ "num-integer",
+ "num-traits",
+ "time",
+ "winapi",
+]
+
+[[package]]
+name = "filetime"
+version = "0.2.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1d34cfa13a63ae058bfa601fe9e313bbdb3746427c1459185464ce0fcf62e1e8"
+dependencies = [
+ "cfg-if 1.0.0",
+ "libc",
+ "redox_syscall",
+ "winapi",
+]
+
+[[package]]
+name = "fnv"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
+
+[[package]]
+name = "getopts"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5"
+dependencies = [
+ "unicode-width",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.9.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7afe4a420e3fe79967a00898cc1f4db7c8a49a9333a29f8a4bd76a253d5cd04"
+
+[[package]]
+name = "indexmap"
+version = "1.6.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "824845a0bf897a9042383849b02c1bc219c2383772efcd5c6f9766fa4b81aef3"
+dependencies = [
+ "autocfg",
+ "hashbrown",
+]
+
+[[package]]
+name = "isabelle-dump"
+version = "0.1.0"
+dependencies = [
+ "cfgrammar",
+ "lrlex",
+ "lrpar",
+ "symbolmacro",
+]
+
+[[package]]
+name = "lazy_static"
+version = "1.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
+
+[[package]]
+name = "libc"
+version = "0.2.97"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "12b8adadd720df158f4d70dfe7ccc6adb0472d7c55ca83445f6a5ab3e36f8fb6"
+
+[[package]]
+name = "lrlex"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cccc0ee64acad6ea2e83d152de81c845523a8eedbed67cad6ebeec7058e87c1a"
+dependencies = [
+ "getopts",
+ "lazy_static",
+ "lrpar",
+ "num-traits",
+ "regex",
+ "try_from",
+]
+
+[[package]]
+name = "lrpar"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "56b920e6cef1188595dc4e6e3ffcc9a81ffc9801af5582df49fa3ade23350f71"
+dependencies = [
+ "bincode",
+ "cactus",
+ "cfgrammar",
+ "filetime",
+ "indexmap",
+ "lazy_static",
+ "lrtable",
+ "num-traits",
+ "packedvec",
+ "regex",
+ "serde",
+ "static_assertions",
+ "vergen",
+ "vob",
+]
+
+[[package]]
+name = "lrtable"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "48212e9df591939f87311b824ff21ea93310f8ec2b06459139bdbd7feb067ad2"
+dependencies = [
+ "cfgrammar",
+ "fnv",
+ "num-traits",
+ "serde",
+ "sparsevec",
+ "static_assertions",
+ "try_from",
+ "vob",
+]
+
+[[package]]
+name = "memchr"
+version = "2.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b16bd47d9e329435e309c58469fe0791c2d0d1ba96ec0954152a5ae2b04387dc"
+
+[[package]]
+name = "num-integer"
+version = "0.1.44"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d2cc698a63b549a70bc047073d2949cce27cd1c7b0a4a862d08a8031bc2801db"
+dependencies = [
+ "autocfg",
+ "num-traits",
+]
+
+[[package]]
+name = "num-traits"
+version = "0.2.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9a64b1ec5cda2586e284722486d802acf1f7dbdc623e2bfc57e65ca1cd099290"
+dependencies = [
+ "autocfg",
+]
+
+[[package]]
+name = "packedvec"
+version = "1.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "330ecfcb0ad33d2e3fb49bc09742dab081112272c8252c5b5bf760f96d8d2b7f"
+dependencies = [
+ "num-traits",
+ "serde",
+]
+
+[[package]]
+name = "pest"
+version = "2.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "10f4872ae94d7b90ae48754df22fd42ad52ce740b8f370b03da4835417403e53"
+dependencies = [
+ "ucd-trie",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0d8caf72986c1a598726adc988bb5984792ef84f5ee5aa50209145ee8077038"
+dependencies = [
+ "unicode-xid",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c3d0b9745dc2debf507c8422de05d7226cc1f0644216dfdfead988f9b1ab32a7"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "redox_syscall"
+version = "0.2.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5ab49abadf3f9e1c4bc499e8845e152ad87d2ad2d30371841171169e9d75feee"
+dependencies = [
+ "bitflags",
+]
+
+[[package]]
+name = "regex"
+version = "1.5.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d07a8629359eb56f1e2fb1652bb04212c072a87ba68546a04065d525673ac461"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-syntax"
+version = "0.6.25"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b"
+
+[[package]]
+name = "rustc_version"
+version = "0.3.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0dfe2087c51c460008730de8b57e6a320782fbfb312e1f4d520e6c6fae155ee"
+dependencies = [
+ "semver 0.11.0",
+]
+
+[[package]]
+name = "rustc_version"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bfa0f585226d2e68097d4f95d113b15b83a82e819ab25717ec0590d9584ef366"
+dependencies = [
+ "semver 1.0.3",
+]
+
+[[package]]
+name = "semver"
+version = "0.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f301af10236f6df4160f7c3f04eec6dbc70ace82d23326abad5edee88801c6b6"
+dependencies = [
+ "semver-parser",
+]
+
+[[package]]
+name = "semver"
+version = "1.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5f3aac57ee7f3272d8395c6e4f502f434f0e289fcd62876f70daa008c20dcabe"
+
+[[package]]
+name = "semver-parser"
+version = "0.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "00b0bef5b7f9e0df16536d3961cfb6e84331c065b4066afb39768d0e319411f7"
+dependencies = [
+ "pest",
+]
+
+[[package]]
+name = "serde"
+version = "1.0.126"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec7505abeacaec74ae4778d9d9328fe5a5d04253220a85c4ee022239fc996d03"
+dependencies = [
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_derive"
+version = "1.0.126"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "963a7dbc9895aeac7ac90e74f34a5d5261828f79df35cbed41e10189d3804d43"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "sparsevec"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a182a1fc36753f8a2e3eea04cc3cd28065d2949cbda1e3a453cd183dace42bbb"
+dependencies = [
+ "num-traits",
+ "packedvec",
+ "serde",
+ "vob",
+]
+
+[[package]]
+name = "static_assertions"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f"
+
+[[package]]
+name = "symbolmacro"
+version = "0.1.0"
+
+[[package]]
+name = "syn"
+version = "1.0.73"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f71489ff30030d2ae598524f61326b902466f72a0fb1a8564c001cc63425bcc7"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-xid",
+]
+
+[[package]]
+name = "time"
+version = "0.1.44"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6db9e6914ab8b1ae1c260a4ae7a49b6c5611b40328a735b21862567685e73255"
+dependencies = [
+ "libc",
+ "wasi",
+ "winapi",
+]
+
+[[package]]
+name = "try_from"
+version = "0.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "283d3b89e1368717881a9d51dad843cc435380d8109c9e47d38780a324698d8b"
+dependencies = [
+ "cfg-if 0.1.10",
+]
+
+[[package]]
+name = "ucd-trie"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "56dee185309b50d1f11bfedef0fe6d036842e3fb77413abef29f8f8d1c5d4c1c"
+
+[[package]]
+name = "unicode-width"
+version = "0.1.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9337591893a19b88d8d87f2cec1e73fad5cdfd10e5a6f349f498ad6ea2ffb1e3"
+
+[[package]]
+name = "unicode-xid"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8ccb82d61f80a663efe1f787a51b16b5a51e3314d6ac365b08639f52387b33f3"
+
+[[package]]
+name = "vergen"
+version = "3.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e7141e445af09c8919f1d5f8a20dae0b20c3b57a45dee0d5823c6ed5d237f15a"
+dependencies = [
+ "bitflags",
+ "chrono",
+ "rustc_version 0.4.0",
+]
+
+[[package]]
+name = "vob"
+version = "2.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8af6d79df9ae93c259d5d076bad5741c3dd650bc10a13dd83704b0c29a280f15"
+dependencies = [
+ "num-traits",
+ "rustc_version 0.3.3",
+ "serde",
+]
+
+[[package]]
+name = "wasi"
+version = "0.10.0+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1a143597ca7c7793eff794def352d41792a93c481eb1042423ff7ff72ba2c31f"
+
+[[package]]
+name = "winapi"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
+dependencies = [
+ "winapi-i686-pc-windows-gnu",
+ "winapi-x86_64-pc-windows-gnu",
+]
+
+[[package]]
+name = "winapi-i686-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
+
+[[package]]
+name = "winapi-x86_64-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
diff --git a/isabelle-dump/Cargo.toml b/isabelle-dump/Cargo.toml
new file mode 100644
index 0000000..924737f
--- /dev/null
+++ b/isabelle-dump/Cargo.toml
@@ -0,0 +1,17 @@
+[package]
+name = "isabelle-dump"
+version = "0.1.0"
+authors = ["stuebinm <stuebinm@disroot.org>"]
+edition = "2018"
+
+
+[build-dependencies]
+cfgrammar = "0.10"
+lrlex = "0.10"
+lrpar = "0.10"
+
+[dependencies]
+cfgrammar = "0.10"
+lrlex = "0.10"
+lrpar = "0.10"
+symbolmacro = { path = "../symbolmacro", version = "0.1" }
diff --git a/isabelle-dump/build.rs b/isabelle-dump/build.rs
new file mode 100644
index 0000000..b11761d
--- /dev/null
+++ b/isabelle-dump/build.rs
@@ -0,0 +1,13 @@
+use cfgrammar::yacc::YaccKind;
+use lrlex::LexerBuilder;
+use lrpar::{CTParserBuilder};
+
+fn main() -> Result<(), Box<dyn std::error::Error>> {
+    let lex_rule_ids_map = CTParserBuilder::new()
+        .yacckind(YaccKind::Grmtools)
+        .process_file_in_src("calc.y")?;
+    LexerBuilder::new()
+        .rule_ids_map(lex_rule_ids_map)
+        .process_file_in_src("calc.l")?;
+    Ok(())
+}
diff --git a/isabelle-dump/src/calc.l b/isabelle-dump/src/calc.l
new file mode 100644
index 0000000..2bf98dc
--- /dev/null
+++ b/isabelle-dump/src/calc.l
@@ -0,0 +1,5 @@
+%%
+\\ "AOPEN"
+< "LT"
+<[^\\<>]+> "NAME"
+[^<\\][^\\]* "TEXT"
diff --git a/isabelle-dump/src/calc.y b/isabelle-dump/src/calc.y
new file mode 100644
index 0000000..2dd3bd3
--- /dev/null
+++ b/isabelle-dump/src/calc.y
@@ -0,0 +1,54 @@
+%start AbbrList
+
+%%
+
+AbbrList -> Result<Vec<Isabelle>, ()>:
+   Text { Ok(vec![Isabelle::Text($1?)]) }
+   | Abbr { Ok(vec![Isabelle::Symbol($1?)]) }
+   | AbbrList Abbr
+      {
+          let mut $1 = $1?;
+          $1.push(Isabelle::Symbol($2?));
+          Ok($1)
+      }
+   | AbbrList Text
+     {
+          let mut $1 = $1?;
+          $1.push(Isabelle::Text($2?));
+          Ok($1)
+     }
+   ;
+
+Abbr -> Result<String, ()>:
+      'AOPEN' Name  { Ok($2?) }
+    ;
+
+Text -> Result<String, ()>:
+  'TEXT'
+      {
+        let v = $1.map_err(|_| ())?;
+        Ok($lexer.span_str(v.span()).to_string())
+      }
+  | 'AOPEN'
+      {
+        //let v = $2.map_err(|_| ())?;
+        Ok("\\".to_string())
+      }
+  | 'LT'
+      {
+        //let v = $2.map_err(|_| ())?;
+        Ok("<".to_string()) //format!("<{}", $lexer.span_str(v.span())))
+      }
+  ;
+
+Name -> Result<String, ()>:
+  'NAME'
+      {
+        let v = $1.map_err(|_| ())?;
+        let name = $lexer.span_str(v.span());
+        Ok(name[1..name.len()-1].to_string())
+      }
+  ;
+%%
+
+use crate::Isabelle;
diff --git a/isabelle-dump/src/main.rs b/isabelle-dump/src/main.rs
new file mode 100644
index 0000000..891108f
--- /dev/null
+++ b/isabelle-dump/src/main.rs
@@ -0,0 +1,71 @@
+use std::io::{self, BufRead, Write};
+
+use lrlex::lrlex_mod;
+use lrpar::lrpar_mod;
+
+#[derive(Debug)]
+pub enum Isabelle {
+    Symbol(String),
+    Text(String),
+}
+
+
+lrlex_mod!("calc.l");
+lrpar_mod!("calc.y");
+
+
+symbolmacro::make_symbols!();
+
+
+fn main() {
+    // Get the `LexerDef` for the `calc` language.
+    let lexerdef = calc_l::lexerdef();
+    let stdin = io::stdin();
+    loop {
+        io::stdout().flush().ok();
+        match stdin.lock().lines().next() {
+            Some(Ok(ref l)) => {
+                if l.trim().is_empty() {
+                    println!("");
+                    continue;
+                }
+                let lexer = lexerdef.lexer(l);
+                let (res, errs) = calc_y::parse(&lexer);
+                for e in errs {
+                    eprintln!(
+                        "{}",
+                        e.pp(&lexer, &calc_y::token_epp)
+                    );
+                }
+                match res {
+                    Some(r) => {
+                        //eprintln!("Result: {:?}", r);
+                        let rendered = r
+                            .unwrap()
+                            .iter()
+                            .map(|token| match token {
+                                Isabelle::Text(ref t) =>
+                                    t,
+                                Isabelle::Symbol(name) =>
+                                    symbol(name)
+                                    .unwrap_or_else(|| {
+                                        Box::leak(
+                                            format!("\\<{}>", name)
+                                                .into()
+                                        )
+                                    })
+                            })
+                            .collect::<Vec<&str>>()
+                            .join("");
+                        println!("{}", rendered);
+                    }
+                    _ => {
+                        eprintln!("could not parse file (probably spurious \\, <, or >)");
+                        std::process::exit(1);
+                    }
+                }
+            }
+            _ => break,
+        }
+    }
+}
diff --git a/isabelle-licence b/isabelle-licence
new file mode 100644
index 0000000..48d5703
--- /dev/null
+++ b/isabelle-licence
@@ -0,0 +1,38 @@
+(applicable for the symbols file)
+
+ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
+
+Copyright (c) 1986-2021,
+  University of Cambridge,
+  Technische Universitaet Muenchen,
+  and contributors.
+
+  All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+* Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+* Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+* Neither the name of the University of Cambridge or the Technische
+Universitaet Muenchen nor the names of their contributors may be used
+to endorse or promote products derived from this software without
+specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/symbolmacro/.gitignore b/symbolmacro/.gitignore
new file mode 100644
index 0000000..ea8c4bf
--- /dev/null
+++ b/symbolmacro/.gitignore
@@ -0,0 +1 @@
+/target
diff --git a/symbolmacro/Cargo.lock b/symbolmacro/Cargo.lock
new file mode 100644
index 0000000..1ed48a4
--- /dev/null
+++ b/symbolmacro/Cargo.lock
@@ -0,0 +1,5 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+[[package]]
+name = "symbolmacro"
+version = "0.1.0"
diff --git a/symbolmacro/Cargo.toml b/symbolmacro/Cargo.toml
new file mode 100644
index 0000000..78ad418
--- /dev/null
+++ b/symbolmacro/Cargo.toml
@@ -0,0 +1,11 @@
+[package]
+name = "symbolmacro"
+version = "0.1.0"
+authors = ["stuebinm <stuebinm@disroot.org>"]
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+[lib]
+proc-macro = true
+
+[dependencies]
diff --git a/symbolmacro/src/lib.rs b/symbolmacro/src/lib.rs
new file mode 100644
index 0000000..f99ccd9
--- /dev/null
+++ b/symbolmacro/src/lib.rs
@@ -0,0 +1,53 @@
+
+extern crate proc_macro;
+
+use proc_macro::TokenStream;
+use std::{collections::HashMap, fs::File, io::BufReader};
+use std::io::prelude::*;
+
+
+
+fn fetchsymbols() -> HashMap<String, char> {
+    // who needs obvious filepaths, anyways?
+    let filename = "symbols";
+    let file = File::open(filename).unwrap();
+    let reader = BufReader::new(file);
+
+    reader.lines()
+          .filter_map(|l| l.ok())
+          .filter_map(|l| {
+              let segments: Vec<&str> = l
+                  .split_whitespace()
+                  .collect();
+              match segments[..] {
+                  [] => None,
+                  [s,"code:",code,..] => {
+                      let codepoint = u32::from_str_radix(&code[2..], 16).ok()?;
+                      let unichar = std::char::from_u32(codepoint)?;
+                      Some((s[2..s.len()-1].to_string(), unichar))
+                  },
+                  _ => None,
+              }
+          })
+          .collect::<HashMap<String,char>>()
+}
+
+
+// rust macros are a strange kind of horrible, tbh
+#[proc_macro]
+pub fn make_symbols(_item: TokenStream) -> TokenStream {
+    let symbols = fetchsymbols();
+
+    format!(
+        "fn symbol(key: &str) -> Option<&'static str> {{
+          match key {{
+             {}
+             _ => None
+          }}
+        }}",
+        symbols.iter()
+               .map(|(k,v)| format!("\"{}\" => Some(\"{}\"),",k,v))
+               .collect::<Vec<_>>()
+               .join("\n")
+    ).parse().unwrap()
+}
diff --git a/symbols b/symbols
new file mode 100644
index 0000000..96589d1
--- /dev/null
+++ b/symbols
@@ -0,0 +1,446 @@
+# file taken from the official isabelle distribution
+# available at isabelle.in.tum.de
+# Default interpretation of some Isabelle symbols
+
+\<zero>                 code: 0x01d7ec  group: digit
+\<one>                  code: 0x01d7ed  group: digit
+\<two>                  code: 0x01d7ee  group: digit
+\<three>                code: 0x01d7ef  group: digit
+\<four>                 code: 0x01d7f0  group: digit
+\<five>                 code: 0x01d7f1  group: digit
+\<six>                  code: 0x01d7f2  group: digit
+\<seven>                code: 0x01d7f3  group: digit
+\<eight>                code: 0x01d7f4  group: digit
+\<nine>                 code: 0x01d7f5  group: digit
+\<A>                    code: 0x01d49c  group: letter
+\<B>                    code: 0x00212c  group: letter
+\<C>                    code: 0x01d49e  group: letter
+\<D>                    code: 0x01d49f  group: letter
+\<E>                    code: 0x002130  group: letter
+\<F>                    code: 0x002131  group: letter
+\<G>                    code: 0x01d4a2  group: letter
+\<H>                    code: 0x00210b  group: letter
+\<I>                    code: 0x002110  group: letter
+\<J>                    code: 0x01d4a5  group: letter
+\<K>                    code: 0x01d4a6  group: letter
+\<L>                    code: 0x002112  group: letter
+\<M>                    code: 0x002133  group: letter
+\<N>                    code: 0x01d4a9  group: letter
+\<O>                    code: 0x01d4aa  group: letter
+\<P>                    code: 0x01d4ab  group: letter
+\<Q>                    code: 0x01d4ac  group: letter
+\<R>                    code: 0x00211b  group: letter
+\<S>                    code: 0x01d4ae  group: letter
+\<T>                    code: 0x01d4af  group: letter
+\<U>                    code: 0x01d4b0  group: letter
+\<V>                    code: 0x01d4b1  group: letter
+\<W>                    code: 0x01d4b2  group: letter
+\<X>                    code: 0x01d4b3  group: letter
+\<Y>                    code: 0x01d4b4  group: letter
+\<Z>                    code: 0x01d4b5  group: letter
+\<a>                    code: 0x01d5ba  group: letter
+\<b>                    code: 0x01d5bb  group: letter
+\<c>                    code: 0x01d5bc  group: letter
+\<d>                    code: 0x01d5bd  group: letter
+\<e>                    code: 0x01d5be  group: letter
+\<f>                    code: 0x01d5bf  group: letter
+\<g>                    code: 0x01d5c0  group: letter
+\<h>                    code: 0x01d5c1  group: letter
+\<i>                    code: 0x01d5c2  group: letter
+\<j>                    code: 0x01d5c3  group: letter
+\<k>                    code: 0x01d5c4  group: letter
+\<l>                    code: 0x01d5c5  group: letter
+\<m>                    code: 0x01d5c6  group: letter
+\<n>                    code: 0x01d5c7  group: letter
+\<o>                    code: 0x01d5c8  group: letter
+\<p>                    code: 0x01d5c9  group: letter
+\<q>                    code: 0x01d5ca  group: letter
+\<r>                    code: 0x01d5cb  group: letter
+\<s>                    code: 0x01d5cc  group: letter
+\<t>                    code: 0x01d5cd  group: letter
+\<u>                    code: 0x01d5ce  group: letter
+\<v>                    code: 0x01d5cf  group: letter
+\<w>                    code: 0x01d5d0  group: letter
+\<x>                    code: 0x01d5d1  group: letter
+\<y>                    code: 0x01d5d2  group: letter
+\<z>                    code: 0x01d5d3  group: letter
+\<AA>                   code: 0x01d504  group: letter
+\<BB>                   code: 0x01d505  group: letter
+\<CC>                   code: 0x00212d  group: letter
+\<DD>                   code: 0x01d507  group: letter
+\<EE>                   code: 0x01d508  group: letter
+\<FF>                   code: 0x01d509  group: letter
+\<GG>                   code: 0x01d50a  group: letter
+\<HH>                   code: 0x00210c  group: letter
+\<II>                   code: 0x002111  group: letter
+\<JJ>                   code: 0x01d50d  group: letter
+\<KK>                   code: 0x01d50e  group: letter
+\<LL>                   code: 0x01d50f  group: letter
+\<MM>                   code: 0x01d510  group: letter
+\<NN>                   code: 0x01d511  group: letter
+\<OO>                   code: 0x01d512  group: letter
+\<PP>                   code: 0x01d513  group: letter
+\<QQ>                   code: 0x01d514  group: letter
+\<RR>                   code: 0x00211c  group: letter
+\<SS>                   code: 0x01d516  group: letter
+\<TT>                   code: 0x01d517  group: letter
+\<UU>                   code: 0x01d518  group: letter
+\<VV>                   code: 0x01d519  group: letter
+\<WW>                   code: 0x01d51a  group: letter
+\<XX>                   code: 0x01d51b  group: letter
+\<YY>                   code: 0x01d51c  group: letter
+\<ZZ>                   code: 0x002128  group: letter
+\<aa>                   code: 0x01d51e  group: letter
+\<bb>                   code: 0x01d51f  group: letter
+\<cc>                   code: 0x01d520  group: letter
+\<dd>                   code: 0x01d521  group: letter
+\<ee>                   code: 0x01d522  group: letter
+\<ff>                   code: 0x01d523  group: letter
+\<gg>                   code: 0x01d524  group: letter
+\<hh>                   code: 0x01d525  group: letter
+\<ii>                   code: 0x01d526  group: letter
+\<jj>                   code: 0x01d527  group: letter
+\<kk>                   code: 0x01d528  group: letter
+\<ll>                   code: 0x01d529  group: letter
+\<mm>                   code: 0x01d52a  group: letter
+\<nn>                   code: 0x01d52b  group: letter
+\<oo>                   code: 0x01d52c  group: letter
+\<pp>                   code: 0x01d52d  group: letter
+\<qq>                   code: 0x01d52e  group: letter
+\<rr>                   code: 0x01d52f  group: letter
+\<ss>                   code: 0x01d530  group: letter
+\<tt>                   code: 0x01d531  group: letter
+\<uu>                   code: 0x01d532  group: letter
+\<vv>                   code: 0x01d533  group: letter
+\<ww>                   code: 0x01d534  group: letter
+\<xx>                   code: 0x01d535  group: letter
+\<yy>                   code: 0x01d536  group: letter
+\<zz>                   code: 0x01d537  group: letter
+\<alpha>                code: 0x0003b1  group: greek
+\<beta>                 code: 0x0003b2  group: greek
+\<gamma>                code: 0x0003b3  group: greek
+\<delta>                code: 0x0003b4  group: greek
+\<epsilon>              code: 0x0003b5  group: greek
+\<zeta>                 code: 0x0003b6  group: greek
+\<eta>                  code: 0x0003b7  group: greek
+\<theta>                code: 0x0003b8  group: greek
+\<iota>                 code: 0x0003b9  group: greek
+\<kappa>                code: 0x0003ba  group: greek
+\<lambda>               code: 0x0003bb  group: greek  abbrev: %
+\<mu>                   code: 0x0003bc  group: greek
+\<nu>                   code: 0x0003bd  group: greek
+\<xi>                   code: 0x0003be  group: greek
+\<pi>                   code: 0x0003c0  group: greek
+\<rho>                  code: 0x0003c1  group: greek
+\<sigma>                code: 0x0003c3  group: greek
+\<tau>                  code: 0x0003c4  group: greek
+\<upsilon>              code: 0x0003c5  group: greek
+\<phi>                  code: 0x0003c6  group: greek
+\<chi>                  code: 0x0003c7  group: greek
+\<psi>                  code: 0x0003c8  group: greek
+\<omega>                code: 0x0003c9  group: greek
+\<Gamma>                code: 0x000393  group: greek
+\<Delta>                code: 0x000394  group: greek
+\<Theta>                code: 0x000398  group: greek
+\<Lambda>               code: 0x00039b  group: greek
+\<Xi>                   code: 0x00039e  group: greek
+\<Pi>                   code: 0x0003a0  group: greek
+\<Sigma>                code: 0x0003a3  group: greek
+\<Upsilon>              code: 0x0003a5  group: greek
+\<Phi>                  code: 0x0003a6  group: greek
+\<Psi>                  code: 0x0003a8  group: greek
+\<Omega>                code: 0x0003a9  group: greek
+\<bool>                 code: 0x01d539  group: letter
+\<complex>              code: 0x002102  group: letter
+\<nat>                  code: 0x002115  group: letter
+\<rat>                  code: 0x00211a  group: letter
+\<real>                 code: 0x00211d  group: letter
+\<int>                  code: 0x002124  group: letter
+\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
+\<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
+\<longlongleftarrow>    code: 0x00290e  group: arrow  abbrev: <.
+\<longlonglongleftarrow> code: 0x0021e0 group: arrow  abbrev: <.
+\<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
+\<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->
+\<longlongrightarrow>   code: 0x00290f  group: arrow  abbrev: .>  abbrev: --->
+\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: --->
+\<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
+\<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
+\<Lleftarrow>           code: 0x0021da  group: arrow  abbrev: <.
+\<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: .>  abbrev: =>
+\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: .>  abbrev: ==>
+\<Rrightarrow>          code: 0x0021db  group: arrow  abbrev: .>
+\<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <>  abbrev: <->
+\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <>  abbrev: <->  abbrev: <-->
+\<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <>
+\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <>
+\<mapsto>               code: 0x0021a6  group: arrow  abbrev: .>  abbrev: |->
+\<longmapsto>           code: 0x0027fc  group: arrow  abbrev: .>  abbrev: |-->
+\<midarrow>             code: 0x002500  group: arrow  abbrev: <>
+\<Midarrow>             code: 0x002550  group: arrow  abbrev: <>
+\<hookleftarrow>        code: 0x0021a9  group: arrow  abbrev: <.
+\<hookrightarrow>       code: 0x0021aa  group: arrow  abbrev: .>
+\<leftharpoondown>      code: 0x0021bd  group: arrow  abbrev: <.
+\<rightharpoondown>     code: 0x0021c1  group: arrow  abbrev: .>
+\<leftharpoonup>        code: 0x0021bc  group: arrow  abbrev: <.
+\<rightharpoonup>       code: 0x0021c0  group: arrow  abbrev: .>
+\<rightleftharpoons>    code: 0x0021cc  group: arrow  abbrev: <> abbrev: ==
+\<leadsto>              code: 0x00219d  group: arrow  abbrev: .> abbrev: ~>
+\<downharpoonleft>      code: 0x0021c3  group: arrow
+\<downharpoonright>     code: 0x0021c2  group: arrow
+\<upharpoonleft>        code: 0x0021bf  group: arrow
+#\<upharpoonright>       code: 0x0021be  group: arrow
+\<restriction>          code: 0x0021be  group: operator
+\<Colon>                code: 0x002237  group: punctuation
+\<up>                   code: 0x002191  group: arrow
+\<Up>                   code: 0x0021d1  group: arrow
+\<down>                 code: 0x002193  group: arrow
+\<Down>                 code: 0x0021d3  group: arrow
+\<updown>               code: 0x002195  group: arrow
+\<Updown>               code: 0x0021d5  group: arrow
+\<langle>               code: 0x0027e8  group: punctuation  abbrev: <<
+\<rangle>               code: 0x0027e9  group: punctuation  abbrev: >>
+\<llangle>              code: 0x0027ea  group: punctuation  abbrev: <<
+\<rrangle>              code: 0x0027eb  group: punctuation  abbrev: >>
+\<lceil>                code: 0x002308  group: punctuation  abbrev: [.
+\<rceil>                code: 0x002309  group: punctuation  abbrev: .]
+\<lfloor>               code: 0x00230a  group: punctuation  abbrev: [.
+\<rfloor>               code: 0x00230b  group: punctuation  abbrev: .]
+\<lparr>                code: 0x002987  group: punctuation  abbrev: (|
+\<rparr>                code: 0x002988  group: punctuation  abbrev: |)
+\<lbrakk>               code: 0x0027e6  group: punctuation  abbrev: [|
+\<rbrakk>               code: 0x0027e7  group: punctuation  abbrev: |]
+\<lbrace>               code: 0x002983  group: punctuation  abbrev: {|
+\<rbrace>               code: 0x002984  group: punctuation  abbrev: |}
+\<guillemotleft>        code: 0x0000ab  group: punctuation  abbrev: <<
+\<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
+\<bottom>               code: 0x0022a5  group: logic
+\<top>                  code: 0x0022a4  group: logic
+\<and>                  code: 0x002227  group: logic  abbrev: /\  abbrev: &
+\<And>                  code: 0x0022c0  group: logic  abbrev: !!
+\<or>                   code: 0x002228  group: logic  abbrev: \/  abbrev: |
+\<Or>                   code: 0x0022c1  group: logic  abbrev: ??
+\<forall>               code: 0x002200  group: logic  abbrev: !  abbrev: ALL
+\<exists>               code: 0x002203  group: logic  abbrev: ?  abbrev: EX
+\<nexists>              code: 0x002204  group: logic  abbrev: ~?
+\<not>                  code: 0x0000ac  group: logic  abbrev: ~
+\<circle>               code: 0x0025cb  group: logic
+\<box>                  code: 0x0025a1  group: logic
+\<diamond>              code: 0x0025c7  group: logic
+\<diamondop>            code: 0x0022c4  group: operator
+\<turnstile>            code: 0x0022a2  group: relation  abbrev: |-
+\<Turnstile>            code: 0x0022a8  group: relation  abbrev: |=
+\<tturnstile>           code: 0x0022a9  group: relation  abbrev: |-
+\<TTurnstile>           code: 0x0022ab  group: relation  abbrev: |=
+\<stileturn>            code: 0x0022a3  group: relation  abbrev: -|
+\<surd>                 code: 0x00221a  group: relation
+\<le>                   code: 0x002264  group: relation  abbrev: <=
+\<ge>                   code: 0x002265  group: relation  abbrev: >=
+\<lless>                code: 0x00226a  group: relation  abbrev: <<
+\<ggreater>             code: 0x00226b  group: relation  abbrev: >>
+\<lesssim>              code: 0x002272  group: relation
+\<greatersim>           code: 0x002273  group: relation
+\<lessapprox>           code: 0x002a85  group: relation
+\<greaterapprox>        code: 0x002a86  group: relation
+\<in>                   code: 0x002208  group: relation  abbrev: :
+\<notin>                code: 0x002209  group: relation  abbrev: ~:
+\<subset>               code: 0x002282  group: relation
+\<supset>               code: 0x002283  group: relation
+\<subseteq>             code: 0x002286  group: relation  abbrev: (=
+\<supseteq>             code: 0x002287  group: relation  abbrev: )=
+\<sqsubset>             code: 0x00228f  group: relation
+\<sqsupset>             code: 0x002290  group: relation
+\<sqsubseteq>           code: 0x002291  group: relation  abbrev: [=
+\<sqsupseteq>           code: 0x002292  group: relation  abbrev: ]=
+\<inter>                code: 0x002229  group: operator  abbrev: Int
+\<Inter>                code: 0x0022c2  group: operator  abbrev: Inter  abbrev: INT
+\<union>                code: 0x00222a  group: operator  abbrev: Un
+\<Union>                code: 0x0022c3  group: operator  abbrev: Union  abbrev: UN
+\<squnion>              code: 0x002294  group: operator
+\<Squnion>              code: 0x002a06  group: operator  abbrev: SUP
+\<sqinter>              code: 0x002293  group: operator
+\<Sqinter>              code: 0x002a05  group: operator  abbrev: INF
+\<setminus>             code: 0x002216  group: operator
+\<propto>               code: 0x00221d  group: operator
+\<uplus>                code: 0x00228e  group: operator
+\<Uplus>                code: 0x002a04  group: operator
+\<noteq>                code: 0x002260  group: relation  abbrev: ~=
+\<sim>                  code: 0x00223c  group: relation
+\<doteq>                code: 0x002250  group: relation  abbrev: .=
+\<simeq>                code: 0x002243  group: relation
+\<approx>               code: 0x002248  group: relation
+\<asymp>                code: 0x00224d  group: relation
+\<cong>                 code: 0x002245  group: relation
+\<smile>                code: 0x002323  group: relation
+\<equiv>                code: 0x002261  group: relation  abbrev: ==
+\<frown>                code: 0x002322  group: relation
+\<Join>                 code: 0x0022c8
+\<bowtie>               code: 0x002a1d
+\<prec>                 code: 0x00227a  group: relation
+\<succ>                 code: 0x00227b  group: relation
+\<preceq>               code: 0x00227c  group: relation
+\<succeq>               code: 0x00227d  group: relation
+\<parallel>             code: 0x002225  group: punctuation  abbrev: ||
+\<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
+\<bbar>                 code: 0x002aff  group: punctuation  abbrev: ||
+\<plusminus>            code: 0x0000b1  group: operator
+\<minusplus>            code: 0x002213  group: operator
+\<times>                code: 0x0000d7  group: operator  abbrev: <*>
+\<div>                  code: 0x0000f7  group: operator
+\<cdot>                 code: 0x0022c5  group: operator
+\<star>                 code: 0x0022c6  group: operator
+\<bullet>               code: 0x002219  group: operator
+\<circ>                 code: 0x002218  group: operator
+\<dagger>               code: 0x002020
+\<ddagger>              code: 0x002021
+\<lhd>                  code: 0x0022b2  group: relation
+\<rhd>                  code: 0x0022b3  group: relation
+\<unlhd>                code: 0x0022b4  group: relation
+\<unrhd>                code: 0x0022b5  group: relation
+\<triangleleft>         code: 0x0025c3  group: relation
+\<triangleright>        code: 0x0025b9  group: relation
+\<triangle>             code: 0x0025b3  group: relation
+\<triangleq>            code: 0x00225c  group: relation
+\<oplus>                code: 0x002295  group: operator
+\<Oplus>                code: 0x002a01  group: operator
+\<otimes>               code: 0x002297  group: operator
+\<Otimes>               code: 0x002a02  group: operator
+\<odot>                 code: 0x002299  group: operator
+\<Odot>                 code: 0x002a00  group: operator
+\<ominus>               code: 0x002296  group: operator
+\<oslash>               code: 0x002298  group: operator
+\<dots>                 code: 0x002026  group: punctuation abbrev: ...
+\<cdots>                code: 0x0022ef  group: punctuation
+\<Sum>                  code: 0x002211  group: operator  abbrev: SUM
+\<Prod>                 code: 0x00220f  group: operator  abbrev: PROD
+\<Coprod>               code: 0x002210  group: operator
+\<infinity>             code: 0x00221e
+\<integral>             code: 0x00222b  group: operator
+\<ointegral>            code: 0x00222e  group: operator
+\<clubsuit>             code: 0x002663
+\<diamondsuit>          code: 0x002662
+\<heartsuit>            code: 0x002661
+\<spadesuit>            code: 0x002660
+\<aleph>                code: 0x002135
+\<emptyset>             code: 0x002205
+\<nabla>                code: 0x002207
+\<partial>              code: 0x002202
+\<flat>                 code: 0x00266d
+\<natural>              code: 0x00266e
+\<sharp>                code: 0x00266f
+\<angle>                code: 0x002220
+\<copyright>            code: 0x0000a9
+\<registered>           code: 0x0000ae
+\<hyphen>               code: 0x002010  group: punctuation
+\<inverse>              code: 0x0000af  group: operator
+\<sqdot>                code: 0x0000b7  group: punctuation
+\<onequarter>           code: 0x0000bc  group: digit
+\<onehalf>              code: 0x0000bd  group: digit
+\<threequarters>        code: 0x0000be  group: digit
+\<ordfeminine>          code: 0x0000aa
+\<ordmasculine>         code: 0x0000ba
+\<section>              code: 0x0000a7
+\<paragraph>            code: 0x0000b6
+\<exclamdown>           code: 0x0000a1
+\<questiondown>         code: 0x0000bf
+\<euro>                 code: 0x0020ac
+\<pounds>               code: 0x0000a3
+\<yen>                  code: 0x0000a5
+\<cent>                 code: 0x0000a2
+\<currency>             code: 0x0000a4
+\<degree>               code: 0x0000b0
+\<amalg>                code: 0x002a3f  group: operator
+\<mho>                  code: 0x002127  group: operator
+\<lozenge>              code: 0x0025ca
+\<wp>                   code: 0x002118
+\<wrong>                code: 0x002240  group: relation
+\<acute>                code: 0x0000b4
+\<index>                code: 0x000131
+\<dieresis>             code: 0x0000a8
+\<cedilla>              code: 0x0000b8
+\<hungarumlaut>         code: 0x0002dd
+\<bind>                 code: 0x00291c  group: operator  abbrev: >>=
+\<then>                 code: 0x002aa2  group: operator  abbrev: >>
+\<some>                 code: 0x0003f5
+\<hole>                 code: 0x002311
+\<newline>              code: 0x0023ce
+\<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^latex>                               group: document  argument: cartouche
+\<^marker>              code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<
+\<close>                code: 0x00203a  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: >>
+\<^here>                code: 0x002302  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^undefined>           code: 0x002756  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^noindent>            code: 0x0021e4  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^smallskip>           code: 0x002508  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^medskip>             code: 0x002509  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^bigskip>             code: 0x002501  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^item>                code: 0x0025aa  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^enum>                code: 0x0025b8  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^descr>               code: 0x0027a7  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^footnote>            code: 0x00204b  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^verbatim>            code: 0x0025a9  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^theory_text>         code: 0x002b1a  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^emph>                code: 0x002217  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^bold>                code: 0x002759  group: control  argument: cartouche  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^sub>                 code: 0x0021e9  group: control  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^sup>                 code: 0x0021e7  group: control  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^bsub>                code: 0x0021d8  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =_(
+\<^esub>                code: 0x0021d9  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =_)
+\<^bsup>                code: 0x0021d7  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =^(
+\<^esup>                code: 0x0021d6  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =^)
+\<^file>                code: 0x01F5CF  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^dir>                 code: 0x01F5C0  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^url>                 code: 0x01F310  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^doc>                 code: 0x01F4D3  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^action>              code: 0x00261b  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<^assert>
+\<^binding>             argument: cartouche
+\<^class>               argument: cartouche
+\<^class_syntax>        argument: cartouche
+\<^command_keyword>     argument: cartouche
+\<^const>               argument: cartouche
+\<^const_abbrev>        argument: cartouche
+\<^const_name>          argument: cartouche
+\<^const_syntax>        argument: cartouche
+\<^context>
+\<^cprop>               argument: cartouche
+\<^cterm>               argument: cartouche
+\<^ctyp>                argument: cartouche
+\<^keyword>             argument: cartouche
+\<^locale>              argument: cartouche
+\<^make_string>
+\<^method>              argument: cartouche
+\<^named_theorems>      argument: cartouche
+\<^nonterminal>         argument: cartouche
+\<^path>                argument: cartouche
+\<^path_binding>        argument: cartouche
+\<^plugin>              argument: cartouche
+\<^print>
+\<^prop>                argument: cartouche
+\<^bash_function>       argument: cartouche
+\<^scala>               argument: cartouche
+\<^scala_function>      argument: cartouche
+\<^scala_method>        argument: cartouche
+\<^scala_object>        argument: cartouche
+\<^scala_thread>        argument: cartouche
+\<^scala_type>          argument: cartouche
+\<^session>             argument: cartouche
+\<^simproc>             argument: cartouche
+\<^sort>                argument: cartouche
+\<^syntax_const>        argument: cartouche
+\<^system_option>       argument: cartouche
+\<^term>                argument: cartouche
+\<^theory>              argument: cartouche
+\<^theory_context>      argument: cartouche
+\<^tool>                argument: cartouche
+\<^typ>                 argument: cartouche
+\<^type_abbrev>         argument: cartouche
+\<^type_name>           argument: cartouche
+\<^type_syntax>         argument: cartouche
+\<^oracle_name>         argument: cartouche
+\<^code>                argument: cartouche
+\<^computation>         argument: cartouche
+\<^computation_conv>    argument: cartouche
+\<^computation_check>   argument: cartouche