diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml
index 86c6e1e..e8c5f4d 100644
--- a/.github/workflows/verify.yml
+++ b/.github/workflows/verify.yml
@@ -46,7 +46,9 @@ jobs:
         run: cargo clippy --all-targets --all-features -- -D warnings
       - name: Format
         run: cargo fmt -- --check
+      - name: Docs
+        run: cargo doc --lib --no-deps
       - name: Verify official set.mm
         run: |
-          curl -s -G https://raw.githubusercontent.com/metamath/set.mm/master/set.mm > set.mm
-          cargo run -- --jobs 8 set.mm --verify --grammar --parse-stmt --verify-parse-stmt
+          curl -s -G https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm > set.mm
+          cargo run -- --jobs 8 set.mm --verify --grammar --parse-stmt --verify-parse-stmt --verify-markup --parse-typesetting
diff --git a/Cargo.lock b/Cargo.lock
index 1e8685f..edc216c 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,50 +2,98 @@
 # It is not intended for manual editing.
 version = 3
 
+[[package]]
+name = "ahash"
+version = "0.8.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011"
+dependencies = [
+ "cfg-if",
+ "getrandom",
+ "once_cell",
+ "version_check",
+ "zerocopy",
+]
+
 [[package]]
 name = "aho-corasick"
-version = "0.7.18"
+version = "1.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1e37cfd5e7657ada45f742d6e99ca5788580b5c529dc78faf11ece6dc702656f"
+checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916"
 dependencies = [
  "memchr",
 ]
 
 [[package]]
 name = "annotate-snippets"
-version = "0.9.1"
+version = "0.11.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c3b9d411ecbaf79885c6df4d75fff75858d5995ff25385657a28af47e82f9c36"
+checksum = "24e35ed54e5ea7997c14ed4c70ba043478db1112e98263b3b035907aa197d991"
 dependencies = [
+ "anstyle",
  "unicode-width",
- "yansi-term",
 ]
 
 [[package]]
-name = "ansi_term"
-version = "0.11.0"
+name = "anstream"
+version = "0.6.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee49baf6cb617b853aa8d93bf420db2383fab46d314482ca2803b40d5fde979b"
+checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526"
 dependencies = [
- "winapi",
+ "anstyle",
+ "anstyle-parse",
+ "anstyle-query",
+ "anstyle-wincon",
+ "colorchoice",
+ "is_terminal_polyfill",
+ "utf8parse",
 ]
 
 [[package]]
-name = "atty"
-version = "0.2.14"
+name = "anstyle"
+version = "1.0.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8"
+checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1"
+
+[[package]]
+name = "anstyle-parse"
+version = "0.2.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb"
 dependencies = [
- "hermit-abi",
- "libc",
- "winapi",
+ "utf8parse",
 ]
 
+[[package]]
+name = "anstyle-query"
+version = "1.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a"
+dependencies = [
+ "windows-sys 0.52.0",
+]
+
+[[package]]
+name = "anstyle-wincon"
+version = "3.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8"
+dependencies = [
+ "anstyle",
+ "windows-sys 0.52.0",
+]
+
+[[package]]
+name = "assert_matches"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9b34d609dfbaf33d6889b2b7106d3ca345eacad44200913df5ba02bfd31d2ba9"
+
 [[package]]
 name = "autocfg"
-version = "1.0.1"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a"
+checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0"
 
 [[package]]
 name = "bitflags"
@@ -53,6 +101,18 @@ version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
+[[package]]
+name = "bitflags"
+version = "2.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
+
+[[package]]
+name = "byteorder"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
+
 [[package]]
 name = "cfg-if"
 version = "1.0.0"
@@ -60,66 +120,147 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
-name = "chrono"
-version = "0.4.19"
+name = "clap"
+version = "4.5.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "670ad68c9088c2a963aaa298cb369688cf3f9465ce5e2d4ca10e6e0098a1ce73"
+checksum = "35723e6a11662c2afb578bcf0b88bf6ea8e21282a953428f240574fcc3a2b5b3"
 dependencies = [
- "libc",
- "num-integer",
- "num-traits",
- "time",
- "winapi",
+ "clap_builder",
+ "clap_derive",
 ]
 
 [[package]]
-name = "clap"
-version = "2.33.3"
+name = "clap_builder"
+version = "4.5.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "37e58ac78573c40708d45522f0d80fa2f01cc4f9b4e2bf749807255454312002"
+checksum = "49eb96cbfa7cfa35017b7cd548c75b14c3118c98b423041d70562665e07fb0fa"
 dependencies = [
- "ansi_term",
- "atty",
- "bitflags",
+ "anstream",
+ "anstyle",
+ "clap_lex",
  "strsim",
- "textwrap",
- "unicode-width",
- "vec_map",
 ]
 
+[[package]]
+name = "clap_derive"
+version = "4.5.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5d029b67f89d30bbb547c89fd5161293c0aec155fc691d7924b64550662db93e"
+dependencies = [
+ "heck",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "clap_lex"
+version = "0.7.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97"
+
+[[package]]
+name = "colorchoice"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0"
+
 [[package]]
 name = "colored"
-version = "1.9.3"
+version = "2.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f4ffc801dacf156c5854b9df4f425a626539c3a6ef7893cc0c5084a23f0b6c59"
+checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8"
 dependencies = [
- "atty",
  "lazy_static",
- "winapi",
+ "windows-sys 0.48.0",
+]
+
+[[package]]
+name = "cssparser"
+version = "0.31.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5b3df4f93e5fbbe73ec01ec8d3f68bba73107993a5b1e7519273c32db9b0d5be"
+dependencies = [
+ "cssparser-macros",
+ "dtoa-short",
+ "itoa",
+ "phf 0.11.2",
+ "smallvec",
+]
+
+[[package]]
+name = "cssparser-macros"
+version = "0.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "13b588ba4ac1a99f7f2964d24b3d896ddc6bf847ee3855dbd4366f058cfcd331"
+dependencies = [
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "deranged"
+version = "0.3.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4"
+dependencies = [
+ "powerfmt",
+]
+
+[[package]]
+name = "derive_more"
+version = "0.99.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5f33878137e4dafd7fa914ad4e259e18a4e8e532b9617a2d0150262bf53abfce"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
 ]
 
 [[package]]
 name = "dot-writer"
-version = "0.1.2"
+version = "0.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1defb949b123415131ecae40ab5dca70e9f39eedda3de2cebb03a8a98fdf5894"
+checksum = "3d1b11bd5e7e98406c6ff39fbc94d6e910a489b978ce7f17c19fce91a1195b7a"
+
+[[package]]
+name = "dtoa"
+version = "1.0.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dcbb2bf8e87535c23f7a8a321e364ce21462d0ff10cb6407820e8e96dfff6653"
+
+[[package]]
+name = "dtoa-short"
+version = "0.3.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cd1511a7b6a56299bd043a9c167a6d2bfb37bf84a6dfceaba651168adfb43c87"
+dependencies = [
+ "dtoa",
+]
+
+[[package]]
+name = "ego-tree"
+version = "0.6.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3a68a4904193147e0a8dec3314640e6db742afd5f6e634f428a6af230d9b3591"
 
 [[package]]
 name = "either"
-version = "1.6.1"
+version = "1.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e78d4f1cc4ae33bbfc157ed5d5a5ef3bc29227303d595861deb238fcec4e9457"
+checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0"
 
 [[package]]
 name = "filetime"
-version = "0.2.15"
+version = "0.2.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "975ccf83d8d9d0d84682850a38c8169027be83368805971cc4f238c2b245bc98"
+checksum = "1ee447700ac8aa0b2f2bd7bc4462ad686ba06baa6727ac149a2d6277f0d240fd"
 dependencies = [
  "cfg-if",
  "libc",
- "redox_syscall",
- "winapi",
+ "redox_syscall 0.4.1",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -129,101 +270,413 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
 
 [[package]]
-name = "hermit-abi"
-version = "0.1.19"
+name = "futf"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "df420e2e84819663797d1ec6544b13c5be84629e7bb00dc960d6917db2987843"
+dependencies = [
+ "mac",
+ "new_debug_unreachable",
+]
+
+[[package]]
+name = "fxhash"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c31b6d751ae2c7f11320402d34e41349dd1016f8d5d45e48c4312bc8625af50c"
+dependencies = [
+ "byteorder",
+]
+
+[[package]]
+name = "getopts"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5"
+dependencies = [
+ "unicode-width",
+]
+
+[[package]]
+name = "getrandom"
+version = "0.2.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
+checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7"
 dependencies = [
+ "cfg-if",
  "libc",
+ "wasi",
 ]
 
+[[package]]
+name = "heck"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
+
+[[package]]
+name = "html5ever"
+version = "0.27.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c13771afe0e6e846f1e67d038d4cb29998a6779f93c809212e4e9c32efd244d4"
+dependencies = [
+ "log",
+ "mac",
+ "markup5ever",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "is_terminal_polyfill"
+version = "1.70.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf"
+
 [[package]]
 name = "itertools"
-version = "0.10.3"
+version = "0.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a9a9d19fa1e79b6215ff29b9d6880b706147f16e9b1dbb1e4e5947b5b02bc5e3"
+checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186"
 dependencies = [
  "either",
 ]
 
+[[package]]
+name = "itoa"
+version = "1.0.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
+
 [[package]]
 name = "lazy_static"
-version = "1.4.0"
+version = "1.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
+checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
 
 [[package]]
 name = "libc"
-version = "0.2.103"
+version = "0.2.155"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c"
+
+[[package]]
+name = "lock_api"
+version = "0.4.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dd8f7255a17a627354f321ef0055d63b898c6fb27eff628af4d1b66b7331edf6"
+checksum = "07af8b9cdd281b7915f413fa73f29ebd5d55d0d3f0155584dade1ff18cea1b17"
+dependencies = [
+ "autocfg",
+ "scopeguard",
+]
 
 [[package]]
 name = "log"
-version = "0.4.14"
+version = "0.4.22"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24"
+
+[[package]]
+name = "mac"
+version = "0.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "51b9bbe6c47d51fc3e1a9b945965946b4c44142ab8792c50835a980d362c2710"
+checksum = "c41e0c4fef86961ac6d6f8a82609f55f31b05e4fce149ac5710e439df7619ba4"
+
+[[package]]
+name = "markup5ever"
+version = "0.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "16ce3abbeba692c8b8441d036ef91aea6df8da2c6b6e21c7e14d3c18e526be45"
 dependencies = [
- "cfg-if",
+ "log",
+ "phf 0.11.2",
+ "phf_codegen 0.11.2",
+ "string_cache",
+ "string_cache_codegen",
+ "tendril",
 ]
 
 [[package]]
 name = "memchr"
-version = "2.4.1"
+version = "2.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a"
+checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
 
 [[package]]
 name = "metamath-knife"
-version = "0.3.6"
+version = "0.3.9"
 dependencies = [
  "annotate-snippets",
  "clap",
+ "metamath-rs",
+ "simple_logger",
+]
+
+[[package]]
+name = "metamath-rs"
+version = "0.3.9"
+dependencies = [
+ "annotate-snippets",
+ "assert_matches",
  "dot-writer",
  "filetime",
  "fnv",
+ "html5ever",
  "itertools",
- "lazy_static",
  "log",
  "regex",
- "simple_logger",
+ "scraper",
  "tinyvec",
  "typed-arena",
+ "xml-rs",
 ]
 
 [[package]]
-name = "num-integer"
-version = "0.1.44"
+name = "new_debug_unreachable"
+version = "1.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "650eef8c711430f1a879fdd01d4745a7deea475becfb90269c06775983bbf086"
+
+[[package]]
+name = "num-conv"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9"
+
+[[package]]
+name = "num_threads"
+version = "0.1.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d2cc698a63b549a70bc047073d2949cce27cd1c7b0a4a862d08a8031bc2801db"
+checksum = "5c7398b9c8b70908f6371f47ed36737907c87c52af34c268fed0bf0ceb92ead9"
 dependencies = [
- "autocfg",
- "num-traits",
+ "libc",
 ]
 
 [[package]]
-name = "num-traits"
-version = "0.2.14"
+name = "once_cell"
+version = "1.19.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a64b1ec5cda2586e284722486d802acf1f7dbdc623e2bfc57e65ca1cd099290"
+checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92"
+
+[[package]]
+name = "parking_lot"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f1bf18183cf54e8d6059647fc3063646a1801cf30896933ec2311622cc4b9a27"
 dependencies = [
- "autocfg",
+ "lock_api",
+ "parking_lot_core",
+]
+
+[[package]]
+name = "parking_lot_core"
+version = "0.9.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1e401f977ab385c9e4e3ab30627d6f26d00e2c73eef317493c4ec6d468726cf8"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "redox_syscall 0.5.3",
+ "smallvec",
+ "windows-targets 0.52.6",
+]
+
+[[package]]
+name = "phf"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fabbf1ead8a5bcbc20f5f8b939ee3f5b0f6f281b6ad3468b84656b658b455259"
+dependencies = [
+ "phf_shared 0.10.0",
+]
+
+[[package]]
+name = "phf"
+version = "0.11.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ade2d8b8f33c7333b51bcf0428d37e217e9f32192ae4772156f65063b8ce03dc"
+dependencies = [
+ "phf_macros",
+ "phf_shared 0.11.2",
+]
+
+[[package]]
+name = "phf_codegen"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4fb1c3a8bc4dd4e5cfce29b44ffc14bedd2ee294559a294e2a4d4c9e9a6a13cd"
+dependencies = [
+ "phf_generator 0.10.0",
+ "phf_shared 0.10.0",
+]
+
+[[package]]
+name = "phf_codegen"
+version = "0.11.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e8d39688d359e6b34654d328e262234662d16cc0f60ec8dcbe5e718709342a5a"
+dependencies = [
+ "phf_generator 0.11.2",
+ "phf_shared 0.11.2",
+]
+
+[[package]]
+name = "phf_generator"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5d5285893bb5eb82e6aaf5d59ee909a06a16737a8970984dd7746ba9283498d6"
+dependencies = [
+ "phf_shared 0.10.0",
+ "rand",
+]
+
+[[package]]
+name = "phf_generator"
+version = "0.11.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "48e4cc64c2ad9ebe670cb8fd69dd50ae301650392e81c05f9bfcb2d5bdbc24b0"
+dependencies = [
+ "phf_shared 0.11.2",
+ "rand",
+]
+
+[[package]]
+name = "phf_macros"
+version = "0.11.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3444646e286606587e49f3bcf1679b8cef1dc2c5ecc29ddacaffc305180d464b"
+dependencies = [
+ "phf_generator 0.11.2",
+ "phf_shared 0.11.2",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "phf_shared"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b6796ad771acdc0123d2a88dc428b5e38ef24456743ddb1744ed628f9815c096"
+dependencies = [
+ "siphasher",
+]
+
+[[package]]
+name = "phf_shared"
+version = "0.11.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "90fcb95eef784c2ac79119d1dd819e162b5da872ce6f3c3abe1e8ca1c082f72b"
+dependencies = [
+ "siphasher",
+]
+
+[[package]]
+name = "powerfmt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"
+
+[[package]]
+name = "ppv-lite86"
+version = "0.2.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2288c0e17cc8d342c712bb43a257a80ebffce59cdb33d5000d8348f3ec02528b"
+dependencies = [
+ "zerocopy",
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "precomputed-hash"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "925383efa346730478fb4838dbe9137d2a47675ad789c546d150a6e1dd4ab31c"
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.86"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "rand"
+version = "0.8.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
+dependencies = [
+ "libc",
+ "rand_chacha",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
+dependencies = [
+ "ppv-lite86",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.6.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
+dependencies = [
+ "getrandom",
+]
+
+[[package]]
+name = "redox_syscall"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa"
+dependencies = [
+ "bitflags 1.3.2",
 ]
 
 [[package]]
 name = "redox_syscall"
-version = "0.2.10"
+version = "0.5.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8383f39639269cde97d255a32bdb68c047337295414940c68bdd30c2e13203ff"
+checksum = "2a908a6e00f1fdd0dfd9c0eb08ce85126f6d8bbda50017e74bc4a4b7d4a926a4"
 dependencies = [
- "bitflags",
+ "bitflags 2.6.0",
 ]
 
 [[package]]
 name = "regex"
-version = "1.5.4"
+version = "1.10.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d07a8629359eb56f1e2fb1652bb04212c072a87ba68546a04065d525673ac461"
+checksum = "b91213439dad192326a0d7c6ee3955910425f441d7038e0d6933b0aec5c4517f"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-automata",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-automata"
+version = "0.4.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "38caf58cc5ef2fed281f89292ef23f6365465ed9a41b7a7754eb4e26496c92df"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -232,106 +685,407 @@ dependencies = [
 
 [[package]]
 name = "regex-syntax"
-version = "0.6.25"
+version = "0.8.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7a66a03ae7c801facd77a29370b4faec201768915ac14a721ba36f20bc9c209b"
+
+[[package]]
+name = "scopeguard"
+version = "1.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b"
+checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
+
+[[package]]
+name = "scraper"
+version = "0.19.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "761fb705fdf625482d2ed91d3f0559dcfeab2798fe2771c69560a774865d0802"
+dependencies = [
+ "ahash",
+ "cssparser",
+ "ego-tree",
+ "getopts",
+ "html5ever",
+ "once_cell",
+ "selectors",
+ "tendril",
+]
+
+[[package]]
+name = "selectors"
+version = "0.25.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4eb30575f3638fc8f6815f448d50cb1a2e255b0897985c8c59f4d37b72a07b06"
+dependencies = [
+ "bitflags 2.6.0",
+ "cssparser",
+ "derive_more",
+ "fxhash",
+ "log",
+ "new_debug_unreachable",
+ "phf 0.10.1",
+ "phf_codegen 0.10.0",
+ "precomputed-hash",
+ "servo_arc",
+ "smallvec",
+]
+
+[[package]]
+name = "serde"
+version = "1.0.204"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bc76f558e0cbb2a839d37354c575f1dc3fdc6546b5be373ba43d95f231bf7c12"
+dependencies = [
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_derive"
+version = "1.0.204"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e0cd7e117be63d3c3678776753929474f3b04a43a080c744d6b0ae2a8c28e222"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "servo_arc"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d036d71a959e00c77a63538b90a6c2390969f9772b096ea837205c6bd0491a44"
+dependencies = [
+ "stable_deref_trait",
+]
 
 [[package]]
 name = "simple_logger"
-version = "1.13.0"
+version = "5.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7de33c687404ec3045d4a0d437580455257c0436f858d702f244e7d652f9f07"
+checksum = "e8c5dfa5e08767553704aa0ffd9d9794d527103c736aba9854773851fd7497eb"
 dependencies = [
- "atty",
- "chrono",
  "colored",
  "log",
- "winapi",
+ "time",
+ "windows-sys 0.48.0",
+]
+
+[[package]]
+name = "siphasher"
+version = "0.3.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "38b58827f4464d87d377d175e90bf58eb00fd8716ff0a62f80356b5e61555d0d"
+
+[[package]]
+name = "smallvec"
+version = "1.13.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
+
+[[package]]
+name = "stable_deref_trait"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a8f112729512f8e442d81f95a8a7ddf2b7c6b8a1a6f509a95864142b30cab2d3"
+
+[[package]]
+name = "string_cache"
+version = "0.8.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f91138e76242f575eb1d3b38b4f1362f10d3a43f47d182a5b359af488a02293b"
+dependencies = [
+ "new_debug_unreachable",
+ "once_cell",
+ "parking_lot",
+ "phf_shared 0.10.0",
+ "precomputed-hash",
+ "serde",
+]
+
+[[package]]
+name = "string_cache_codegen"
+version = "0.5.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6bb30289b722be4ff74a408c3cc27edeaad656e06cb1fe8fa9231fa59c728988"
+dependencies = [
+ "phf_generator 0.10.0",
+ "phf_shared 0.10.0",
+ "proc-macro2",
+ "quote",
 ]
 
 [[package]]
 name = "strsim"
-version = "0.8.0"
+version = "0.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a"
+checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
 
 [[package]]
-name = "textwrap"
-version = "0.11.0"
+name = "syn"
+version = "2.0.72"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060"
+checksum = "dc4b9b9bf2add8093d3f2c0204471e951b2285580335de42f9d2534f3ae7a8af"
 dependencies = [
- "unicode-width",
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "tendril"
+version = "0.4.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d24a120c5fc464a3458240ee02c299ebcb9d67b5249c8848b09d639dca8d7bb0"
+dependencies = [
+ "futf",
+ "mac",
+ "utf-8",
 ]
 
 [[package]]
 name = "time"
-version = "0.1.44"
+version = "0.3.36"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6db9e6914ab8b1ae1c260a4ae7a49b6c5611b40328a735b21862567685e73255"
+checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
 dependencies = [
+ "deranged",
+ "itoa",
  "libc",
- "wasi",
- "winapi",
+ "num-conv",
+ "num_threads",
+ "powerfmt",
+ "serde",
+ "time-core",
+ "time-macros",
+]
+
+[[package]]
+name = "time-core"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
+
+[[package]]
+name = "time-macros"
+version = "0.2.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f252a68540fde3a3877aeea552b832b40ab9a69e318efd078774a01ddee1ccf"
+dependencies = [
+ "num-conv",
+ "time-core",
 ]
 
 [[package]]
 name = "tinyvec"
-version = "1.5.0"
+version = "1.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f83b2a3d4d9091d0abd7eba4dc2710b1718583bd4d8992e2190720ea38f391f7"
+checksum = "445e881f4f6d382d5f27c034e25eb92edd7c784ceab92a0937db7f2e9471b938"
 
 [[package]]
 name = "typed-arena"
-version = "2.0.1"
+version = "2.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a"
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0685c84d5d54d1c26f7d3eb96cd41550adb97baed141a761cf335d3d33bcd0ae"
+checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
 
 [[package]]
 name = "unicode-width"
-version = "0.1.9"
+version = "0.1.13"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0336d538f7abc86d282a4189614dfaa90810dfc2c6f6427eaf88e16311dd225d"
+
+[[package]]
+name = "utf-8"
+version = "0.7.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973"
+checksum = "09cc8ee72d2a9becf2f2febe0205bbed8fc6615b7cb429ad062dc7b7ddd036a9"
 
 [[package]]
-name = "vec_map"
-version = "0.8.2"
+name = "utf8parse"
+version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191"
+checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
+
+[[package]]
+name = "version_check"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
 [[package]]
 name = "wasi"
-version = "0.10.0+wasi-snapshot-preview1"
+version = "0.11.0+wasi-snapshot-preview1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1a143597ca7c7793eff794def352d41792a93c481eb1042423ff7ff72ba2c31f"
+checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
 
 [[package]]
-name = "winapi"
-version = "0.3.9"
+name = "windows-sys"
+version = "0.48.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
+checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9"
 dependencies = [
- "winapi-i686-pc-windows-gnu",
- "winapi-x86_64-pc-windows-gnu",
+ "windows-targets 0.48.5",
 ]
 
 [[package]]
-name = "winapi-i686-pc-windows-gnu"
-version = "0.4.0"
+name = "windows-sys"
+version = "0.52.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
+checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
+dependencies = [
+ "windows-targets 0.52.6",
+]
 
 [[package]]
-name = "winapi-x86_64-pc-windows-gnu"
-version = "0.4.0"
+name = "windows-targets"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
+checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c"
+dependencies = [
+ "windows_aarch64_gnullvm 0.48.5",
+ "windows_aarch64_msvc 0.48.5",
+ "windows_i686_gnu 0.48.5",
+ "windows_i686_msvc 0.48.5",
+ "windows_x86_64_gnu 0.48.5",
+ "windows_x86_64_gnullvm 0.48.5",
+ "windows_x86_64_msvc 0.48.5",
+]
 
 [[package]]
-name = "yansi-term"
-version = "0.1.2"
+name = "windows-targets"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
+dependencies = [
+ "windows_aarch64_gnullvm 0.52.6",
+ "windows_aarch64_msvc 0.52.6",
+ "windows_i686_gnu 0.52.6",
+ "windows_i686_gnullvm",
+ "windows_i686_msvc 0.52.6",
+ "windows_x86_64_gnu 0.52.6",
+ "windows_x86_64_gnullvm 0.52.6",
+ "windows_x86_64_msvc 0.52.6",
+]
+
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
+
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"
+
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
+
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"
+
+[[package]]
+name = "windows_i686_gnu"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
+
+[[package]]
+name = "windows_i686_gnu"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"
+
+[[package]]
+name = "windows_i686_gnullvm"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"
+
+[[package]]
+name = "windows_i686_msvc"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
+
+[[package]]
+name = "windows_i686_msvc"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"
+
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
+
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"
+
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
+
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"
+
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
+
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
+
+[[package]]
+name = "xml-rs"
+version = "0.8.20"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "791978798f0597cfc70478424c2b4fdc2b7a8024aaff78497ef00f24ef674193"
+
+[[package]]
+name = "zerocopy"
+version = "0.7.35"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0"
+dependencies = [
+ "byteorder",
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.7.35"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fe5c30ade05e61656247b2e334a031dfd0cc466fadef865bdcdea8d537951bf1"
+checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
 dependencies = [
- "winapi",
+ "proc-macro2",
+ "quote",
+ "syn",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index 3265ca1..4e1682e 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,37 +1,20 @@
-[package]
+[workspace]
+members = [
+    "metamath-rs",
+    "metamath-knife",
+]
+resolver = "2"
+
+[workspace.package]
 authors = ["David A. Wheeler <dwheeler@dwheeler.com>", "Stefan O'Rear <sorear2@gmail.com>"]
 license = "MIT OR Apache-2.0"
-name = "metamath-knife"
 readme = "README.md"
-version = "0.3.6"
 description = "A parallel and incremental verifier for Metamath databases"
-repository = "https://github.com/david-a-wheeler/metamath-knife"
+repository = "https://github.com/metamath/metamath-knife"
 keywords = ["theorem", "proving", "verifier", "proof", "assistant"]
 categories = ["command-line-utilities", "development-tools", "mathematics"]
 edition = "2021"
 
-[dependencies]
-lazy_static = "1.4"
-itertools = "0.10"
-filetime = "0.2"
-fnv = "1.0"
-regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
-tinyvec = "1.5"
-log = "0.4"
-annotate-snippets = "0.9"
-typed-arena = "2.0"
-
-# Dependencies for standalone executable, not needed for a library
-clap = "2.33"
-simple_logger = "1.13"
-
-# Optional dependencies
-dot-writer = { version = "0.1.2", optional = true }
-
-[features]
-default = ["annotate-snippets/color"]
-dot = ["dot-writer"]
-
 [profile]
 
 [profile.release]
@@ -44,8 +27,3 @@ codegen-units = 4
 
 [profile.test]
 codegen-units = 4
-
-[[bin]]
-name = "metamath-knife"
-path = "src/main.rs"
-doc = false
diff --git a/README.md b/README.md
index e165861..d41d11c 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,7 @@ Metamath-knife is a friendly fork of
   adds support for *all* Metamath proof formats
   (<a href="https://groups.google.com/g/metamath/c/xCUNA2ttHew/m/RXSNzdovBAAJ">uncompressed, compressed, package, or explicit</a>.
 * We take extra steps to prevent errors, e.g., we have a CI pipeline
-  (implemented using GitHub actons).
+  (implemented using GitHub actions).
 * We remove deprecated constructs, e.g., the deprecated try!(...)
   has been replaced with the easier-to-read "?" construct.
 * We actively work to eliminate compiler warnings. This tends to
@@ -23,7 +23,7 @@ Metamath-knife is a friendly fork of
 
 ## Building
 
-Install Rust, "Rust 2018" (version 1.31.0) or later, then check out this repository and run:
+Install Rust, "Rust 2021" (version 1.56.0) or later, preferably using (rustup)[https://rustup.rs], then check out this repository and run:
 
     cargo build --release
 
@@ -38,12 +38,54 @@ Alternatively using `cargo install`:
     git clone https://github.com/metamath/set.mm
 
     # One-shot verification using 4 threads
-    target/release/metamath-knife --timing --jobs 4 --split --verify set.mm/set.mm
+    target/release/metamath-knife --time --jobs 4 --split --verify set.mm/set.mm
 
     # Incremental verification
-    (while sleep 5; do echo; done) | target/release/metamath-knife --timing --jobs 4 --split --repeat --trace-recalc --verify set.mm/set.mm
+    (while sleep 5; do echo; done) | target/release/metamath-knife --time --jobs 4 --split --repeat --trace-recalc --verify set.mm/set.mm
     # then make small changes to the beginning, end, or middle of the DB and observe how behavior changes
 
+Here is the command line help, which gives an idea of the options available:
+```
+A Metamath database verifier and processing tool
+
+USAGE:
+    metamath-knife [FLAGS] [OPTIONS] <DATABASE>
+
+FLAGS:
+        --debug                Activates debug logs, including for the grammar building and statement parsing
+    -F, --dump-formula         Dumps the formulas of this database
+    -G, --dump-grammar         Dumps the database's grammar
+    -T, --dump-typesetting     Dumps typesetting information
+        --free                 Explicitly deallocates working memory before exit
+    -g, --grammar              Checks grammar
+    -h, --help                 Prints help information
+    -O, --outline              Shows database outline
+    -p, --parse-stmt           Parses all statements according to the database's grammar
+    -t, --parse-typesetting    Parses typesetting information
+        --repeat               Demonstrates incremental verifier
+        --split                Processes files > 1 MiB in multiple segments
+        --time                 Prints milliseconds after each stage
+        --trace-recalc         Prints segments as they are recalculated
+    -V, --version              Prints version information
+    -v, --verify               Checks proof validity
+    -m, --verify-markup        Checks comment markup
+        --verify-parse-stmt    Checks that printing parsed statements gives back the original formulas
+    -u, --verify-usage         Checks axiom usage
+
+OPTIONS:
+        --text <NAME> <TEXT>          Provides raw database content on the command line
+    -X, --axiom-use <FILE>            Generate `axiom-use` file
+        --biblio <FILE>...            Supplies a bibliography file for verify-markup
+                                      Can be used one or two times; the second is for exthtml processing
+    -D, --discouraged <FILE>          Regenerates `discouraged` file
+    -e, --export <LABEL>...           Outputs a proof file
+    -j, --jobs <jobs>                 Number of threads to use for verification
+        --stmt-use <FILE> <LABELS>    Outputs statements directly or indirectly using the given list of statements
+
+ARGS:
+    <DATABASE>    Database file to load
+```
+
 ## License
 
 This is licensed under either of
diff --git a/metamath-knife/Cargo.toml b/metamath-knife/Cargo.toml
new file mode 100644
index 0000000..f3ace8f
--- /dev/null
+++ b/metamath-knife/Cargo.toml
@@ -0,0 +1,28 @@
+[package]
+name = "metamath-knife"
+readme = "metamath-knife/README.md"
+description = "A command-line tool for Metamath, including parallel and incremental verifier for Metamath databases"
+version = "0.3.9"
+authors.workspace = true
+license.workspace = true
+repository.workspace = true
+keywords.workspace = true
+categories.workspace = true
+edition = "2021"
+
+[dependencies]
+clap = { version = "4.5", features = ["derive"] }
+simple_logger = "5.0"
+annotate-snippets = "0.11"
+metamath-rs = { path = "../metamath-rs" }
+
+[[bin]]
+name = "metamath-knife"
+path = "src/main.rs"
+doc = false
+
+[features]
+default = ["verify_markup"]
+dot = ["metamath-rs/dot"]
+xml = ["metamath-rs/xml"]
+verify_markup = ["metamath-rs/verify_markup"]
diff --git a/metamath-knife/src/list_stmt.rs b/metamath-knife/src/list_stmt.rs
new file mode 100644
index 0000000..f241b73
--- /dev/null
+++ b/metamath-knife/src/list_stmt.rs
@@ -0,0 +1,56 @@
+use metamath_rs::{as_str, Database, StatementRef, StatementType};
+
+pub fn list_statements(
+    db: &Database,
+    label_test: impl Fn(&[u8]) -> bool,
+    out: &mut impl std::io::Write,
+) -> Result<(), std::io::Error> {
+    let separator = "-".repeat(79);
+    let scope = db.scope_result();
+    let name = db.name_result();
+    for stmt in db.statements() {
+        if let StatementType::Axiom | StatementType::Provable = stmt.statement_type() {
+            let label = stmt.label();
+            if label_test(label) {
+                if let Some(frame) = scope.get(label) {
+                    for (ix1, ix2) in &*frame.mandatory_dv {
+                        writeln!(
+                            out,
+                            "$d {} {} $.",
+                            as_str(name.atom_name(frame.var_list[*ix1])),
+                            as_str(name.atom_name(frame.var_list[*ix2]))
+                        )?;
+                    }
+                    for hyp in frame.hypotheses.iter().skip(frame.mandatory_count) {
+                        write_statement(db.statement_by_address(hyp.address()), out)?;
+                    }
+                    write_statement(stmt, out)?;
+                    writeln!(out, "{}", separator)?;
+                }
+            }
+        }
+    }
+    Ok(())
+}
+
+pub fn write_statement(
+    stmt: StatementRef,
+    out: &mut impl std::io::Write,
+) -> Result<(), std::io::Error> {
+    write!(
+        out,
+        "{} ${}",
+        as_str(stmt.label()),
+        match stmt.statement_type() {
+            StatementType::Axiom => "a",
+            StatementType::Essential => "e",
+            StatementType::Provable => "p",
+            _ => "x",
+        }
+    )?;
+    for token in stmt.math_iter() {
+        write!(out, " {}", as_str(&token))?;
+    }
+    writeln!(out)?;
+    Ok(())
+}
diff --git a/metamath-knife/src/main.rs b/metamath-knife/src/main.rs
new file mode 100644
index 0000000..583f05c
--- /dev/null
+++ b/metamath-knife/src/main.rs
@@ -0,0 +1,318 @@
+//! A library for manipulating [Metamath](http://us.metamath.org/#faq)
+//! databases.  The entry point for all API operations is in the `database`
+//! module, as is a discussion of the data representation.
+
+mod list_stmt;
+
+use annotate_snippets::Renderer;
+use clap::error::ErrorKind;
+use clap::{CommandFactory, Parser};
+use list_stmt::list_statements;
+use metamath_rs::database::{Database, DbOptions};
+use metamath_rs::parser::is_valid_label;
+use metamath_rs::statement::StatementAddress;
+use simple_logger::SimpleLogger;
+use std::fs::File;
+use std::io::{self, stdout, BufWriter};
+use std::mem;
+
+/// A Metamath database verifier and processing tool
+#[derive(Debug, clap::Parser)]
+#[command(version, about, verbatim_doc_comment)]
+struct Cli {
+    /// Database file to load
+    #[arg(id("DATABASE"), required_unless_present("text"))]
+    db: Option<String>,
+    /// Provides raw database content on the command line
+    #[arg(long, value_names(&["NAME", "TEXT"]))]
+    text: Vec<String>,
+    /// Processes files > 1 MiB in multiple segments
+    #[arg(long)]
+    split: bool,
+    /// Prints milliseconds after each stage
+    #[arg(long = "time")]
+    timing: bool,
+    /// Checks proof validity
+    #[arg(short, long)]
+    verify: bool,
+    /// Regenerates `discouraged` file
+    #[arg(short = 'D', long, value_name("FILE"))]
+    discouraged: Option<String>,
+    /// Generate `axiom-use` file
+    #[arg(short = 'X', long, value_name("FILE"))]
+    axiom_use: Option<String>,
+    /// Outputs statements directly or indirectly using the given list of statements
+    #[arg(long, value_names(&["FILE", "LABELS"]))]
+    stmt_use: Vec<String>,
+    /// Checks axiom usage
+    #[arg(short = 'u', long)]
+    verify_usage: bool,
+    /// Shows database outline
+    #[arg(short = 'O', long)]
+    outline: bool,
+    /// Dumps typesetting information
+    #[arg(short = 'T', long)]
+    dump_typesetting: bool,
+    /// Parses typesetting information
+    #[arg(short = 't', long)]
+    parse_typesetting: bool,
+    /// Checks grammar
+    #[arg(short, long)]
+    grammar: bool,
+    /// Parses all statements according to the database's grammar
+    #[arg(short, long)]
+    parse_stmt: bool,
+    /// Checks that printing parsed statements gives back the original formulas
+    #[arg(long)]
+    verify_parse_stmt: bool,
+    /// Dumps the database's grammar
+    #[arg(short = 'G', long)]
+    dump_grammar: bool,
+    /// Dumps the formulas of this database
+    #[arg(short = 'F', long)]
+    dump_formula: bool,
+    /// List all statements of this database
+    #[arg(short = 'S', long)]
+    list_statements: bool,
+    /// Activates debug logs, including for the grammar building and statement parsing
+    #[arg(long)]
+    debug: bool,
+    /// Prints segments as they are recalculated
+    #[arg(long)]
+    trace_recalc: bool,
+    /// Explicitly deallocates working memory before exit
+    #[arg(long)]
+    free: bool,
+    /// Demonstrates incremental verifier
+    #[arg(long)]
+    repeat: bool,
+    /// Number of threads to use for verification
+    #[arg(short, long, value_parser = clap::value_parser!(u32).range(1..))]
+    jobs: Option<u32>,
+    /// Outputs a proof file
+    #[arg(short, long, value_name("LABEL"))]
+    export: Vec<String>,
+    /// Supplies a bibliography file for verify-markup
+    /// Can be used one or two times; the second is for exthtml processing
+    #[arg(long, value_name("FILE"))]
+    biblio: Vec<String>,
+    #[cfg(feature = "dot")]
+    /// Export the database's grammar in Graphviz DOT format for visualization
+    #[arg(short = 'E', long)]
+    export_grammar_dot: bool,
+    #[cfg(feature = "xml")]
+    /// Exports all theorem dependencies in the GraphML file format
+    #[arg(long, value_name("FILE"))]
+    export_graphml_deps: Option<String>,
+    #[cfg(feature = "verify_markup")]
+    /// Checks comment markup
+    #[arg(short = 'm', long)]
+    verify_markup: bool,
+}
+
+fn main() {
+    let cli = Cli::parse();
+    let mut cmd = Cli::command();
+
+    let incremental = cli.repeat
+        || cli.grammar
+        || cli.parse_stmt
+        || cli.verify_parse_stmt
+        || cli.dump_grammar
+        || cli.dump_formula;
+    #[cfg(feature = "dot")]
+    let incremental = incremental || cli.export_grammar_dot;
+    let options = DbOptions {
+        autosplit: cli.split,
+        timing: cli.timing,
+        trace_recalc: cli.trace_recalc,
+        incremental,
+        jobs: cli.jobs.unwrap_or(1) as usize,
+    };
+
+    if cli.debug {
+        SimpleLogger::new().init().unwrap();
+    }
+
+    let mut db = Database::new(options);
+
+    let mut data = Vec::new();
+    for kv in cli.text.chunks(2) {
+        data.push((kv[0].clone(), kv[1].clone().into_bytes()));
+    }
+    let start = cli.db.unwrap_or_else(|| data[0].0.clone());
+
+    loop {
+        db.parse(start.clone(), data.clone());
+
+        if cli.verify {
+            db.verify_pass();
+        }
+
+        if cli.grammar {
+            db.grammar_pass();
+        }
+
+        if cli.parse_stmt {
+            db.stmt_parse_pass();
+        }
+
+        if cli.parse_typesetting {
+            db.typesetting_pass();
+        }
+
+        if cli.verify_parse_stmt {
+            db.stmt_parse_pass();
+            db.verify_parse_stmt();
+        }
+
+        if cli.verify_usage {
+            db.verify_usage_pass();
+        }
+
+        let mut diags = db.diag_notations();
+
+        if let Some(discouraged) = &cli.discouraged {
+            File::create(discouraged)
+                .and_then(|file| db.write_discouraged(&mut BufWriter::new(file)))
+                .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
+        }
+
+        #[cfg(feature = "xml")]
+        if let Some(file) = &cli.export_graphml_deps {
+            File::create(file)
+                .map_err(|err| err.into())
+                .and_then(|file| db.export_graphml_deps(&mut BufWriter::new(file)))
+                .unwrap_or_else(|diag| diags.push((StatementAddress::default(), diag)));
+        }
+
+        if let Some(file) = &cli.axiom_use {
+            File::create(file)
+                .and_then(|file| {
+                    db.write_stmt_use(|label| label.starts_with(b"ax-"), &mut BufWriter::new(file))
+                })
+                .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
+        }
+
+        if !cli.stmt_use.is_empty() {
+            let output_file_path = &cli.stmt_use[0];
+            let stmt_list: Vec<_> = cli.stmt_use[1].split(',').map(str::as_bytes).collect();
+            if !stmt_list.iter().copied().all(is_valid_label) {
+                cmd.error(
+                    ErrorKind::InvalidValue,
+                    "Expected list of labels as second argument to --stmt-use",
+                )
+                .exit();
+            }
+            File::create(output_file_path)
+                .and_then(|file| {
+                    db.write_stmt_use(
+                        |label| stmt_list.contains(&label),
+                        &mut BufWriter::new(file),
+                    )
+                })
+                .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
+        }
+
+        if cli.list_statements {
+            db.scope_pass();
+            _ = list_statements(&db, |_label| true, &mut stdout());
+        }
+
+        let r = Renderer::styled();
+        #[allow(unused_mut)]
+        let mut count = db
+            .render_diags(diags, |msg| println!("{}", r.render(msg)))
+            .len();
+
+        #[cfg(feature = "verify_markup")]
+        if cli.verify_markup {
+            use metamath_rs::diag::BibError;
+            use metamath_rs::verify_markup::{Bibliography, Bibliography2};
+
+            db.scope_pass();
+            db.typesetting_pass();
+
+            if cli.biblio.len() > 2 {
+                cmd.error(
+                    ErrorKind::TooManyValues,
+                    "expected at most 2 bibliography files",
+                )
+                .exit()
+            }
+            let sources: Vec<_> = cli
+                .biblio
+                .iter()
+                .map(|val| {
+                    let file = std::fs::read(val).unwrap();
+                    metamath_rs::SourceInfo::new(val.to_owned(), std::sync::Arc::new(file))
+                })
+                .collect();
+            let mut bib_diags = vec![];
+            let mut bibs = sources
+                .iter()
+                .map(|source| Bibliography::parse(source, &mut bib_diags));
+            let bib = bibs.next().map(|base| Bibliography2 {
+                base,
+                ext: bibs.next(),
+            });
+
+            count += BibError::render_list(&bib_diags, |msg| println!("{}", r.render(msg))).len();
+
+            let diags = db.verify_markup(bib.as_ref());
+            count += db
+                .render_diags(diags, |msg| println!("{}", r.render(msg)))
+                .len();
+        }
+
+        println!("{count} diagnostics issued.");
+
+        if cli.dump_grammar {
+            db.grammar_pass();
+            db.dump_grammar();
+        }
+
+        #[cfg(feature = "dot")]
+        if cli.export_grammar_dot {
+            db.grammar_pass();
+            db.export_grammar_dot();
+        }
+
+        if cli.dump_formula {
+            db.stmt_parse_pass();
+            db.dump_formula();
+        }
+
+        if cli.outline {
+            db.outline_pass();
+            db.print_outline();
+        }
+
+        if cli.dump_typesetting {
+            db.typesetting_pass();
+            db.print_typesetting();
+        }
+
+        if !cli.export.is_empty() {
+            db.scope_pass();
+            for file in &cli.export {
+                db.export(file);
+            }
+        }
+
+        if cli.repeat {
+            let mut input = String::new();
+            if io::stdin().read_line(&mut input).unwrap() == 0 {
+                break;
+            }
+        } else {
+            if !cli.free {
+                mem::forget(db);
+            }
+
+            // Exit with code 1 if any warning or error were encountered
+            let code = if count > 0 { 1 } else { 0 };
+            std::process::exit(code);
+        }
+    }
+}
diff --git a/metamath-rs/Cargo.toml b/metamath-rs/Cargo.toml
new file mode 100644
index 0000000..08e1e2c
--- /dev/null
+++ b/metamath-rs/Cargo.toml
@@ -0,0 +1,36 @@
+[package]
+name = "metamath-rs"
+readme = "README.md"
+description = "A library manipulating Metamath databases, including a parallel and incremental verifier for Metamath databases"
+version = "0.3.9"
+authors.workspace = true
+license.workspace = true
+repository.workspace = true
+keywords.workspace = true
+categories.workspace = true
+edition = "2021"
+
+[dependencies]
+itertools = "0.13"
+filetime = "0.2"
+fnv = "1.0"
+regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
+tinyvec = "1.5"
+log = "0.4"
+annotate-snippets = "0.11"
+typed-arena = "2.0"
+
+# Optional dependencies
+dot-writer = { version = "0.1.2", optional = true }
+xml-rs = { version = "0.8.14", optional = true }
+html5ever = { version = "0.27.0", optional = true }
+scraper = { version = "0.19.0", optional = true }
+
+[dev-dependencies]
+assert_matches = "1.5"
+
+[features]
+default = ["verify_markup"]
+dot = ["dot-writer"]
+xml = ["xml-rs"]
+verify_markup = ["scraper", "html5ever"]
diff --git a/metamath-rs/README.md b/metamath-rs/README.md
new file mode 100644
index 0000000..d2a61f2
--- /dev/null
+++ b/metamath-rs/README.md
@@ -0,0 +1,39 @@
+# Metamath-rs - a library for processing Metamath databases
+
+## A what?
+
+Metamath is a language for expressing formal proofs in mathematics. Metamath makes few assumptions on the underlying logic and is simple enough to support a wide variety of tools.
+See http://us.metamath.org/#faq.
+
+Metamath-rs can rapidly verify these proofs, providing much stronger confidence that the proof is correct. And we do mean *rapid*: over 28,000 proofs can be proved in less than a second.
+
+Metamath-rs is the library component of the [metamath-knife](https://github.com/metamath/metamath-knife) project, which also contains a standalone command-line application.
+
+* It supports *all* Metamath proof formats. In particular, Metamath-knife
+  adds support for *all* Metamath proof formats
+  (<a href="https://groups.google.com/g/metamath/c/xCUNA2ttHew/m/RXSNzdovBAAJ">uncompressed, compressed, package, or explicit</a>.
+* We take extra steps to prevent errors, e.g., we have a CI pipeline
+  (implemented using GitHub actions).
+* We remove deprecated constructs, e.g., the deprecated try!(...)
+  has been replaced with the easier-to-read "?" construct.
+* We actively work to eliminate compiler warnings. This tends to
+  counter errors, make the code more readable, and improve performance
+  (e.g., by eliminating unnecessary clone() calls).
+
+## License
+
+This is licensed under either of
+
+ * Apache License, Version 2.0 ([LICENSE-APACHE](LICENSE-APACHE) or http://www.apache.org/licenses/LICENSE-2.0)
+ * MIT license ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT)
+
+The SPDX license expression for its license is "(MIT OR Apache-2.0)".
+
+Note that this is exactly the same license as smetamath-rs (SMM3),
+That is intentional, because we want smetamath-rs (SMM3) to be able to
+re-incorporate whatever we do if they like.
+
+### Contribution
+
+Unless you explicitly state otherwise, any contribution intentionally submitted
+for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.
diff --git a/metamath-rs/src/axiom_use.rs b/metamath-rs/src/axiom_use.rs
new file mode 100644
index 0000000..a8bf1e7
--- /dev/null
+++ b/metamath-rs/src/axiom_use.rs
@@ -0,0 +1,175 @@
+//! Generation of the `axiom_use` file.
+use std::sync::Arc;
+
+use itertools::PeekingNext;
+
+use crate::bit_set::Bitset;
+use crate::diag::Diagnostic;
+use crate::segment::SegmentRef;
+use crate::segment_set::SegmentSet;
+use crate::statement::{CommandToken, StatementAddress, TokenPtr};
+use crate::util::HashMap;
+use crate::StatementType;
+use crate::{as_str, database::time, Database};
+
+/// Diagnostics issued when checking axiom usage in the Database.
+///
+#[derive(Debug, Default)]
+pub struct UsageResult(Vec<(StatementAddress, Diagnostic)>);
+
+impl UsageResult {
+    /// Returns the list of errors that were generated during the usage check pass.
+    #[must_use]
+    pub fn diagnostics(&self) -> Vec<(StatementAddress, Diagnostic)> {
+        self.0.clone()
+    }
+}
+
+struct UsagePass<'a> {
+    axiom_use_map: HashMap<TokenPtr<'a>, Bitset>,
+    axioms: Vec<TokenPtr<'a>>,
+    result: &'a mut UsageResult,
+}
+
+impl<'a> UsagePass<'a> {
+    // Parses the 'usage' commmands in the database,
+    fn parse_command(
+        &self,
+        sref: SegmentRef<'_>,
+        args: &[CommandToken],
+    ) -> Result<(), Vec<Diagnostic>> {
+        use CommandToken::*;
+        let buf = &**sref.buffer;
+        match args {
+            [Keyword(cmd), label, Keyword(avoids), axioms @ ..]
+                if cmd.as_ref(buf) == b"usage" && avoids.as_ref(buf) == b"avoids" =>
+            {
+                let stmt = &*label.value(buf);
+                let usage = self
+                    .axiom_use_map
+                    .get(stmt)
+                    .ok_or_else(|| vec![Diagnostic::UnknownLabel(label.full_span())])?;
+                let mut diags = vec![];
+                for cmd in axioms {
+                    let axiom = &*cmd.value(buf);
+                    if let Some(index) = self.axioms.iter().position(|&x| x == axiom) {
+                        if usage.has_bit(index) {
+                            // TODO possibly research the usage "path" leading to this error.
+                            diags.push(Diagnostic::UsageViolation(
+                                cmd.full_span(),
+                                stmt.into(),
+                                axiom.into(),
+                            ));
+                        }
+                    }
+                }
+                Err(diags)
+            }
+            _ => Ok(()),
+        }
+    }
+
+    /// Verify that all usage declarations are correct.
+    fn verify_usage(&'a mut self, sset: &'a SegmentSet) {
+        for sref in sset.segments(..) {
+            let mut j_commands: std::slice::Iter<'_, (i32, (crate::Span, Vec<CommandToken>))> =
+                sref.j_commands.iter();
+            for stmt in sref.range(..) {
+                match stmt.statement_type() {
+                    StatementType::AdditionalInfoComment => {
+                        while let Some(&(_, (_, ref args))) =
+                            j_commands.peeking_next(|i| i.0 == stmt.index)
+                        {
+                            if let Err(diags) = self.parse_command(sref, args) {
+                                for diag in diags {
+                                    self.result.0.push((stmt.address(), diag));
+                                }
+                            }
+                        }
+                    }
+                    StatementType::Provable => {
+                        let label = stmt.label();
+                        let mut usage = Bitset::new();
+                        let mut i = 1;
+                        loop {
+                            let tk = stmt.proof_slice_at(i);
+                            i += 1;
+                            if tk == b")" {
+                                break;
+                            }
+                            if let Some(usage2) = self.axiom_use_map.get(tk) {
+                                usage |= usage2
+                            }
+                            if i == stmt.proof_len() {
+                                break;
+                            }
+                        }
+                        self.axiom_use_map.insert(label, usage);
+                    }
+                    StatementType::Axiom => {
+                        let label = stmt.label();
+                        if label.starts_with(b"ax-") {
+                            let mut usage = Bitset::new();
+                            usage.set_bit(self.axioms.len());
+                            self.axioms.push(label);
+                            self.axiom_use_map.insert(label, usage);
+                        }
+                    }
+                    _ => {}
+                }
+            }
+        }
+    }
+}
+
+/// Verify the axiom usage
+pub(crate) fn verify_usage(sset: &Arc<SegmentSet>, usage: &mut UsageResult) {
+    UsagePass {
+        axiom_use_map: HashMap::default(),
+        axioms: vec![],
+        result: usage,
+    }
+    .verify_usage(sset);
+}
+
+impl Database {
+    /// Writes a `stmt_use` file to the given writer.
+    pub fn write_stmt_use(
+        &self,
+        label_test: impl Fn(&[u8]) -> bool,
+        out: &mut impl std::io::Write,
+    ) -> Result<(), std::io::Error> {
+        time(&self.options.clone(), "stmt_use", || {
+            let mut stmt_use_map = HashMap::default();
+            let mut stmt_list = vec![];
+            for sref in self.statements().filter(|stmt| stmt.is_assertion()) {
+                let label = sref.label();
+                let mut usage = Bitset::new();
+                if label_test(label) {
+                    usage.set_bit(stmt_list.len());
+                    stmt_list.push(as_str(label));
+                    stmt_use_map.insert(label, usage);
+                } else if sref.statement_type() == StatementType::Provable {
+                    let mut i = 1;
+                    loop {
+                        let tk = sref.proof_slice_at(i);
+                        i += 1;
+                        if tk == b")" {
+                            break;
+                        }
+                        if let Some(usage2) = stmt_use_map.get(tk) {
+                            usage |= usage2
+                        }
+                    }
+                    write!(out, "{}:", as_str(label))?;
+                    for i in &usage {
+                        write!(out, " {}", stmt_list[i])?;
+                    }
+                    writeln!(out)?;
+                    stmt_use_map.insert(label, usage);
+                }
+            }
+            Ok(())
+        })
+    }
+}
diff --git a/src/bit_set.rs b/metamath-rs/src/bit_set.rs
similarity index 96%
rename from src/bit_set.rs
rename to metamath-rs/src/bit_set.rs
index 54d004c..4afb879 100644
--- a/src/bit_set.rs
+++ b/metamath-rs/src/bit_set.rs
@@ -60,6 +60,7 @@ impl Bitset {
     }
 
     fn tail(&self) -> &[usize] {
+        #[allow(clippy::manual_unwrap_or_default)] // clippy#12928
         match self.tail {
             None => Default::default(),
             Some(ref bx) => bx,
@@ -128,6 +129,11 @@ impl Bitset {
                 Some(bx) => bx.iter().all(|&word| word == 0),
             }
     }
+
+    /// Returns an iterator over the indices of set bits in the bitset.
+    pub fn iter(&self) -> BitsetIter<'_> {
+        self.into_iter()
+    }
 }
 
 impl<'a> BitOrAssign<&'a Bitset> for Bitset {
diff --git a/src/comment_parser.rs b/metamath-rs/src/comment_parser.rs
similarity index 78%
rename from src/comment_parser.rs
rename to metamath-rs/src/comment_parser.rs
index c976eeb..0ab7962 100644
--- a/src/comment_parser.rs
+++ b/metamath-rs/src/comment_parser.rs
@@ -14,12 +14,11 @@
 //! corresponding byte string in the file has to be unescaped before
 //! interpretation, using the [`CommentParser::unescape_text`] and
 //! [`CommentParser::unescape_math`] functions.
-use std::fmt::Display;
+use std::{fmt::Display, sync::OnceLock};
 
-use lazy_static::lazy_static;
 use regex::bytes::{CaptureMatches, Match, Regex, RegexSet};
 
-use crate::Span;
+use crate::{statement::unescape, Span};
 
 /// A comment markup item, which represents either a piece of text from the input
 /// or some kind of metadata item like the start or end of an italicized group.
@@ -27,32 +26,32 @@ use crate::Span;
 pub enum CommentItem {
     /// A piece of regular text. The characters in the buffer at the given
     /// span should be interpreted literally, except for the escapes.
-    /// Use `unescape_text` to strip the text escapes `[`, `~`, and `` ` ``.
-    /// Note that `[` can also appear unescaped.
+    /// Use `unescape_text` to strip the text escapes `[`, `~`, `` ` ``, and `_`.
+    /// Note that `[` and `_` can also appear unescaped.
     Text(Span),
     /// A paragraph break, caused by two or more consecutive newlines in the input.
     /// This is a zero-length item (all characters will be present in `Text` nodes
     /// before and after the element), but corresponds roughly to a `<p>` tag in HTML.
     LineBreak(usize),
     /// Start math mode, indicated by a backtick character. The usize points to the character.
-    /// Between [`StartMathMode`] and [`EndMathMode`],
-    /// there will be no comment items other than [`MathToken`].
+    /// Between [`CommentItem::StartMathMode`] and [`CommentItem::EndMathMode`],
+    /// there will be no comment items other than [`CommentItem::MathToken`].
     StartMathMode(usize),
     /// End math mode, indicated by a backtick character. The usize points to the character.
-    /// Between [`StartMathMode`] and [`EndMathMode`],
-    /// there will be no comment items other than [`MathToken`].
+    /// Between [`CommentItem::StartMathMode`] and [`CommentItem::EndMathMode`],
+    /// there will be no comment items other than [`CommentItem::MathToken`].
     EndMathMode(usize),
     /// A single math token. After unescaping this should correspond to a `$c` or `$v` statement
     /// in the database.
     /// Use `unescape_math` to strip the escape character `` ` ``.
     MathToken(Span),
     /// A label of an existing theorem. The `usize` points to the `~` character.
-    /// Use `unescape_text` to strip the text escapes `[`, `~`, and `` ` ``.
-    /// Note that `[` and `~` can also appear unescaped.
+    /// Use `unescape_text` to strip the text escapes `[`, `~`, `` ` ``, and `_`.
+    /// Note that `[`, `~`, `_` can also appear unescaped.
     Label(usize, Span),
     /// A link to a web site URL. The `usize` points to the `~` character.
-    /// Use `unescape_text` to strip the text escapes `[`, `~`, and `` ` ``.
-    /// Note that `[` and `~` can also appear unescaped.
+    /// Use `unescape_text` to strip the text escapes `[`, `~`, `` ` ``, and `_`.
+    /// Note that `[`, `~`, `_` can also appear unescaped.
     Url(usize, Span),
     /// The `<HTML>` keyword, which starts HTML mode
     /// (it doesn't actually put `<HTML>` in the output).
@@ -73,28 +72,20 @@ pub enum CommentItem {
     BibTag(Span),
 }
 
+/// Returns true if this is a character that is escaped in [`CommentItem::Text`] fields,
+/// meaning that doubled occurrences are turned into single occurrences.
 #[inline]
-fn unescape(mut buf: &[u8], out: &mut Vec<u8>, is_escape: impl FnOnce(u8) -> bool + Copy) {
-    while let Some(n) = buf.iter().position(|&c| is_escape(c)) {
-        out.extend_from_slice(&buf[..=n]);
-        if buf.get(n + 1) == Some(&buf[n]) {
-            buf = &buf[n + 2..];
-        } else {
-            // this will not normally happen, but in some cases unescaped escapes
-            // are left uninterpreted because they appear in invalid position,
-            // and in that case they should be left as is
-            buf = &buf[n + 1..];
-        }
-    }
-    out.extend_from_slice(buf);
+#[must_use]
+pub const fn is_text_escape(html_mode: bool, c: u8) -> bool {
+    matches!(c, b'`' | b'[' | b'~') || !html_mode && c == b'_'
 }
 
-/// Returns true if this is a character that is escaped in [`CommentItem::Text`],
+/// Returns true if this is a character that is escaped in
 /// [`CommentItem::Label`] and [`CommentItem::Url`] fields,
 /// meaning that doubled occurrences are turned into single occurrences.
 #[inline]
 #[must_use]
-pub const fn is_text_escape(c: u8) -> bool {
+pub const fn is_label_escape(c: u8) -> bool {
     matches!(c, b'`' | b'[' | b'~')
 }
 
@@ -108,9 +99,15 @@ pub const fn is_math_escape(c: u8) -> bool {
 
 impl CommentItem {
     /// Remove text escapes from a markup segment `buf`, generally coming from the
-    /// [`CommentItem::Text`], [`CommentItem::Label`], or [`CommentItem::Url`] fields.
-    pub fn unescape_text(buf: &[u8], out: &mut Vec<u8>) {
-        unescape(buf, out, is_text_escape)
+    /// [`CommentItem::Text`] field.
+    pub fn unescape_text(html_mode: bool, buf: &[u8], out: &mut Vec<u8>) {
+        unescape(buf, out, |c| is_text_escape(html_mode, c))
+    }
+
+    /// Remove text escapes from a markup segment `buf`, generally coming from the
+    /// [`CommentItem::Label`] or [`CommentItem::Url`] fields.
+    pub fn unescape_label(buf: &[u8], out: &mut Vec<u8>) {
+        unescape(buf, out, is_label_escape)
     }
 
     /// Remove math escapes from a markup segment `buf`, generally coming from the
@@ -140,6 +137,8 @@ pub struct CommentParser<'a> {
     end_subscript: usize,
 }
 
+const CLOSING_PUNCTUATION: &[u8] = b".,;)?!:]'\"_-";
+
 impl<'a> CommentParser<'a> {
     /// Construct a new `CommentParser` from a sub-span of a buffer.
     /// The returned comment items will have spans based on the input span,
@@ -158,9 +157,15 @@ impl<'a> CommentParser<'a> {
     }
 
     /// Remove text escapes from a markup segment `span`, generally coming from the
-    /// [`CommentItem::Text`], [`CommentItem::Label`], or [`CommentItem::Url`] fields.
+    /// [`CommentItem::Text`] field.
     pub fn unescape_text(&self, span: Span, out: &mut Vec<u8>) {
-        CommentItem::unescape_text(span.as_ref(self.buf), out)
+        CommentItem::unescape_text(self.html_mode, span.as_ref(self.buf), out)
+    }
+
+    /// Remove text escapes from a markup segment `span`, generally coming from the
+    /// [`CommentItem::Label`] or [`CommentItem::Url`] fields.
+    pub fn unescape_label(&self, span: Span, out: &mut Vec<u8>) {
+        CommentItem::unescape_label(span.as_ref(self.buf), out)
     }
 
     /// Remove math escapes from a markup segment `span`, generally coming from the
@@ -184,20 +189,7 @@ impl<'a> CommentParser<'a> {
         None
     }
 
-    fn is_subscript(&self) -> Option<()> {
-        const OPENING_PUNCTUATION: &[u8] = b"(['\"";
-        if self.pos == self.end_subscript {
-            return None;
-        }
-        let c = self.buf.get(self.pos.checked_sub(1)?)?;
-        if c.is_ascii_whitespace() || OPENING_PUNCTUATION.contains(c) {
-            return None;
-        }
-        Some(())
-    }
-
     fn parse_subscript(&self) -> Option<usize> {
-        const CLOSING_PUNCTUATION: &[u8] = b".,;)?!:]'\"_-";
         let c = self.buf.get(self.pos + 1)?;
         if c.is_ascii_whitespace() || CLOSING_PUNCTUATION.contains(c) {
             return None;
@@ -217,7 +209,18 @@ impl<'a> CommentParser<'a> {
         if !self.buf.get(self.pos + 1)?.is_ascii_alphanumeric() {
             return None;
         }
-        let end = (self.pos + 2) + self.buf[self.pos + 2..].iter().position(|&c| c == b'_')?;
+        let mut end = self.pos + 2;
+        loop {
+            if *self.buf.get(end)? == b'_' {
+                if self.buf.get(end + 1) == Some(&b'_') {
+                    end += 2
+                } else {
+                    break;
+                }
+            } else {
+                end += 1
+            }
+        }
         if !self.buf[end - 1].is_ascii_alphanumeric()
             || matches!(self.buf.get(end + 1), Some(c) if c.is_ascii_alphanumeric())
         {
@@ -227,17 +230,22 @@ impl<'a> CommentParser<'a> {
     }
 
     fn parse_underscore(&mut self) -> Option<(usize, CommentItem)> {
+        const OPENING_PUNCTUATION: &[u8] = b"(['\"";
         let start = self.pos;
-        let item = if self.is_subscript().is_some() {
-            let sub_end = self.parse_subscript()?;
-            self.pos += 1;
-            self.end_subscript = sub_end;
-            CommentItem::StartSubscript(start)
-        } else {
+        let is_italic = self.pos == self.end_subscript
+            || (self.pos.checked_sub(1).and_then(|pos| self.buf.get(pos))).map_or(true, |c| {
+                c.is_ascii_whitespace() || OPENING_PUNCTUATION.contains(c)
+            });
+        let item = if is_italic {
             let it_end = self.parse_italic()?;
             self.pos += 1;
             self.end_italic = it_end;
             CommentItem::StartItalic(start)
+        } else {
+            let sub_end = self.parse_subscript()?;
+            self.pos += 1;
+            self.end_subscript = sub_end;
+            CommentItem::StartSubscript(start)
         };
         Some((start, item))
     }
@@ -295,7 +303,7 @@ impl<'a> CommentParser<'a> {
         while let Some(&c) = self.buf.get(self.pos) {
             match c {
                 b'[' | b'`' if self.buf.get(self.pos + 1) == Some(&c) => self.pos += 2,
-                b' ' | b'\n' | b'`' => break,
+                b' ' | b'\r' | b'\n' | b'`' => break,
                 b'[' if self.parse_bib().is_some() => break,
                 b'<' if self.buf[self.pos..].starts_with(b"<HTML>")
                     || self.buf[self.pos..].starts_with(b"</HTML>") =>
@@ -315,11 +323,31 @@ impl<'a> CommentParser<'a> {
             CommentItem::Label(tilde, Span::new(label_start, self.pos))
         }
     }
+
+    fn trim_space_before_open(&self, lo: usize, pos: usize) -> bool {
+        lo + 2 <= pos
+            && self.buf[pos - 1] == b' '
+            && (b"([".contains(&self.buf[pos - 2])
+                || self.buf[pos - 2] == b'\"'
+                    && pos
+                        .checked_sub(3)
+                        .and_then(|i| self.buf.get(i))
+                        .map_or(true, u8::is_ascii_whitespace))
+    }
+
+    fn trim_space_after_close(&self) -> bool {
+        self.buf.get(self.pos) == Some(&b' ')
+            && self
+                .buf
+                .get(self.pos + 1)
+                .map_or(false, |c| CLOSING_PUNCTUATION.contains(c))
+    }
 }
 
 impl<'a> Iterator for CommentParser<'a> {
     type Item = CommentItem;
 
+    #[allow(clippy::cognitive_complexity)]
     fn next(&mut self) -> Option<Self::Item> {
         if let Some(item) = self.item.take() {
             return Some(item);
@@ -339,6 +367,13 @@ impl<'a> Iterator for CommentParser<'a> {
                     end = self.pos;
                     self.pos += 1;
                     self.item = Some(self.parse_math_delim(end));
+                    if self.math_mode && self.trim_space_before_open(start, end) {
+                        // trim a single space if we are opening math mode after opening punct
+                        end -= 1;
+                    } else if !self.math_mode && self.trim_space_after_close() {
+                        // trim a single space if we are exiting math mode before closing punct
+                        self.pos += 1;
+                    }
                     break;
                 }
             } else if math_token {
@@ -361,7 +396,15 @@ impl<'a> Iterator for CommentParser<'a> {
                     self.pos += 2;
                 } else {
                     end = self.pos;
+                    if self.trim_space_before_open(start, end) {
+                        // trim a single space if we have a label after opening punct
+                        end -= 1;
+                    }
                     self.item = Some(self.parse_label());
+                    if self.trim_space_after_close() {
+                        // trim a single space if we have a label before closing punct
+                        self.pos += 1;
+                    }
                     break;
                 }
             } else if c == b'[' {
@@ -385,18 +428,20 @@ impl<'a> Iterator for CommentParser<'a> {
                 }
                 self.pos += 1;
             } else if c == b'_' {
-                if self.end_italic == self.pos {
+                if self.buf.get(self.pos + 1) == Some(&b'_') {
+                    self.pos += 2;
+                } else if self.end_italic == self.pos {
                     end = self.pos;
                     self.pos += 1;
                     self.item = Some(CommentItem::EndItalic(end));
                     break;
-                }
-                if let Some((pos, item)) = self.parse_underscore() {
+                } else if let Some((pos, item)) = self.parse_underscore() {
                     end = pos;
                     self.item = Some(item);
                     break;
+                } else {
+                    self.pos += 1;
                 }
-                self.pos += 1;
             } else {
                 self.pos += 1;
             }
@@ -427,14 +472,15 @@ impl Discouragements {
     /// is discouraged.
     #[must_use]
     pub fn new(buf: &[u8]) -> Self {
-        lazy_static! {
-            static ref MODIFICATION: RegexSet = RegexSet::new([
-                r"\(Proof[ \n]+modification[ \n]+is[ \n]+discouraged\.\)",
-                r"\(New[ \n]+usage[ \n]+is[ \n]+discouraged\.\)"
+        static MODIFICATION: OnceLock<RegexSet> = OnceLock::new();
+        let modification = MODIFICATION.get_or_init(|| {
+            RegexSet::new([
+                r"\(Proof[ \r\n]+modification[ \r\n]+is[ \r\n]+discouraged\.\)",
+                r"\(New[ \r\n]+usage[ \r\n]+is[ \r\n]+discouraged\.\)",
             ])
-            .unwrap();
-        }
-        let m = MODIFICATION.matches(buf);
+            .unwrap()
+        });
+        let m = modification.matches(buf);
         Self {
             modification_discouraged: m.matched(0),
             usage_discouraged: m.matched(1),
@@ -486,17 +532,17 @@ impl<'a> ParentheticalIter<'a> {
     /// Construct a new parenthetical iterator given a segment buffer and a span in it.
     #[must_use]
     pub fn new(buf: &'a [u8], span: Span) -> Self {
-        lazy_static! {
-            static ref PARENTHETICALS: Regex = Regex::new(concat!(
-                r"\((Contributed|Revised|Proof[ \n]+shortened)",
-                r"[ \n]+by[ \n]+([^,)]+),[ \n]+([0-9]{1,2}-[A-Z][a-z]{2}-[0-9]{4})\.\)|",
-                r"\((Proof[ \n]+modification|New[ \n]+usage)[ \n]+is[ \n]+discouraged\.\)",
+        static PARENTHETICALS: OnceLock<Regex> = OnceLock::new();
+        let parentheticals = PARENTHETICALS.get_or_init(|| {
+            Regex::new(concat!(
+                r"\((Contributed|Revised|Proof[ \r\n]+shortened)",
+                r"[ \r\n]+by[ \r\n]+([^,)]+),[ \r\n]+([0-9]{1,2}-[A-Z][a-z]{2}-[0-9]{4})\.\)|",
+                r"\((Proof[ \r\n]+modification|New[ \r\n]+usage)[ \r\n]+is[ \r\n]+discouraged\.\)",
             ))
-            .unwrap();
-        }
-
+            .unwrap()
+        });
         Self {
-            matches: PARENTHETICALS.captures_iter(span.as_ref(buf)),
+            matches: parentheticals.captures_iter(span.as_ref(buf)),
             off: span.start,
         }
     }
diff --git a/src/comment_parser_tests.rs b/metamath-rs/src/comment_parser_tests.rs
similarity index 84%
rename from src/comment_parser_tests.rs
rename to metamath-rs/src/comment_parser_tests.rs
index 5231c28..6abf6b8 100644
--- a/src/comment_parser_tests.rs
+++ b/metamath-rs/src/comment_parser_tests.rs
@@ -94,6 +94,40 @@ fn test_italic() {
     );
 }
 
+#[test]
+fn test_space_around_math() {
+    check(
+        b"a ` b ` c ~ d e",
+        &[
+            Text(Span::new(0, 2)),
+            StartMathMode(2),
+            MathToken(Span::new(4, 5)),
+            EndMathMode(6),
+            Text(Span::new(7, 10)),
+            Label(10, Span::new(12, 13)),
+            Text(Span::new(13, 15)),
+        ],
+    );
+    check(
+        b"\" ` x ` \" and ~x .",
+        &[
+            Text(Span::new(0, 1)),
+            StartMathMode(2),
+            MathToken(Span::new(4, 5)),
+            EndMathMode(6),
+            Text(Span::new(8, 14)),
+            Label(14, Span::new(15, 16)),
+            Text(Span::new(17, 18)),
+        ],
+    );
+}
+
+/// Two underscores in a row are treated as normal text.
+#[test]
+fn test_double_underscore() {
+    check(b"MINIMIZE__WITH", &[Text(Span::new(0, 14))])
+}
+
 #[test]
 fn test_bib() {
     check(
@@ -181,7 +215,7 @@ fn edge_cases() {
             StartMathMode(0),
             MathToken(Span::new(2, 3)),
             EndMathMode(4),
-            Text(Span::new(5, 8)),
+            Text(Span::new(6, 8)),
         ],
     );
 
@@ -190,6 +224,10 @@ fn edge_cases() {
         b"~</HTML>",
         &[Label(0, Span::new(1, 1)), Text(Span::new(1, 8))],
     );
+    check(
+        b"_a__b_",
+        &[StartItalic(0), Text(Span::new(1, 5)), EndItalic(5)],
+    );
 }
 
 #[test]
@@ -202,6 +240,10 @@ fn test_label() {
         b"Visit ~http://example.com",
         &[Text(Span::new(0, 6)), Url(6, Span::new(7, 25))],
     );
+    check(
+        b"test ~ https://a_b__c.com",
+        &[Text(Span::new(0, 5)), Url(5, Span::new(7, 25))],
+    );
 }
 
 #[test]
@@ -284,6 +326,16 @@ fn test_discouragements() {
             usage_discouraged: true,
         }
     );
+    assert_eq!(
+        Discouragements::new(
+            b"A false axiom, experimental.  (Proof modification\r\n\
+            is discouraged.)  (New usage is discouraged.)"
+        ),
+        Discouragements {
+            modification_discouraged: true,
+            usage_discouraged: true,
+        }
+    );
 }
 
 #[track_caller]
diff --git a/src/database.rs b/metamath-rs/src/database.rs
similarity index 85%
rename from src/database.rs
rename to metamath-rs/src/database.rs
index bbb4b90..f8f7998 100644
--- a/src/database.rs
+++ b/metamath-rs/src/database.rs
@@ -98,9 +98,9 @@
 //! estimated runtime.  This requires an additional argument when queueing.
 
 use crate::as_str;
+use crate::axiom_use::UsageResult;
 use crate::diag;
 use crate::diag::Diagnostic;
-use crate::diag::DiagnosticClass;
 use crate::export;
 use crate::formula::Formula;
 use crate::formula::Label;
@@ -122,7 +122,7 @@ use crate::typesetting::TypesettingData;
 use crate::verify;
 use crate::verify::VerifyResult;
 use crate::StatementRef;
-use annotate_snippets::snippet::Snippet;
+use annotate_snippets::Message;
 use std::cmp::Ordering;
 use std::collections::BinaryHeap;
 use std::fmt;
@@ -225,6 +225,7 @@ fn queue_work(exec: &Executor, estimate: usize, mut f: Box<dyn FnMut() + Send>)
     let mut wq = exec.mutex.lock().unwrap();
     wq.push(Job(estimate, f));
     exec.work_cv.notify_one();
+    drop(wq);
 }
 
 impl Executor {
@@ -290,6 +291,7 @@ impl Executor {
                     panic::AssertUnwindSafe(task_o.take().expect("should only be called once"));
                 *g = Some(panic::catch_unwind(task_f));
                 partsc.1.notify_one();
+                drop(g);
             }),
         );
 
@@ -397,6 +399,7 @@ pub struct Database {
     scopes: Option<Arc<ScopeResult>>,
     prev_verify: Option<Arc<VerifyResult>>,
     verify: Option<Arc<VerifyResult>>,
+    usage: Option<Arc<UsageResult>>,
     typesetting: Option<Arc<TypesettingData>>,
     outline: Option<Arc<Outline>>,
     grammar: Option<Arc<Grammar>>,
@@ -450,6 +453,7 @@ impl Database {
             nameset: None,
             scopes: None,
             verify: None,
+            usage: None,
             typesetting: None,
             outline: None,
             grammar: None,
@@ -495,6 +499,7 @@ impl Database {
             self.nameset = None;
             self.scopes = None;
             self.verify = None;
+            self.usage = None;
             self.typesetting = None;
             self.outline = None;
             self.grammar = None;
@@ -527,7 +532,7 @@ impl Database {
     #[must_use]
     pub fn name_result(&self) -> &Arc<Nameset> {
         self.nameset.as_ref().expect(
-            "The database has not run `name_pass()`. Please ensure it is run before calling depdending methods."
+            "The database has not run `name_pass()`. Please ensure it is run before calling depending methods."
         )
     }
 
@@ -551,6 +556,17 @@ impl Database {
         self.scope_result()
     }
 
+    /// Returns the frames for this database, i.e. the actual logical system.
+    /// Returns `None` if [`Database::scope_pass`] was not previously called.
+    ///
+    /// All logical properties of the database (as opposed to surface syntactic
+    /// properties) can be obtained from this object.
+    #[inline]
+    #[must_use]
+    pub const fn try_scope_result(&self) -> Option<&Arc<ScopeResult>> {
+        self.scopes.as_ref()
+    }
+
     /// Returns the frames for this database, i.e. the actual logical system.
     /// Panics if [`Database::scope_pass`] was not previously called.
     ///
@@ -559,8 +575,8 @@ impl Database {
     #[inline]
     #[must_use]
     pub fn scope_result(&self) -> &Arc<ScopeResult> {
-        self.scopes.as_ref().expect(
-            "The database has not run `scope_pass()`. Please ensure it is run before calling depdending methods."
+        self.try_scope_result().expect(
+            "The database has not run `scope_pass()`. Please ensure it is run before calling depending methods."
         )
     }
 
@@ -585,6 +601,17 @@ impl Database {
         self.verify_result()
     }
 
+    /// Returns verification information for the database.
+    /// Returns `None` if [`Database::verify_pass`] was not previously called.
+    ///
+    /// This is an optimized verifier which returns no useful information other
+    /// than error diagnostics.  It does not save any parsed proof data.
+    #[inline]
+    #[must_use]
+    pub const fn try_verify_result(&self) -> Option<&Arc<VerifyResult>> {
+        self.verify.as_ref()
+    }
+
     /// Returns verification information for the database.
     /// Panics if [`Database::verify_pass`] was not previously called.
     ///
@@ -593,11 +620,38 @@ impl Database {
     #[inline]
     #[must_use]
     pub fn verify_result(&self) -> &Arc<VerifyResult> {
-        self.verify.as_ref().expect(
-            "The database has not run `verify_pass()`. Please ensure it is run before calling depdending methods."
+        self.try_verify_result().expect(
+            "The database has not run `verify_pass()`. Please ensure it is run before calling depending methods."
         )
     }
 
+    /// Calculates and returns axiom usage information for the database.
+    ///
+    /// This is an optimized verifier which returns no useful information other
+    /// than error diagnostics.  It does not save any parsed proof data.
+    pub fn verify_usage_pass(&mut self) -> &Arc<UsageResult> {
+        if self.usage.is_none() {
+            time(&self.options.clone(), "usage", || {
+                let parse = self.parse_result();
+                let mut usage = UsageResult::default();
+                crate::axiom_use::verify_usage(parse, &mut usage);
+                self.usage = Some(Arc::new(usage));
+            });
+        }
+        self.usage.as_ref().unwrap()
+    }
+
+    /// Returns axiom usage verification information for the database.
+    /// Returns `None` if [`Database::verify_usage_pass`] was not previously called.
+    ///
+    /// This is an optimized verifier which returns no useful information other
+    /// than error diagnostics.  It does not save any parsed proof data.
+    #[inline]
+    #[must_use]
+    pub const fn try_usage_result(&self) -> Option<&Arc<UsageResult>> {
+        self.usage.as_ref()
+    }
+
     /// Computes and returns the typesetting data.
     pub fn typesetting_pass(&mut self) -> &Arc<TypesettingData> {
         if self.typesetting.is_none() {
@@ -609,13 +663,21 @@ impl Database {
         self.typesetting_result()
     }
 
+    /// Returns the typesetting data.
+    /// Returns `None` if [`Database::typesetting_pass`] was not previously called.
+    #[inline]
+    #[must_use]
+    pub const fn try_typesetting_result(&self) -> Option<&Arc<TypesettingData>> {
+        self.typesetting.as_ref()
+    }
+
     /// Returns the typesetting data.
     /// Panics if [`Database::typesetting_pass`] was not previously called.
     #[inline]
     #[must_use]
     pub fn typesetting_result(&self) -> &Arc<TypesettingData> {
-        self.typesetting.as_ref().expect(
-            "The database has not run `typesetting_pass()`. Please ensure it is run before calling depdending methods."
+        self.try_typesetting_result().expect(
+            "The database has not run `typesetting_pass()`. Please ensure it is run before calling depending methods."
         )
     }
 
@@ -630,13 +692,21 @@ impl Database {
         self.outline_result()
     }
 
+    /// Returns the root node of the outline.
+    /// Panics if [`Database::outline_pass`] was not previously called.
+    #[inline]
+    #[must_use]
+    pub const fn try_outline_result(&self) -> Option<&Arc<Outline>> {
+        self.outline.as_ref()
+    }
+
     /// Returns the root node of the outline.
     /// Panics if [`Database::outline_pass`] was not previously called.
     #[inline]
     #[must_use]
     pub fn outline_result(&self) -> &Arc<Outline> {
-        self.outline.as_ref().expect(
-            "The database has not run `outline_pass()`. Please ensure it is run before calling depdending methods."
+        self.try_outline_result().expect(
+            "The database has not run `outline_pass()`. Please ensure it is run before calling depending methods."
         )
     }
 
@@ -652,13 +722,21 @@ impl Database {
         self.grammar_result()
     }
 
+    /// Returns the grammar.
+    /// Returns `None` if [`Database::grammar_pass`] was not previously called.
+    #[inline]
+    #[must_use]
+    pub const fn try_grammar_result(&self) -> Option<&Arc<Grammar>> {
+        self.grammar.as_ref()
+    }
+
     /// Returns the grammar.
     /// Panics if [`Database::grammar_pass`] was not previously called.
     #[inline]
     #[must_use]
     pub fn grammar_result(&self) -> &Arc<Grammar> {
-        self.grammar.as_ref().expect(
-            "The database has not run `grammar_pass()`. Please ensure it is run before calling depdending methods."
+        self.try_grammar_result().expect(
+            "The database has not run `grammar_pass()`. Please ensure it is run before calling depending methods."
         )
     }
 
@@ -680,13 +758,21 @@ impl Database {
         self.stmt_parse_result()
     }
 
+    /// Returns the statements parsed using the grammar.
+    /// Returns `None` if [`Database::stmt_parse_pass`] was not previously called.
+    #[inline]
+    #[must_use]
+    pub const fn try_stmt_parse_result(&self) -> Option<&Arc<StmtParse>> {
+        self.stmt_parse.as_ref()
+    }
+
     /// Returns the statements parsed using the grammar.
     /// Panics if [`Database::stmt_parse_pass`] was not previously called.
     #[inline]
     #[must_use]
     pub fn stmt_parse_result(&self) -> &Arc<StmtParse> {
-        self.stmt_parse.as_ref().expect(
-            "The database has not run `stmt_parse_pass()`. Please ensure it is run before calling depdending methods."
+        self.try_stmt_parse_result().expect(
+            "The database has not run `stmt_parse_pass()`. Please ensure it is run before calling depending methods."
         )
     }
 
@@ -707,9 +793,7 @@ impl Database {
     /// Get a statement by label atom. Requires: [`Database::name_pass`]
     #[must_use]
     pub fn statement_by_label(&self, label: Label) -> Option<StatementRef<'_>> {
-        let token = self.name_result().atom_name(label);
-        let lookup = self.name_result().lookup_label(token)?;
-        Some(self.statement_by_address(lookup.address))
+        self.statement(self.name_result().atom_name(label))
     }
 
     /// Get a statement by address. **Panics** if the statement does not exist.
@@ -768,13 +852,19 @@ impl Database {
             .flat_map(move |seg| seg.range_address(&self.segments.order, (start2, end2)))
     }
 
-    /// Compare the database position of two labels. Proofs can only reference earlier theorems.
+    /// Compare the database position of two label atoms. Proofs can only reference earlier theorems.
     #[must_use]
-    pub fn cmp(&self, left: &Label, right: &Label) -> Option<std::cmp::Ordering> {
+    pub fn cmp_label(&self, left: &Label, right: &Label) -> Option<std::cmp::Ordering> {
         let token_left = self.name_result().atom_name(*left);
         let token_right = self.name_result().atom_name(*right);
-        let lookup_left = self.name_result().lookup_label(token_left)?;
-        let lookup_right = self.name_result().lookup_label(token_right)?;
+        self.cmp(token_left, token_right)
+    }
+
+    /// Compare the database position of two labels. Proofs can only reference earlier theorems.
+    #[must_use]
+    pub fn cmp(&self, left: &[u8], right: &[u8]) -> Option<std::cmp::Ordering> {
+        let lookup_left = self.name_result().lookup_label(left)?;
+        let lookup_right = self.name_result().lookup_label(right)?;
         Some(
             self.parse_result()
                 .order
@@ -782,6 +872,16 @@ impl Database {
         )
     }
 
+    /// Compare the database position of two addresses. Proofs can only reference earlier theorems.
+    #[must_use]
+    pub fn cmp_address(
+        &self,
+        left: &StatementAddress,
+        right: &StatementAddress,
+    ) -> std::cmp::Ordering {
+        self.parse_result().order.cmp(left, right)
+    }
+
     /// Returns the typecode for a given label.
     #[must_use]
     pub fn label_typecode(&self, label: Label) -> TypeCode {
@@ -842,16 +942,16 @@ impl Database {
 
     /// Dump the grammar of this database.
     /// Requires: [`Database::name_pass`], [`Database::grammar_pass`]
-    pub fn print_grammar(&self) {
-        time(&self.options, "print_grammar", || {
+    pub fn dump_grammar(&self) {
+        time(&self.options, "dump_grammar", || {
             self.grammar_result().dump(self);
         })
     }
 
     /// Dump the formulas of this database.
     /// Requires: [`Database::name_pass`], [`Database::stmt_parse_pass`]
-    pub fn print_formula(&self) {
-        time(&self.options, "print_formulas", || {
+    pub fn dump_formula(&self) {
+        time(&self.options, "dump_formulas", || {
             self.stmt_parse_result().dump(self);
         })
     }
@@ -894,34 +994,28 @@ impl Database {
 
     /// Collects and returns all errors generated by the passes run.
     ///
-    /// Passes are identified by the `types` argument and are not inclusive; if
-    /// you ask for Verify, you will not get Parse unless you specifically ask
-    /// for that as well.
-    ///
     /// Currently there is no way to incrementally fetch diagnostics, so this
     /// will be a bit slow if there are thousands of errors.
-    pub fn diag_notations(
-        &mut self,
-        types: &[DiagnosticClass],
-    ) -> Vec<(StatementAddress, Diagnostic)> {
-        let mut diags = Vec::new();
-        if types.contains(&DiagnosticClass::Parse) {
-            diags.extend(self.parse_result().parse_diagnostics());
+    #[must_use]
+    pub fn diag_notations(&self) -> Vec<(StatementAddress, Diagnostic)> {
+        let mut diags = self.parse_result().parse_diagnostics();
+        if let Some(pass) = self.try_scope_result() {
+            diags.extend(pass.diagnostics())
         }
-        if types.contains(&DiagnosticClass::Scope) {
-            diags.extend(self.scope_pass().diagnostics());
+        if let Some(pass) = self.try_verify_result() {
+            diags.extend(pass.diagnostics())
         }
-        if types.contains(&DiagnosticClass::Verify) {
-            diags.extend(self.verify_pass().diagnostics());
+        if let Some(pass) = self.try_usage_result() {
+            diags.extend_from_slice(&pass.diagnostics())
         }
-        if types.contains(&DiagnosticClass::Grammar) {
-            diags.extend(self.grammar_pass().diagnostics());
+        if let Some(pass) = self.try_grammar_result() {
+            diags.extend(pass.diagnostics())
         }
-        if types.contains(&DiagnosticClass::StmtParse) {
-            diags.extend(self.stmt_parse_pass().diagnostics());
+        if let Some(pass) = self.try_stmt_parse_result() {
+            diags.extend(pass.diagnostics())
         }
-        if types.contains(&DiagnosticClass::Typesetting) {
-            diags.extend(self.typesetting_pass().diagnostics.iter().cloned());
+        if let Some(pass) = self.try_typesetting_result() {
+            diags.extend_from_slice(&pass.diagnostics)
         }
         diags
     }
@@ -930,7 +1024,7 @@ impl Database {
     pub fn render_diags<T>(
         &self,
         diags: Vec<(StatementAddress, Diagnostic)>,
-        f: impl for<'a> FnOnce(Snippet<'a>) -> T + Copy,
+        f: impl for<'a> FnOnce(Message<'a>) -> T + Copy,
     ) -> Vec<T> {
         let mut lc = LineCache::default();
         time(&self.options.clone(), "diag", move || {
diff --git a/src/diag.rs b/metamath-rs/src/diag.rs
similarity index 83%
rename from src/diag.rs
rename to metamath-rs/src/diag.rs
index f6d2e04..7bab1e1 100644
--- a/src/diag.rs
+++ b/metamath-rs/src/diag.rs
@@ -20,35 +20,15 @@ use crate::statement::NO_STATEMENT;
 use crate::Span;
 use crate::StatementRef;
 use crate::StatementType;
-use annotate_snippets::display_list::FormatOptions;
-use annotate_snippets::snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation};
+use annotate_snippets::{Level, Message, Snippet};
 use itertools::Itertools;
 use std::borrow::Borrow;
 use std::borrow::Cow;
+use std::error::Error;
+use std::fmt::Display;
 use std::io;
 use typed_arena::Arena;
 
-/// List of passes that generate diagnostics, for use with the
-/// `Database::diag_notations` filter.
-#[derive(Copy, Clone, Eq, PartialEq, Debug)]
-pub enum DiagnosticClass {
-    /// Parse errors, which can be observed from a single statement in
-    /// isolation.
-    Parse,
-    /// Scope errors are mostly inter-statement consistency checks which
-    /// invalidate the logical interpretation of a statement.
-    Scope,
-    /// Verify errors do not invalidate the interpretation of statements, but
-    /// affect only proofs.
-    Verify,
-    /// Grammar errors reflect whether the database is unambiguous
-    Grammar,
-    /// Statement Parsing result
-    StmtParse,
-    /// $t statement parsing result
-    Typesetting,
-}
-
 /// The three kinds of markup supported by `$t` typesetting comments.
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub enum MarkupKind {
@@ -148,6 +128,7 @@ pub enum Diagnostic {
     GrammarAmbiguous(StatementAddress),
     GrammarCantBuild(&'static str),
     GrammarProvableFloat,
+    HtmlParseError(Span, Vec<Cow<'static, str>>),
     HeaderCommentParseError(HeadingLevel),
     InvalidAxiomRestatement(Span, Span),
     IoError(String),
@@ -217,6 +198,7 @@ pub enum Diagnostic {
     UnknownKeyword(Span),
     UnknownTypesettingCommand(Span),
     UnmatchedCloseGroup,
+    UsageViolation(Span, Token, Token),
     VariableMissingFloat(TokenIndex),
     VariableRedeclaredAsConstant(TokenIndex, TokenAddress),
     WindowsReservedLabel(Span),
@@ -235,7 +217,7 @@ pub(crate) fn to_annotations<T>(
     sset: &SegmentSet,
     lc: &mut LineCache,
     mut diags: Vec<(StatementAddress, Diagnostic)>,
-    f: impl for<'a> FnOnce(Snippet<'a>) -> T + Copy,
+    f: impl for<'a> FnOnce(Message<'a>) -> T + Copy,
 ) -> Vec<T> {
     diags.sort_by(|x, y| sset.order.cmp(&x.0, &y.0));
     diags
@@ -250,14 +232,14 @@ pub(crate) fn to_annotations<T>(
 /// Annotation info
 ///
 /// * `label` - A global error message for the diagnostic
-/// For each annotation:
-/// * `label` - The diagnostic message
-/// * `annotation_type` -  Severity level of the message
-/// * `span` - The location of the error (byte offset within the segment; _this is
-/// not the same as the byte offset in the file_).
+/// * For each annotation:
+///   * `label` - The diagnostic message
+///   * `annotation_type` -  Severity level of the message
+///   * `span` - The location of the error (byte offset within the segment;
+///     _this is not the same as the byte offset in the file_).
 type AnnInfo<'a> = (
     Cow<'a, str>,
-    Vec<(AnnotationType, Cow<'a, str>, StatementRef<'a>, Span)>,
+    Vec<(Level, Cow<'a, str>, StatementRef<'a>, Span)>,
 );
 
 /// Creates a `Snippet` containing a diagnostic annotation.
@@ -270,51 +252,37 @@ type AnnInfo<'a> = (
 #[must_use]
 fn make_snippet_from<'b, T>(
     label: &str,
-    infos: impl Iterator<Item = (AnnotationType, Cow<'b, str>, Span, &'b SourceInfo)>,
+    infos: impl Iterator<Item = (Level, Cow<'b, str>, Span, &'b SourceInfo)>,
     footer: &[&str],
     lc: &mut LineCache,
-    f: impl for<'a> FnOnce(Snippet<'a>) -> T,
+    f: impl for<'a> FnOnce(Message<'a>) -> T,
 ) -> T {
-    let mut slices = vec![];
+    let mut snippets = vec![];
     let arena: Arena<String> = Arena::new();
-    for (annotation_type, label, span, source) in infos {
+    let mut level = None;
+    for (level2, label, span, source) in infos {
+        level.get_or_insert(level2);
         let offs = (span.start + source.span.start) as usize;
         let (line_start, col) = lc.from_offset(&source.text, offs);
         let end_offs = (span.end + source.span.start) as usize;
         let source_start = offs + 1 - col as usize;
         let source_end = LineCache::line_end(&source.text, end_offs);
-        slices.push(Slice {
-            source: as_str(&source.text[source_start..source_end]),
-            line_start: line_start as usize,
-            origin: Some(source.name.as_str()),
-            annotations: vec![SourceAnnotation {
-                label: arena.alloc(label.to_string()),
-                annotation_type,
-                range: (offs - source_start, end_offs - source_start),
-            }],
-            fold: true,
-        });
+        let annotation = level2
+            .span(offs - source_start..end_offs - source_start)
+            .label(arena.alloc(label.to_string()));
+        let snippet = Snippet::source(as_str(&source.text[source_start..source_end]))
+            .line_start(line_start as usize)
+            .origin(source.name.as_str())
+            .fold(true)
+            .annotation(annotation);
+        snippets.push(snippet);
     }
-    f(Snippet {
-        title: Some(Annotation {
-            label: Some(label),
-            id: None,
-            annotation_type: slices[0].annotations[0].annotation_type,
-        }),
-        footer: footer
-            .iter()
-            .map(|msg| Annotation {
-                id: None,
-                label: Some(msg),
-                annotation_type: AnnotationType::Note,
-            })
-            .collect(),
-        slices,
-        opt: FormatOptions {
-            color: true,
-            ..FormatOptions::default()
-        },
-    })
+
+    f(level
+        .unwrap()
+        .title(label)
+        .snippets(snippets)
+        .footers(footer.iter().map(|msg| Level::Note.title(msg))))
 }
 
 /// Creates a `Snippet` containing a diagnostic annotation.
@@ -331,7 +299,7 @@ fn make_snippet<T>(
     (label, infos): AnnInfo<'_>,
     footer: &[&str],
     lc: &mut LineCache,
-    f: impl for<'a> FnOnce(Snippet<'a>) -> T,
+    f: impl for<'a> FnOnce(Message<'a>) -> T,
 ) -> T {
     let iter = (infos.into_iter()).map(|(annotation_type, label, stmt, span)| {
         let source = sset.source_info(stmt.segment().id).borrow();
@@ -346,7 +314,7 @@ impl Diagnostic {
         sset: &SegmentSet,
         stmt: StatementRef<'_>,
         lc: &mut LineCache,
-        f: impl for<'a> FnOnce(Snippet<'a>) -> T,
+        f: impl for<'a> FnOnce(Message<'a>) -> T,
     ) -> T {
         fn t(v: &Token) -> String {
             as_str(v).to_owned()
@@ -354,43 +322,43 @@ impl Diagnostic {
         let mut notes: &[&str] = &[];
         let infos = match self {
             BadCharacter(pos, byte) => ("Invalid character".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 format!("Invalid character (byte value {byte}); Metamath source files are limited to \
                         US-ASCII with controls TAB, CR, LF, FF)").into(),
                 stmt,
                 Span::new(*pos, *pos + 1),
             )]),
             BadCommand(span) => ("Invalid command".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Commands must start with a keyword".into(),
                 stmt,
                 *span,
             )]),
             BadCommentEnd(tok, opener) => ("Bad comment end".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "$) sequence must be surrounded by whitespace to end a comment".into(),
                 stmt,
                 *tok,
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Comment started here".into(),
                 stmt,
                 *opener,
             )]),
             BadExplicitLabel(ref tok) => ("Bad explicit label".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 format!("Explicit label {label} does not refer to a hypothesis of the parent step", label = t(tok)).into(),
                 stmt,
                 stmt.span(),
             )]),
             BadFloating => ("Bad floating".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "A $f statement must have exactly two math tokens".into(),
                 stmt,
                 stmt.span(),
             )]),
             BadLabel(lbl) => ("Bad label".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Statement labels may contain only alphanumeric characters and - _ .".into(),
                 stmt,
                 *lbl,
@@ -399,72 +367,72 @@ impl Diagnostic {
                 notes = &["Avoid uses of escape characters in bibliography tags \
                     since they break regex-based implementations"];
                 ("Invalid escape character".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "Use of ~ or ` in a bibliography tag".into(),
                     stmt,
                     Span::new2(index, index + 1),
                 ), (
-                    AnnotationType::Note,
+                    Level::Note,
                     "computed bibliography span".into(),
                     stmt,
                     span,
                 )])
             }
             ChainBackref(span) => ("Chain backref".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Backreference steps are not permitted to have local labels".into(),
                 stmt,
                 *span,
             )]),
             CommandExpectedAs(span) => ("Expected 'as'".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Expected the keyword 'as' here".into(),
                 stmt,
                 *span,
             )]),
             CommandExpectedString(span) => ("Expected string, got keyword argument".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Expected a string here".into(),
                 stmt,
                 *span,
             )]),
             CommandIncomplete(span) => ("Incomplete command".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "This command ended early, it was expecting more arguments".into(),
                 stmt,
                 *span,
             )]),
             CommentMarkerNotStart(marker) => ("Wrong comment marker".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "This comment marker must be the first token in the comment to be effective".into(),
                 stmt,
                 *marker,
             )]),
             ConstantNotTopLevel => ("Constant is not at top level".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "$c statements are not allowed in nested groups".into(),
                 stmt,
                 stmt.span(),
             )]),
             DisjointSingle => ("Disjoint statement with single variable".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "A $d statement which lists only one variable is meaningless".into(),
                 stmt,
                 stmt.span(),
             )]),
             DjNotVariable(index) => ("Disjoint constraints are not applicable to constants".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "$d constraints are not applicable to constants".into(),
                 stmt,
                 stmt.math_span(*index),
             )]),
             DjRepeatedVariable(index1, index2) => ("Variable repeated in disjoint statement".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "A variable may not be used twice in the same $d constraint".into(),
                 stmt,
                 stmt.math_span(*index1),
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Previous appearance was here".into(),
                 stmt,
                 stmt.math_span(*index2),
@@ -472,25 +440,25 @@ impl Diagnostic {
             &DateOrderError(contrib, later) => {
                 notes = &["It is easiest to read the contribution comments when they come in order"];
                 (format!("at {}: Parentheticals should come in chronological order", as_str(stmt.label())).into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "this date...".into(),
                     stmt,
                     contrib,
                 ), (
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "comes after this one".into(),
                     stmt,
                     later,
                 )])
             }
             &DateParseError(span) => ("Failed to parse date".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Expected DD-MMM-YYYY format".into(),
                 stmt,
                 span,
             )]),
             &DefaultAuthor(span) => ("Use of default author".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "There should be a person's name here".into(),
                 stmt,
                 span,
@@ -499,53 +467,53 @@ impl Diagnostic {
                 notes = &["The 'Contributed by' field indicates the first author of a theorem.\n\
                     Use 'Revised by' for subsequent contributions to the same theorem."];
                 ("Statement has multiple contributors".into(), vec![(
-                    AnnotationType::Note,
+                    Level::Note,
                     "First contributor here".into(),
                     stmt,
                     fst,
                 ), (
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "Second contributor here".into(),
                     stmt,
                     snd,
                 )])
             },
             DuplicateExplicitLabel(ref tok) => ("Duplicate explicit label".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 format!("Explicit label {label} is used twice in the same step", label = t(tok)).into(),
                 stmt,
                 stmt.span(),
             )]),
             DuplicateLabel(prevstmt) => ("Duplicate label".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Statement labels must be unique".into(),
                 stmt,
                 stmt.span(),
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Label was previously used here".into(),
                 sset.statement(*prevstmt),
                 sset.statement(*prevstmt).span(),
             )]),
             &DuplicateMarkupDef(kind, fst, snd) => (format!("Duplicate {}", kind.def_name()).into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "This token has already been defined".into(),
                 stmt,
                 snd,
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Token was previously defined here".into(),
                 sset.statement_or_dummy(StatementAddress::new(fst.0, NO_STATEMENT)),
                 fst.1,
             )]),
             EmptyFilename => ("Empty filename".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Filename included by a $[ directive must not be empty".into(),
                 stmt,
                 stmt.span(),
             )]),
             EmptyMathString => ("Empty math string".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "A math string must have at least one token".into(),
                 stmt,
                 stmt.span(),
@@ -555,112 +523,118 @@ impl Diagnostic {
                     was used at the end of a comment,",
                     "or before <HTML>, a math string, or a bibliography tag"];
                 ("Empty label reference".into(), vec![(
-                    AnnotationType::Error,
+                    Level::Error,
                     "This references nothing".into(),
                     stmt,
                     Span::new2(index, index + 1),
                 )])
             },
             EssentialAtTopLevel => ("Essential at top level".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "$e statements must be inside scope brackets, not at the top level".into(),
                 stmt,
                 stmt.span(),
             )]),
             ExprNotConstantPrefix(index) => ("Expression does not have a constant prefix".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "The math string of an $a, $e, or $p assertion must start with a constant, \
                         not a variable".into(),
                 stmt,
                 stmt.math_span(*index),
             )]),
             FilenameDollar => ("Dollar in filename".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Filenames included by $[ are not allowed to contain the $ character".into(),
                 stmt,
                 stmt.span(),
             )]),
             FilenameSpaces => ("Spaces in filename".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Filenames included by $[ are not allowed to contain whitespace".into(),
                 stmt,
                 stmt.span(),
             )]),
             FloatNotConstant(index) => ("Typecode was not declared".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "The first token of a $f statement must be a declared constant (typecode)".into(),
                 stmt,
                 stmt.math_span(*index),
             )]),
             FloatNotVariable(index) => ("Variable not declared".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "The second token of a $f statement must be a declared variable (to \
                         associate the type)".into(),
                 stmt,
                 stmt.math_span(*index),
             )]),
             FloatRedeclared(saddr) => ("Float redeclared".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "There is already an active $f for this variable".into(),
                 stmt,
                 stmt.span(),
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Previous $f was here".into(),
                 sset.statement(*saddr),
                 sset.statement(*saddr).span(),
             )]),
             FormulaVerificationFailed => ("Formula verification failed".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Formula verification failed at this symbol".into(),
                 stmt,
                 stmt.span(),
             )]),
             GrammarAmbiguous(prevstmt) => ("Grammar ambiguous".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Grammar is ambiguous; ".into(),
                 stmt,
                 stmt.span(),
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Collision with this statement:".into(),
                 sset.statement(*prevstmt),
                 sset.statement(*prevstmt).span(),
             )]),
             GrammarCantBuild(message) => ("Can't build the grammar".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 (*message).into(),
                 stmt,
                 stmt.span(),
             )]),
             GrammarProvableFloat => ("Floating declaration of provable type".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Floating declaration of provable type".into(),
                 stmt,
                 stmt.span(),
             )]),
+            HtmlParseError(span, msg) => (format!("HTML parse error(s): {}", msg.iter().format(", ")).into(), vec![(
+                Level::Warning,
+                "in this HTML block".into(),
+                stmt,
+                *span,
+            )]),
             HeaderCommentParseError(lvl) => {
                 notes = lvl.diagnostic_note();
                 ("Invalid header comment".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "Could not parse this as a header".into(),
                     stmt,
                     stmt.span(),
                 )])
             },
             InvalidAxiomRestatement(ax_span, th_span) => ("Invalid axiom restatement".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "This ax* theorem does not match the corresponding ax-*".into(),
                 stmt,
                 *th_span,
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Axiom ax-* here".into(),
                 stmt,
                 *ax_span,
             )]),
             IoError(ref err) => (format!("I/O error: {error}", error = err.clone()).into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Source file could not be read".into(),
                 stmt,
                 stmt.span(),
@@ -668,32 +642,32 @@ impl Diagnostic {
             LabelContainsUnderscore(span) => {
                 notes = &["Prefer '-' over '_' in labels"];
                 ("Label contains underscore".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "this statement has an underscore".into(),
                     stmt,
                     *span,
                 )])
             },
             LineLengthExceeded(span) => ("Line is too long".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "These characters go over the line limit".into(),
                 stmt,
                 *span,
             )]),
             LocalLabelAmbiguous(span) => ("Local label is ambiguous".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Local label conflicts with the name of an existing statement".into(),
                 stmt,
                 *span,
             )]),
             LocalLabelDuplicate(span) => ("Duplicate local Label".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Local label duplicates another label in the same proof".into(),
                 stmt,
                 *span,
             )]),
             &MarkupNeedsWhitespace(index) => ("Markup character requires surrounding whitespace".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Put spaces around this character".into(),
                 stmt,
                 Span::new2(index, index + 1),
@@ -707,84 +681,84 @@ impl Diagnostic {
                     if that_name.is_empty() { "defined in a different mathbox".into() }
                     else { format!("defined in {}'s mathbox", as_str(that_name)).into() };
                 ("Mathbox uses a theorem from another mathbox".into(), vec![
-                    (AnnotationType::Warning, ann1, stmt, this),
-                    (AnnotationType::Note, "it refers to a theorem here...".into(), stmt, span),
-                    (AnnotationType::Note, ann2, stmt, that)
+                    (Level::Warning, ann1, stmt, this),
+                    (Level::Note, "it refers to a theorem here...".into(), stmt, span),
+                    (Level::Note, ann2, stmt, that)
                 ])
             }
             MathboxHeaderFormat(span) => ("Malformed mathbox header".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Expected 'Mathbox for <name>'".into(),
                 stmt,
                 *span,
             )]),
             MalformedAdditionalInfo(span) => ("Malformed additional info".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Malformed additional information".into(),
                 stmt,
                 *span,
             )]),
             MidStatementCommentMarker(marker) => ("Mid-statement comment".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Marked comments are only effective between statements, not inside them".into(),
                 stmt,
                 *marker,
             )]),
-            MissingContributor => ("No contribution comment".into(), vec![(
-                AnnotationType::Warning,
+            MissingContributor => ("Missing or malformed contribution comment".into(), vec![(
+                Level::Warning,
                 "No (Contributed by...) provided for this statement".into(),
                 stmt,
                 stmt.label_span(),
             )]),
             MissingLabel => ("Missing label".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "This statement type requires a label".into(),
                 stmt,
                 stmt.span(),
             )]),
             &MissingMarkupDef([html, alt_html, latex], span) => {
                 let msg = html.then_some("htmldef").into_iter()
-                    .chain(alt_html.then_some("althtmldef").into_iter())
-                    .chain(latex.then_some("latexdef").into_iter());
+                    .chain(alt_html.then_some("althtmldef"))
+                    .chain(latex.then_some("latexdef"));
                 (format!("Missing {} for token", msg.format(", ")).into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "This token has not been declared in the $t comment".into(),
                     stmt,
                     span,
                 )])
             },
             MissingProof(math_end) => ("Missing proof".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Provable assertion requires a proof introduced with $= here; use $= ? $. \
                         if you do not have a proof yet".into(),
                 stmt,
                 *math_end,
             )]),
             MMReservedLabel(span) => ("Reserved label".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Labels beginning with 'mm' are reserved for Metamath file names".into(),
                 stmt,
                 *span,
             )]),
             NestedComment(tok, opener) => ("Nested comment".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Nested comments are not supported - comment will end at the first $)".into(),
                 stmt,
                 *tok,
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Comment started here".into(),
                 stmt,
                 *opener,
             )]),
             NotActiveSymbol(index) => ("Inactive symbol".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Token used here must be active in the current scope".into(),
                 stmt,
                 stmt.math_span(*index),
             )]),
             NotAProvableStatement => ("Not a provable statement".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Statement does not start with the provable constant type".into(),
                 stmt,
                 stmt.span(),
@@ -792,7 +766,7 @@ impl Diagnostic {
             OldAltNotDiscouraged if stmt.statement_type() == StatementType::Axiom => {
                 notes = &["Add (New usage is discouraged.) to the comment"];
                 ("OLD/ALT axiom not discouraged".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "OLD and ALT axioms should be discouraged".into(),
                     stmt,
                     stmt.label_span(),
@@ -802,7 +776,7 @@ impl Diagnostic {
                 notes = &["Add (Proof modification is discouraged.) \
                     and (New usage is discouraged.) to the comment"];
                 ("OLD/ALT theorem not discouraged".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "OLD and ALT theorems should be discouraged".into(),
                     stmt,
                     stmt.label_span(),
@@ -811,43 +785,43 @@ impl Diagnostic {
             &ParenOrderError(contrib, later) => {
                 notes = &["The contribution comment should come before any revisions"];
                 ("(Revised by...) precedes (Contributed by...)".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "contribution comment here".into(),
                     stmt,
                     contrib,
                 ), (
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "earlier revision comment".into(),
                     stmt,
                     later,
                 )])
             }
             ProofDvViolation => ("Distinct variable violation".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Disjoint variable constraint violated".into(),
                 stmt,
                 stmt.span(),
             )]),
             ProofExcessEnd => ("Proof does not end with a single statement".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Must be exactly one statement on stack at end of proof".into(),
                 stmt,
                 stmt.span(),
             )]),
             ProofIncomplete => ("Proof incomplete".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Proof is incomplete".into(),
                 stmt,
                 stmt.span(),
             )]),
             ProofInvalidSave => ("Invalid save".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Z must appear immediately after a complete step integer".into(),
                 stmt,
                 stmt.span(),
             )]),
             ProofMalformedVarint => ("Proof too long".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Proof step number too long or missing terminator".into(),
                 stmt,
                 stmt.span(),
@@ -856,49 +830,49 @@ impl Diagnostic {
                 notes = &["it doesn't make sense to put this marker on an axiom,\n\
                     because axioms don't have proofs"];
                 ("Axiom contains (Proof modification is discouraged.)".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "This doesn't make sense".into(),
                     stmt,
                     span,
                 )])
             },
             ProofNoSteps => ("Empty proof".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Proof must have at least one step (use ? if deliberately incomplete)".into(),
                 stmt,
                 stmt.span(),
             )]),
             ProofUnderflow => ("Proof underflow".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Too few statements on stack to satisfy step's mandatory hypotheses".into(),
                 stmt,
                 stmt.span(),
             )]),
             ProofUnterminatedRoster => ("Unterminated roster".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "List of referenced assertions in a compressed proof must be terminated by )".into(),
                 stmt,
                 stmt.span(),
             )]),
             ProofWrongExprEnd => ("Proven statement does not match assertion".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Final step statement does not match assertion".into(),
                 stmt,
                 stmt.span(),
             )]),
             ProofWrongTypeEnd => ("Proven statement has wrong typecode".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Final step typecode does not match assertion".into(),
                 stmt,
                 stmt.span(),
             )]),
             RepeatedLabel(l_span, f_span) => ("Repeated label".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "A statement may have only one label".into(),
                 stmt,
                 *l_span,
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "First label was here".into(),
                 stmt,
                 *f_span,
@@ -907,7 +881,7 @@ impl Diagnostic {
                 notes = &["The '@' character is discouraged in tokens because it is\n\
                     traditionally used to replace '$' in commented out database source code."];
                 ("Token contains '@'".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "Used '@' character here".into(),
                     stmt,
                     *span,
@@ -917,204 +891,204 @@ impl Diagnostic {
                 notes = &["The '?' character is discouraged in tokens because it is\n\
                     sometimes used as a math token search wildcard."];
                 ("Token contains '?'".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "Used '?' character here".into(),
                     stmt,
                     *span,
                 )])
             }
             SpuriousLabel(lspan) => ("Spurious label".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Labels are only permitted for statements of type $a, $e, $f, or $p".into(),
                 stmt,
                 *lspan,
             )]),
             SpuriousProof(math_end) => ("Spurious proof".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Proofs are only allowed on $p assertions".into(),
                 stmt,
                 *math_end,
             )]),
             StepEssenWrong => ("Wrong essential statement".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Step used for $e hypothesis does not match statement".into(),
                 stmt,
                 stmt.span(),
             )]),
             StepEssenWrongType => ("Wrong essential typecode".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Step used for $e hypothesis does not match typecode".into(),
                 stmt,
                 stmt.span(),
             )]),
             StepFloatWrongType => ("Wrong floating typecode".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Step used for $f hypothesis does not match typecode".into(),
                 stmt,
                 stmt.span(),
             )]),
             StepMissing(ref tok) => ("Missing step".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 format!("Step {step} referenced by proof does not correspond to a $p statement (or \
                         is malformed)", step = t(tok)).into(),
                 stmt,
                 stmt.span(),
             )]),
             StepOutOfRange => ("Step out of range".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Step in compressed proof is out of range of defined steps".into(),
                 stmt,
                 stmt.span(),
             )]),
             StepUsedAfterScope(ref tok) => ("Step used after scope".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 format!("Step {step} referenced by proof is a hypothesis not active in this scope", step = t(tok)).into(),
                 stmt,
                 stmt.span(),
             )]),
             StepUsedBeforeDefinition(ref tok) => ("Step used before definition".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 format!("Step {step} referenced by proof has not yet been proved", step = t(tok)).into(),
                 stmt,
                 stmt.span(),
             )]),
             StmtParseError(err) => err.build_info(stmt),
             SymbolDuplicatesLabel(index, saddr) => ("Symbol duplicates label".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Metamath spec forbids symbols which are the same as labels in the same \
                         database".into(),
                 stmt,
                 stmt.math_span(*index),
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Symbol was used as a label here".into(),
                 sset.statement(*saddr),
                 sset.statement(*saddr).span(),
             )]),
             SymbolRedeclared(index, taddr) => ("Symbol redeclared".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "This symbol is already active in this scope".into(),
                 stmt,
                 stmt.math_span(*index),
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Symbol was previously declared here".into(),
                 stmt,
                 sset.statement(taddr.statement).math_span(taddr.token_index),
             )]),
             TabUsed(span) => ("Tab character used".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Use spaces instead".into(),
                 stmt,
                 *span,
             )]),
             TrailingWhitespace(span) => ("Trailing whitespace".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "whitespace here".into(),
                 stmt,
                 *span,
             )]),
             UnclosedBeforeEof => ("Unclosed before eof".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "${ group must be closed with a $} before end of file".into(),
                 stmt,
                 stmt.span(),
             )]),
             UnclosedBeforeInclude(index) => ("Include not at top level".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "${ group must be closed with a $} before another file can be included".into(),
                 stmt,
                 stmt.span(),
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Include statement is here".into(),
                 stmt.segment().statement(*index),
                 stmt.segment().statement(*index).span(),
             )]),
             UnclosedCommandComment(span) => ("Unclosed comment".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "$t/$j comment requires closing */ before end of statement".into(),
                 stmt,
                 *span,
             )]),
             UnclosedCommandString(span) => ("Unclosed string".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "A string must be closed with ' or \"".into(),
                 stmt,
                 *span,
             )]),
             UnclosedComment(comment) => ("Unclosed comment".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Comment requires closing $) before end of file".into(),
                 stmt,
                 *comment,
             )]),
             &UnclosedHtml(start, end) => ("Unclosed <HTML>".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "HTML blocks must be closed".into(),
                 stmt,
                 Span::new2(end, end + 2), // the $)
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "HTML block started here".into(),
                 stmt,
                 Span::new2(start, start + 6), // the <HTML>
             )]),
             UnclosedInclude => ("Unclosed include".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "$[ requires a matching $]".into(),
                 stmt,
                 stmt.span(),
             )]),
             UnclosedMath => ("Unclosed math".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "A math string must be closed with $= or $.".into(),
                 stmt,
                 stmt.span(),
             )]),
             &UnclosedMathMarkup(start, end) => ("Unclosed math".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "A math string must be closed with `".into(),
                 stmt,
                 Span::new2(end, end + 2), // the $)
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Math string started here".into(),
                 stmt,
                 Span::new2(start, start + 1), // the `
             )]),
             UnclosedProof => ("Unclosed proof".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "A proof must be closed with $.".into(),
                 stmt,
                 stmt.span(),
             )]),
             UnconventionalAxiomLabel(span) => ("Unconventional axiom label".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "Axioms should start with 'ax-' or 'df-'".into(),
                 stmt,
                 *span,
             )]),
             UndefinedBibTag(span) => ("Missing bibliography tag".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "This tag was not found in the bibliography file".into(),
                 stmt,
                 *span,
             )]),
             UndefinedToken(span, tk) => (format!("Undeclared token '{}'", as_str(tk)).into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "This token was not declared in any $v or $c statement".into(),
                 stmt,
                 *span,
             )]),
             UnknownKeyword(kwspan) => ("Unknown keyword".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Statement-starting keyword must be one of $a $c $d $e $f $p $v".into(),
                 stmt,
                 *kwspan,
             )]),
             UnknownTypesettingCommand(kwspan) => ("Unknown $t command".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Typesetting command must be one of:\n\
                 latexdef, htmldef, althtmldef, htmlvarcolor, htmltitle, htmlhome,\n\
                 exthtmltitle, exthtmlhome, exthtmllabel, htmldir, althtmldir,\n\
@@ -1126,46 +1100,53 @@ impl Diagnostic {
                 notes = &[
                     "This character has special meaning in this position, \
                     but it was not interpretable here.",
-                    "Use ~~ or [[ or `` if you mean to include the character literally"
+                    // Zero width space, see #136
+                    "Use ~~ or [[ or `` or _\u{200B}_ if you mean to include the character literally"
                 ];
                 ("Invalid escape character".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "This escape character should be doubled".into(),
                     stmt,
                     Span::new2(index, index + 1),
                 )])
             }
             UninterpretedHtml(tok) => ("incorrect use of <HTML>".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "This <HTML> was not interpreted".into(),
                 stmt,
                 *tok,
             )]),
             UnknownLabel(span) => ("Unknown label".into(), vec![(
-                AnnotationType::Warning,
+                Level::Warning,
                 "This is not the label of any statement".into(),
                 stmt,
                 *span,
             )]),
             UnmatchedCloseGroup => ("Unmatched close group".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "This $} does not match any open ${".into(),
                 stmt,
                 stmt.span(),
             )]),
+            UsageViolation(span, label, axiom) => ("Usage violation".into(), vec![(
+                Level::Warning,
+                format!("Statement {label} uses axiom {axiom} despite $j declaring it avoids its usage.", label=as_str(label), axiom=as_str(axiom)).into(),
+                stmt,
+                *span,
+            )]),
             VariableMissingFloat(index) => ("Variable missing float".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Variable token used in statement must have an active $f".into(),
                 stmt,
                 stmt.math_span(*index),
             )]),
             VariableRedeclaredAsConstant(index, taddr) => ("Variable redeclared as a constant".into(), vec![(
-                AnnotationType::Error,
+                Level::Error,
                 "Symbol cannot be used as a variable here and as a constant later".into(),
                 stmt,
                 stmt.math_span(*index),
             ), (
-                AnnotationType::Note,
+                Level::Note,
                 "Symbol will be used as a constant here".into(),
                 sset.statement(taddr.statement),
                 sset.statement(taddr.statement).math_span(taddr.token_index),
@@ -1174,7 +1155,7 @@ impl Diagnostic {
                 notes = &["On windows, it is not legal to name a file any of:\n\
                     CON, PRN, AUX, CLOCK$, NUL, COM[1-9], LPT[1-9]."];
                 ("Windows reserved label".into(), vec![(
-                    AnnotationType::Warning,
+                    Level::Warning,
                     "This label cannot be used as the name of a file on windows".into(),
                     stmt,
                     *span,
@@ -1216,8 +1197,8 @@ impl StmtParseError {
     /// The diagnostic's severity
     #[must_use]
     #[allow(clippy::unused_self)]
-    pub const fn severity(&self) -> AnnotationType {
-        AnnotationType::Error
+    pub const fn severity(&self) -> Level {
+        Level::Error
     }
 
     fn build_info<'a>(&self, stmt: StatementRef<'a>) -> AnnInfo<'a> {
@@ -1263,12 +1244,9 @@ impl StmtParseError {
                 stmt,
                 *span,
             ),
-            StmtParseError::ParsedStatementNoTypeCode => (
-                AnnotationType::Error,
-                "Empty statement".into(),
-                stmt,
-                stmt.span(),
-            ),
+            StmtParseError::ParsedStatementNoTypeCode => {
+                (Level::Error, "Empty statement".into(), stmt, stmt.span())
+            }
         };
         (self.label(), vec![info])
     }
@@ -1280,6 +1258,18 @@ impl From<StmtParseError> for Diagnostic {
     }
 }
 
+impl Display for StmtParseError {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        f.write_str(&self.label())
+    }
+}
+
+impl Error for StmtParseError {
+    fn source(&self) -> Option<&(dyn Error + 'static)> {
+        None
+    }
+}
+
 /// An error during bibliography parsing.
 #[derive(Debug, Clone, Copy)]
 #[allow(missing_docs)]
@@ -1293,18 +1283,18 @@ impl BibError {
         &self,
         source: &SourceInfo,
         lc: &mut LineCache,
-        f: impl for<'a> FnOnce(Snippet<'a>) -> T,
+        f: impl for<'a> FnOnce(Message<'a>) -> T,
     ) -> T {
         let (label, infos): (Cow<'_, str>, Vec<_>) = match self {
             &BibError::DuplicateBib(span, other) => (
                 "duplicate bibliography anchor".into(),
                 vec![
                     (
-                        AnnotationType::Warning,
+                        Level::Warning,
                         "this anchor has already appeared".into(),
                         span,
                     ),
-                    (AnnotationType::Note, "previous occurrence".into(), other),
+                    (Level::Note, "previous occurrence".into(), other),
                 ],
             ),
         };
@@ -1316,7 +1306,7 @@ impl BibError {
     /// Convert a list of diagnostics collected by `diag_notations` to a list of snippets.
     pub fn render_list<T>(
         diags: &[(&SourceInfo, BibError)],
-        f: impl for<'a> FnOnce(Snippet<'a>) -> T + Copy,
+        f: impl for<'a> FnOnce(Message<'a>) -> T + Copy,
     ) -> Vec<T> {
         let mut lc = LineCache::default();
         diags
diff --git a/src/discouraged.rs b/metamath-rs/src/discouraged.rs
similarity index 100%
rename from src/discouraged.rs
rename to metamath-rs/src/discouraged.rs
diff --git a/src/export.rs b/metamath-rs/src/export.rs
similarity index 96%
rename from src/export.rs
rename to metamath-rs/src/export.rs
index 32b64fd..53cbb34 100644
--- a/src/export.rs
+++ b/metamath-rs/src/export.rs
@@ -14,6 +14,7 @@ use std::fmt;
 use std::io;
 use std::io::Write;
 use std::str;
+use std::sync::OnceLock;
 
 /// The error type for [`Database::export_mmp`].
 #[derive(Debug)]
@@ -77,13 +78,13 @@ impl Database {
             as_str(thm_label)
         )?;
         if let Some(comment) = stmt.associated_comment() {
-            lazy_static::lazy_static! {
-                static ref LEADING_WHITESPACE: Regex = Regex::new(r"\n +").unwrap();
-            }
+            static LEADING_WHITESPACE: OnceLock<Regex> = OnceLock::new();
+            let leading_whitespace =
+                LEADING_WHITESPACE.get_or_init(|| Regex::new(r"\n +").unwrap());
             let mut span = comment.span();
             span.start += 2;
             span.end -= 3;
-            let cstr = LEADING_WHITESPACE.replace_all(
+            let cstr = leading_whitespace.replace_all(
                 as_str(span.as_ref(&comment.segment().segment.buffer)),
                 "\n  ",
             );
diff --git a/metamath-rs/src/export_deps.rs b/metamath-rs/src/export_deps.rs
new file mode 100644
index 0000000..0ff66a8
--- /dev/null
+++ b/metamath-rs/src/export_deps.rs
@@ -0,0 +1,62 @@
+//! Generation of a `GraphML` file containing all theorem dependencies.
+
+use crate::StatementType;
+use crate::{as_str, database::time, Database};
+use xml::writer::{EmitterConfig, XmlEvent};
+
+use crate::diag::Diagnostic;
+
+impl From<xml::writer::Error> for Diagnostic {
+    fn from(err: xml::writer::Error) -> Diagnostic {
+        Diagnostic::IoError(format!("{err}"))
+    }
+}
+
+impl Database {
+    /// Writes down all dependencies in a `GraphML` file format to the given writer.
+    pub fn export_graphml_deps(&mut self, out: &mut impl std::io::Write) -> Result<(), Diagnostic> {
+        self.name_pass();
+        time(&self.options.clone(), "export_graphml_deps", || {
+            let mut writer = EmitterConfig::new().perform_indent(true).create_writer(out);
+            writer.write(
+                XmlEvent::start_element("graphml")
+                    .attr("xmlns", "http://graphml.graphdrawing.org/xmlns")
+                    .attr("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance")
+                    .attr(
+                        "xsi:schemaLocation",
+                        "http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd",
+                    ),
+            )?;
+            writer.write(XmlEvent::start_element("graph").attr("id", "dependencies"))?;
+            for sref in self.statements().filter(|stmt| stmt.is_assertion()) {
+                let label = sref.label();
+                writer.write(XmlEvent::start_element("node").attr("id", as_str(label)))?;
+                writer.write(XmlEvent::end_element())?; // node
+                if sref.statement_type() == StatementType::Provable {
+                    let mut i = 1;
+                    loop {
+                        let tk = sref.proof_slice_at(i);
+                        i += 1;
+                        if tk == b")" {
+                            break;
+                        }
+                        let sref = self
+                            .statement(tk)
+                            .ok_or_else(|| Diagnostic::UnknownLabel(sref.proof_span(i)))?;
+                        if sref.statement_type() == StatementType::Provable {
+                            writer.write(
+                                XmlEvent::start_element("edge")
+                                    .attr("source", as_str(label))
+                                    .attr("target", as_str(tk)),
+                            )?;
+                            writer.write(XmlEvent::end_element())?;
+                        }
+                    }
+                }
+            }
+            writer.write(XmlEvent::end_element())?; // graph
+            writer.write(XmlEvent::end_element())?; // graphml
+            Ok(())
+        })
+    }
+}
diff --git a/src/formula.rs b/metamath-rs/src/formula.rs
similarity index 95%
rename from src/formula.rs
rename to metamath-rs/src/formula.rs
index fcbcc17..1d37ff4 100644
--- a/src/formula.rs
+++ b/metamath-rs/src/formula.rs
@@ -25,6 +25,10 @@ use crate::scopeck::Hyp;
 use crate::segment_set::SegmentSet;
 use crate::statement::SymbolType;
 use crate::statement::TokenIter;
+use crate::tree::NodeId;
+use crate::tree::NodeIter;
+use crate::tree::SiblingIter;
+use crate::tree::Tree;
 use crate::util::fast_extend;
 use crate::util::HashMap;
 use crate::verify::ProofBuilder;
@@ -33,14 +37,9 @@ use core::ops::Index;
 use std::collections::hash_map::Iter;
 use std::fmt::Debug;
 use std::fmt::Display;
-use std::iter::FromIterator;
 use std::ops::Range;
 use std::sync::Arc;
 
-pub use crate::tree::NodeId;
-pub use crate::tree::SiblingIter;
-pub use crate::tree::Tree;
-
 /// An atom representing a typecode (for "set.mm", that's one of 'wff', 'class', 'setvar' or '|-')
 pub type TypeCode = Atom;
 
@@ -199,6 +198,13 @@ impl Formula {
         }
     }
 
+    #[inline]
+    /// Iterates through the labels of a formula, depth-first, post-order.
+    #[must_use]
+    pub fn labels_postorder_iter(&self) -> LabelPostorderIter<'_> {
+        LabelPostorderIter(self.tree.node_iter())
+    }
+
     /// Augment a formula with a database reference, to produce a [`FormulaRef`].
     /// The resulting object implements [`Display`], [`Debug`], and [`IntoIterator`].
     #[must_use]
@@ -415,7 +421,7 @@ impl PartialEq for Formula {
 }
 
 /// An iterator through the labels of a formula.
-/// This iterator sequence is depth-first, postfix (post-order).
+/// This iterator sequence is depth-first, pre-order.
 /// It provides the label, and a boolean indicating whether the current label is a variable or not.
 #[derive(Debug)]
 pub struct LabelIter<'a> {
@@ -454,6 +460,29 @@ impl<'a> Iterator for LabelIter<'a> {
     }
 }
 
+/// An iterator through the labels of a formula.
+/// This iterator sequence is depth-first, post-order.
+/// It provides the label, and a boolean indicating whether the current label is a variable or not.
+#[derive(Debug)]
+pub struct LabelPostorderIter<'a>(NodeIter<'a, Label>);
+
+impl Iterator for LabelPostorderIter<'_> {
+    type Item = Label;
+    fn next(&mut self) -> Option<Self::Item> {
+        self.0.next().copied()
+    }
+
+    fn size_hint(&self) -> (usize, Option<usize>) {
+        self.0.size_hint()
+    }
+}
+
+impl ExactSizeIterator for LabelPostorderIter<'_> {
+    fn len(&self) -> usize {
+        self.0.len()
+    }
+}
+
 /// A [`Formula`] reference in the context of a [`Database`].
 /// This allows the values in the [`Formula`] to be resolved,
 #[derive(Copy, Clone)]
@@ -549,7 +578,7 @@ impl<'a> FormulaRef<'a> {
     ) -> Result<(), E> {
         if self.is_variable(node_id) {
             let label = &self.tree[node_id];
-            if substitutions.0.get(label).is_none() {
+            if !substitutions.0.contains_key(label) {
                 let typecode = self.db.label_typecode(*label);
                 let work_var = wvp.new_work_variable(typecode)?;
                 substitutions.insert(*label, Formula::from_float(work_var, typecode));
@@ -765,6 +794,17 @@ pub(crate) struct FormulaBuilder {
 
 /// A utility to build a formula.
 impl FormulaBuilder {
+    pub(crate) fn from_formula(fmla: Formula) -> Self {
+        let stack = vec![fmla.root];
+        let tree = (*fmla.tree).clone();
+        let variables = fmla.variables;
+        FormulaBuilder {
+            stack,
+            variables,
+            tree,
+        }
+    }
+
     /// Every REDUCE pops `var_count` subformula items on the stack,
     /// and pushes one single new item, with the popped subformulas as children
     pub(crate) fn reduce(&mut self, label: Label, var_count: u8, offset: u8, is_variable: bool) {
diff --git a/src/formula_tests.rs b/metamath-rs/src/formula_tests.rs
similarity index 100%
rename from src/formula_tests.rs
rename to metamath-rs/src/formula_tests.rs
diff --git a/src/grammar.rs b/metamath-rs/src/grammar.rs
similarity index 87%
rename from src/grammar.rs
rename to metamath-rs/src/grammar.rs
index 359369c..4af171f 100644
--- a/src/grammar.rs
+++ b/metamath-rs/src/grammar.rs
@@ -109,7 +109,7 @@ impl GrammarTree {
                     map: ref mut to_map,
                 },
             ) => {
-                for (&(stype, symbol), next_node) in map.iter() {
+                for (&(stype, symbol), next_node) in map {
                     match to_map.entry((stype, symbol)) {
                         Entry::Occupied(_) => {
                             // Skip error here, do nothing for now...
@@ -139,7 +139,7 @@ impl GrammarTree {
 ///
 /// Example:
 /// ```
-/// use metamath_knife::database::{Database, DbOptions};
+/// use metamath_rs::database::{Database, DbOptions};
 ///
 /// // Setup the required options
 /// let mut options = DbOptions::default();
@@ -170,7 +170,7 @@ pub struct Grammar {
 /// - `label` is the syntax axiom being applied.
 /// - `var_count` is the number of variables this syntax axiom requires. This tells how many of the parse trees will be joined.
 /// - `offset` says how far in the stack of yet un-joined parse trees the reduce will join. The cases when this is non-zero are rare.
-#[derive(Clone, Copy, Debug, Default, PartialEq)]
+#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
 struct Reduce {
     label: Label,
     var_count: u8,
@@ -420,13 +420,16 @@ impl Grammar {
                     [Keyword(cmd), sort, Keyword(as_), logic]
                         if cmd.as_ref(buf) == b"syntax" && as_.as_ref(buf) == b"as" =>
                     {
-                        self.provable_type = nset.lookup_symbol(sort.value(buf)).unwrap().atom;
-                        self.logic_type = nset.lookup_symbol(logic.value(buf)).unwrap().atom;
+                        self.provable_type = nset.lookup_symbol(&sort.value(buf)).unwrap().atom;
+                        self.logic_type = nset.lookup_symbol(&logic.value(buf)).unwrap().atom;
                         self.typecodes.push(self.logic_type);
                     }
-                    [Keyword(cmd), sort] if cmd.as_ref(buf) == b"syntax" => self
-                        .typecodes
-                        .push(nset.lookup_symbol(sort.value(buf)).unwrap().atom),
+                    [Keyword(cmd), rest @ ..] if cmd.as_ref(buf) == b"syntax" => {
+                        for sort in rest {
+                            self.typecodes
+                                .push(nset.lookup_symbol(&sort.value(buf)).unwrap().atom)
+                        }
+                    }
                     _ => {}
                 }
             }
@@ -517,31 +520,24 @@ impl Grammar {
         stype: SymbolType,
         add_reduce: ReduceVec,
     ) -> Result<NodeId, NodeId> {
-        match self.nodes.get_mut(to_node) {
-            GrammarNode::Leaf { .. } => {
-                Err(to_node) // Error: cannot add to a leaf node, `to_node` is the conflicting node
-            }
-            GrammarNode::Branch { map } => {
-                match map.get(&(stype, symbol)) {
-                    Some(prev_node) if prev_node.leaf_label == add_reduce => {
-                        Ok(prev_node.next_node_id)
-                    }
-                    Some(prev_node) => Err(prev_node.next_node_id),
-                    None => {
-                        let new_node_id = self.nodes.create_branch();
-                        // here we have to re-borrow from self after the creation,
-                        // because the previous var_map and cst_map may not be valid pointers anymore
-                        if let GrammarNode::Branch { map } = self.nodes.get_mut(to_node) {
-                            map.insert(
-                                (stype, symbol),
-                                NextNode::new_with_reduce_vec(new_node_id, add_reduce),
-                            );
-                            Ok(new_node_id)
-                        } else {
-                            panic!("Shall not happen!");
-                        }
-                    }
-                }
+        let GrammarNode::Branch { map } = self.nodes.get_mut(to_node) else {
+            return Err(to_node); // Error: cannot add to a leaf node, `to_node` is the conflicting node
+        };
+        match map.get(&(stype, symbol)) {
+            Some(prev_node) if prev_node.leaf_label == add_reduce => Ok(prev_node.next_node_id),
+            Some(prev_node) => Err(prev_node.next_node_id),
+            None => {
+                let new_node_id = self.nodes.create_branch();
+                // here we have to re-borrow from self after the creation,
+                // because the previous var_map and cst_map may not be valid pointers anymore
+                let GrammarNode::Branch { map } = self.nodes.get_mut(to_node) else {
+                    unreachable!();
+                };
+                map.insert(
+                    (stype, symbol),
+                    NextNode::new_with_reduce_vec(new_node_id, add_reduce),
+                );
+                Ok(new_node_id)
             }
         }
     }
@@ -574,14 +570,11 @@ impl Grammar {
                 .lookup_symbol(token_ptr)
                 .ok_or_else(|| Diagnostic::UndefinedToken(sref.math_span(1), token_ptr.into()))?;
             if symbol.stype == SymbolType::Variable {
-                let from_typecode = match names.lookup_float(token_ptr) {
-                    Some(lookup_float) => lookup_float.typecode_atom,
-                    _ => {
-                        return Err(Diagnostic::VariableMissingFloat(1));
-                    }
+                let Some(lookup_float) = names.lookup_float(token_ptr) else {
+                    return Err(Diagnostic::VariableMissingFloat(1));
                 };
                 self.type_conversions
-                    .push((from_typecode, this_typecode, this_label));
+                    .push((lookup_float.typecode_atom, this_typecode, this_label));
                 return Ok(()); // we don't need to add the type conversion axiom itself to the grammar (or do we?)
             }
         }
@@ -605,14 +598,13 @@ impl Grammar {
                         .typecode_atom
                 }
             };
-            match match &tokens.peek() {
-                Some(_) => self.add_branch_with_reduce(node, atom, symbol.stype, ReduceVec::new()),
-                None => {
-                    let leaf_node_id = self
-                        .nodes
-                        .create_leaf(Reduce::new(this_label, var_count), this_typecode);
-                    self.add_branch(node, atom, symbol.stype, &NextNode::new(leaf_node_id))
-                }
+            match if tokens.peek().is_some() {
+                self.add_branch_with_reduce(node, atom, symbol.stype, ReduceVec::new())
+            } else {
+                let leaf_node_id = self
+                    .nodes
+                    .create_leaf(Reduce::new(this_label, var_count), this_typecode);
+                self.add_branch(node, atom, symbol.stype, &NextNode::new(leaf_node_id))
             } {
                 Ok(next_node) => {
                     node = next_node;
@@ -662,21 +654,19 @@ impl Grammar {
             as_str(nset.statement_name(sref))
         );
 
-        match self.nodes.get_mut(self.root) {
-            // We ignore the ambiguity in floats, since they are actually frame dependent.
-            GrammarNode::Branch { map } => {
-                map.insert(
-                    (SymbolType::Constant, symbol.atom),
-                    NextNode::new(leaf_node),
-                );
-                Ok(())
-                // match cst_map.insert(symbol.atom, NextNode::new(leaf_node)) {
-                //     None => Ok(()),
-                //     Some(_) => Err(self.ambiguous(conflict_node.next_node_id, nset)),
-                // }
-            }
-            GrammarNode::Leaf { .. } => panic!("Root node shall be a branch node!"),
-        }
+        let GrammarNode::Branch { map } = self.nodes.get_mut(self.root) else {
+            unreachable!("Root node must be a branch node!")
+        };
+        // We ignore the ambiguity in floats, since they are actually frame dependent.
+        map.insert(
+            (SymbolType::Constant, symbol.atom),
+            NextNode::new(leaf_node),
+        );
+        Ok(())
+        // match cst_map.insert(symbol.atom, NextNode::new(leaf_node)) {
+        //     None => Ok(()),
+        //     Some(_) => Err(self.ambiguous(conflict_node.next_node_id, nset)),
+        // }
     }
 
     /// Handle type conversion:
@@ -737,16 +727,14 @@ impl Grammar {
     }
 
     fn next_var_node(&self, node_id: NodeId, typecode: TypeCode) -> Option<(NodeId, &ReduceVec)> {
-        match self.nodes.get(node_id) {
-            GrammarNode::Branch { map } => match map.get(&(SymbolType::Variable, typecode)) {
-                Some(NextNode {
-                    next_node_id,
-                    leaf_label,
-                }) => Some((*next_node_id, leaf_label)),
-                _ => None,
-            },
-            GrammarNode::Leaf { .. } => None,
-        }
+        let GrammarNode::Branch { map } = self.nodes.get(node_id) else {
+            return None;
+        };
+        let NextNode {
+            next_node_id,
+            leaf_label,
+        } = map.get(&(SymbolType::Variable, typecode))?;
+        Some((*next_node_id, leaf_label))
     }
 
     /// Recursively clone the whole grammar tree starting from `add_from_node_id`
@@ -789,7 +777,7 @@ impl Grammar {
                     typecode,
                 } = *self.nodes.get(next_node.next_node_id)
                 {
-                    let mut reduce_vec = ReduceVec::new();
+                    let mut reduce_vec = next_node.leaf_label;
                     for reduce in stored_reduces {
                         reduce_vec.push(reduce);
                     }
@@ -959,7 +947,7 @@ impl Grammar {
             if let GrammarNode::Branch { map } = self.nodes.get(node_id) {
                 let prefix_symbol = db
                     .name_result()
-                    .lookup_symbol(prefix[index].value(buf))
+                    .lookup_symbol(&prefix[index].value(buf))
                     .ok_or_else(|| undefined_cmd(&prefix[index], buf))?
                     .atom;
                 let next_node = map
@@ -976,7 +964,7 @@ impl Grammar {
 
         // We note the typecode and next branch of the "shadowed" prefix
         let shadowed_typecode = names
-            .lookup_float(shadows[index].value(buf))
+            .lookup_float(&shadows[index].value(buf))
             .ok_or_else(|| undefined_cmd(&shadows[index], buf))?
             .typecode_atom;
         let (shadowed_next_node, _) =
@@ -992,11 +980,11 @@ impl Grammar {
         let mut missing_reduce = ReduceVec::new();
         for token in &prefix[index..] {
             let lookup_symbol = names
-                .lookup_symbol(token.value(buf))
+                .lookup_symbol(&token.value(buf))
                 .ok_or_else(|| undefined_cmd(token, buf))?;
             debug!(
                 "Following prefix {}, at {} / {}",
-                as_str(token.value(buf)),
+                as_str(&token.value(buf)),
                 node_id,
                 add_from_node_id
             );
@@ -1006,7 +994,7 @@ impl Grammar {
                 SymbolType::Variable => {
                     increment_offsets(&mut missing_reduce);
                     names
-                        .lookup_float(token.value(buf))
+                        .lookup_float(&token.value(buf))
                         .ok_or_else(|| undefined_cmd(token, buf))?
                         .typecode_atom
                 }
@@ -1034,7 +1022,7 @@ impl Grammar {
             }
         }
 
-        debug!("Shadowed token: {}", as_str(shadows[index].value(buf)));
+        debug!("Shadowed token: {}", as_str(&shadows[index].value(buf)));
         debug!("Missing reduces: {}", missing_reduce.len());
         debug!(
             "Handle shadowed next node {}, typecode {:?}",
@@ -1096,77 +1084,74 @@ impl Grammar {
             for &(ix, (span, ref command)) in &sref.j_commands {
                 use CommandToken::*;
                 let address = StatementAddress::new(sref.id, ix);
-                if let (Keyword(k), rest) = command
-                    .split_first()
-                    .ok_or((address, Diagnostic::BadCommand(span)))?
-                {
-                    // Empty parser command
-                    match k.as_ref(buf) {
-                        b"syntax" => match rest {
-                            [ty, Keyword(as_), code] if as_.as_ref(buf) == b"as" => {
-                                // syntax '|-' as 'wff';
-                                self.provable_type = nset
-                                    .lookup_symbol(ty.value(buf))
-                                    .ok_or((address, undefined_cmd(ty, buf)))?
-                                    .atom;
-                                self.typecodes.push(
-                                    nset.lookup_symbol(code.value(buf))
-                                        .ok_or((address, undefined_cmd(code, buf)))?
-                                        .atom,
-                                );
-                            }
-                            [ty] => {
+                let [Keyword(k), ref rest @ ..] = **command else {
+                    return Err((address, Diagnostic::BadCommand(span)));
+                };
+                // Empty parser command
+                match k.as_ref(buf) {
+                    b"syntax" => match rest {
+                        [ty, Keyword(as_), code] if as_.as_ref(buf) == b"as" => {
+                            // syntax '|-' as 'wff';
+                            self.provable_type = nset
+                                .lookup_symbol(&ty.value(buf))
+                                .ok_or((address, undefined_cmd(ty, buf)))?
+                                .atom;
+                            self.typecodes.push(
+                                nset.lookup_symbol(&code.value(buf))
+                                    .ok_or((address, undefined_cmd(code, buf)))?
+                                    .atom,
+                            );
+                        }
+                        _ => {
+                            for ty in rest {
                                 // syntax 'setvar';
                                 self.typecodes.push(
-                                    nset.lookup_symbol(ty.value(buf))
+                                    nset.lookup_symbol(&ty.value(buf))
                                         .ok_or((address, undefined_cmd(ty, buf)))?
                                         .atom,
                                 );
                             }
-                            _ => {}
-                        },
-                        // Handle Ambiguous prefix commands
-                        b"garden_path" => {
-                            let split_index = rest
-                                .iter()
-                                .position(|t| matches!(t, Keyword(k) if k.as_ref(buf) == b"=>"))
-                                .ok_or((address, Diagnostic::BadCommand(*k)))?; // '=>' not present in 'garden_path' command
-                            let (prefix, shadows) = rest.split_at(split_index);
-                            if let Err(diag) =
-                                self.handle_common_prefixes(prefix, &shadows[1..], buf, db, names)
-                            {
-                                return Err((address, diag));
-                            }
                         }
-                        // Handle replacement schemes
-                        b"type_conversions" => {
-                            for &(from_typecode, to_typecode, label) in
-                                &self.type_conversions.clone()
-                            {
-                                if let Err(diag) = self.perform_type_conversion(
-                                    from_typecode,
-                                    to_typecode,
-                                    label,
-                                    db,
-                                ) {
-                                    return Err((address, diag));
-                                }
-                            }
+                    },
+                    // Handle Ambiguous prefix commands
+                    b"garden_path" => {
+                        let split_index = rest
+                            .iter()
+                            .position(|t| matches!(t, Keyword(k) if k.as_ref(buf) == b"=>"))
+                            .ok_or((address, Diagnostic::BadCommand(k)))?; // '=>' not present in 'garden_path' command
+                        let (prefix, shadows) = rest.split_at(split_index);
+                        if let Err(diag) =
+                            self.handle_common_prefixes(prefix, &shadows[1..], buf, db, names)
+                        {
+                            return Err((address, diag));
+                        }
+                    }
+                    // Handle replacement schemes
+                    b"type_conversions" => {
+                        for &(from_typecode, to_typecode, label) in &self.type_conversions.clone() {
+                            self.perform_type_conversion(from_typecode, to_typecode, label, db)
+                                .map_err(|diag| (address, diag))?;
                         }
-                        _ => {}
                     }
+                    _ => {}
                 }
             }
         }
         Ok(())
     }
 
-    fn do_shift(&self, symbol_iter: &mut dyn Iterator<Item = FormulaToken>, nset: &Nameset) {
+    fn do_shift(
+        &self,
+        symbol_iter: &mut dyn Iterator<Item = Result<FormulaToken, StmtParseError>>,
+        nset: &Nameset,
+    ) -> Result<(), StmtParseError> {
         if let Some(token) = symbol_iter.next() {
+            let token = token?;
             if self.debug {
                 debug!("   SHIFT {:?}", as_str(nset.atom_name(token.symbol)));
             }
         }
+        Ok(())
     }
 
     fn do_reduce(formula_builder: &mut FormulaBuilder, reduce: Reduce, nset: &Nameset) {
@@ -1189,7 +1174,7 @@ impl Grammar {
     /// Parses the given list of symbols into a formula syntax tree.
     pub fn parse_formula(
         &self,
-        symbol_iter: &mut impl Iterator<Item = FormulaToken>,
+        symbol_iter: &mut impl Iterator<Item = Result<FormulaToken, StmtParseError>>,
         expected_typecodes: &[TypeCode],
         convert_to_provable: bool,
         nset: &Nameset,
@@ -1201,9 +1186,12 @@ impl Grammar {
 
         let mut formula_builder = FormulaBuilder::default();
         let mut symbol_enum = symbol_iter.peekable();
-        let mut last_token = *symbol_enum
+        let Ok(mut last_token) = symbol_enum
             .peek()
-            .ok_or(StmtParseError::ParsedStatementNoTypeCode)?;
+            .ok_or(StmtParseError::ParsedStatementNoTypeCode)?
+        else {
+            return Err(symbol_enum.next().unwrap().unwrap_err());
+        };
         let mut e = StackElement {
             node_id: self.root,
             expected_typecodes: expected_typecodes.to_vec().into_boxed_slice(),
@@ -1292,7 +1280,7 @@ impl Grammar {
                     }
                 }
                 GrammarNode::Branch { ref map } => {
-                    if let Some(&token) = symbol_enum.peek() {
+                    if let Some(&Ok(token)) = symbol_enum.peek() {
                         last_token = token;
                         debug!("   {:?}", as_str(nset.atom_name(token.symbol)));
 
@@ -1307,7 +1295,7 @@ impl Grammar {
                             }
 
                             // Found an atom matching one of our next nodes: SHIFT, to the next node
-                            self.do_shift(&mut symbol_enum, nset);
+                            self.do_shift(&mut symbol_enum, nset)?;
                             e.node_id = *next_node_id;
                             debug!("   Next Node: {:?}", e.node_id);
                         } else {
@@ -1333,6 +1321,9 @@ impl Grammar {
                             };
                         }
                     } else {
+                        if let Some(token) = symbol_enum.next() {
+                            token?;
+                        }
                         return Err(Grammar::too_short(last_token, map, nset));
                     }
                 }
@@ -1401,6 +1392,47 @@ impl Iterator for FormulaTokenIter<'_> {
     }
 }
 
+/// An iterator through the tokens of a math expression
+#[derive(Debug)]
+pub struct StmtTokenIter<'a, 'b> {
+    span: &'a [Span],
+    buffer: &'a [u8],
+    index: usize,
+    names: &'a mut NameReader<'b>,
+}
+
+impl StatementRef<'_> {
+    /// Returns a new iterator over tokens of a math expression.
+    /// `names` caches the result of any name lookups performed.
+    pub fn token_iter<'a, 'b>(&'a self, names: &'a mut NameReader<'b>) -> StmtTokenIter<'a, 'b> {
+        let range = self.statement.math_start..self.statement.proof_start;
+        StmtTokenIter {
+            span: &self.segment.segment.span_pool[range],
+            buffer: &self.segment.segment.buffer,
+            index: 1,
+            names,
+        }
+    }
+}
+
+impl Iterator for StmtTokenIter<'_, '_> {
+    type Item = Result<FormulaToken, StmtParseError>;
+    fn next(&mut self) -> Option<Self::Item> {
+        let span = *self.span.get(self.index)?;
+        self.index += 1;
+        Some(
+            if let Some(lookup) = self.names.lookup_symbol(span.as_ref(self.buffer)) {
+                Ok(FormulaToken {
+                    symbol: lookup.atom,
+                    span,
+                })
+            } else {
+                Err(StmtParseError::UnknownToken(span))
+            },
+        )
+    }
+}
+
 impl Grammar {
     /// Parses a character string into a formula
     /// As a first math token, the string is expected to contain the typecode for the formula.
@@ -1410,12 +1442,10 @@ impl Grammar {
         formula_string: &str,
         nset: &Arc<Nameset>,
     ) -> Result<Formula, StmtParseError> {
-        let mut symbols = FormulaTokenIter::from_str(formula_string, nset)
-            .collect::<Result<Vec<_>, _>>()?
-            .into_iter();
+        let mut symbols = FormulaTokenIter::from_str(formula_string, nset);
         let typecode = symbols
             .next()
-            .ok_or(StmtParseError::ParsedStatementNoTypeCode)?;
+            .ok_or(StmtParseError::ParsedStatementNoTypeCode)??;
         let expected_typecode = if typecode.symbol == self.provable_type {
             self.logic_type
         } else {
@@ -1430,13 +1460,13 @@ impl Grammar {
         )
     }
 
-    /// Parse a statement into a formula. Returns None if the statement is a syntactic axiom.
+    /// Parses an individual statement into a formula.
     pub fn parse_statement(
         &self,
         sref: &StatementRef<'_>,
         nset: &Nameset,
         names: &mut NameReader<'_>,
-    ) -> Result<Option<Formula>, StmtParseError> {
+    ) -> Result<Formula, StmtParseError> {
         if sref.math_len() == 0 {
             return Err(StmtParseError::ParsedStatementNoTypeCode);
         }
@@ -1445,12 +1475,6 @@ impl Grammar {
         let typecode = nset.get_atom(sref.math_at(0).slice);
         let mut expected_typecode = typecode;
 
-        // Skip syntactic axioms
-        if sref.statement_type() == StatementType::Axiom && expected_typecode != self.provable_type
-        {
-            return Ok(None);
-        }
-
         // If this is a provable statement, prove that this is a wff. Otherwise just use the provided typecode
         if expected_typecode == self.provable_type {
             expected_typecode = self.logic_type;
@@ -1462,29 +1486,15 @@ impl Grammar {
             as_str(nset.statement_name(sref))
         );
 
-        let math_string: Result<Vec<_>, _> = sref
-            .math_iter()
-            .skip(1)
-            .map(|token| {
-                let span = sref.math_span(token.index());
-                if let Some(lookup) = names.lookup_symbol(token.slice) {
-                    Ok(FormulaToken {
-                        symbol: lookup.atom,
-                        span,
-                    })
-                } else {
-                    Err(StmtParseError::UnknownToken(span))
-                }
-            })
-            .collect();
+        let mut math_string = sref.token_iter(names);
         let convert_to_provable = typecode == self.provable_type;
         let formula = self.parse_formula(
-            &mut math_string?.into_iter(),
+            &mut math_string,
             &[expected_typecode],
             convert_to_provable,
             nset,
         )?;
-        Ok(Some(formula))
+        Ok(formula)
     }
 
     /// Returns the typecodes allowed in this grammar
@@ -1507,6 +1517,21 @@ impl Grammar {
         self.logic_type
     }
 
+    /// Converts the given formula to the target typecode,
+    /// provided there is a suitable type conversion.
+    #[must_use]
+    pub fn convert_typecode(&self, fmla: Formula, target_tc: TypeCode) -> Option<Formula> {
+        let source_tc = fmla.get_typecode();
+        self.type_conversions
+            .iter()
+            .find(|(from_tc, to_tc, _)| *from_tc == source_tc && *to_tc == target_tc)
+            .map(|(_, _, label)| {
+                let mut builder = FormulaBuilder::from_formula(fmla);
+                builder.reduce(*label, 1, 0, false);
+                builder.build(target_tc)
+            })
+    }
+
     /// Lists the contents of the grammar's parse table. This can be used for debugging.
     pub fn dump(&self, db: &Database) {
         println!("Grammar tree has {:?} nodes.", self.nodes.len());
@@ -1645,7 +1670,7 @@ impl Grammar {
 ///
 /// Example:
 /// ```
-/// use metamath_knife::database::{Database, DbOptions};
+/// use metamath_rs::database::{Database, DbOptions};
 ///
 /// // Setup the required options
 /// let mut options = DbOptions::default();
@@ -1751,21 +1776,19 @@ fn parse_statements_single(
     let mut formulas = HashMap::default();
 
     for sref in segment {
-        match match sref.statement_type() {
-            StatementType::Axiom | StatementType::Essential | StatementType::Provable => {
-                grammar.parse_statement(&sref, nset, names)
-            }
-            _ => Ok(None),
-        } {
-            Err(diag) => {
-                warn!(" FAILED to parse {}!", as_str(nset.statement_name(&sref)));
-                diagnostics.insert(sref.address(), diag);
-                break; // inserted here to stop at first error!
-            }
-            Ok(Some(formula)) => {
-                formulas.insert(sref.address(), formula);
+        if let StatementType::Axiom | StatementType::Essential | StatementType::Provable =
+            sref.statement_type()
+        {
+            match grammar.parse_statement(&sref, nset, names) {
+                Err(diag) => {
+                    warn!(" FAILED to parse {}!", as_str(nset.statement_name(&sref)));
+                    diagnostics.insert(sref.address(), diag);
+                    break; // inserted here to stop at first error!
+                }
+                Ok(formula) => {
+                    formulas.insert(sref.address(), formula);
+                }
             }
-            _ => {}
         }
     }
 
diff --git a/src/grammar_tests.rs b/metamath-rs/src/grammar_tests.rs
similarity index 90%
rename from src/grammar_tests.rs
rename to metamath-rs/src/grammar_tests.rs
index adbbc38..e322ef5 100644
--- a/src/grammar_tests.rs
+++ b/metamath-rs/src/grammar_tests.rs
@@ -113,7 +113,7 @@ fn test_parse_formula() {
     let fmla_vec = vec![a, eq, open_parens, b, plus, a, close_parens];
     let formula = grammar
         .parse_formula(
-            &mut fmla_vec.clone().into_iter(),
+            &mut fmla_vec.iter().map(|t| Ok(*t)),
             &[wff, class],
             false,
             &names,
@@ -213,7 +213,7 @@ fn test_setvar_as_class() {
     {
         let formula = grammar
             .parse_formula(
-                &mut vec![x_symbol].into_iter(),
+                &mut std::iter::once(Ok(x_symbol)),
                 &[class_symbol],
                 false,
                 &names,
@@ -329,6 +329,39 @@ macro_rules! grammar_test {
     };
 }
 
+const ISSUE_135: &[u8] = b"
+    $c = class wff setvar -> ( ) |- + [ ] $.
+    $( $j syntax 'setvar' 'class' 'wff'; syntax '|-' as 'wff'; $)
+    $( $j type_conversions; garden_path ( x => ( ph ; $)
+    $v x A B ph ps $.
+    vx $f setvar x $.
+    wph $f wff ph $.
+    wps $f wff ps $.
+    cA $f class A $.
+    cB $f class B $.
+    cv $a class x $.
+    wn $a wff [ A ] $.
+    wceq $a wff A = B $.
+    wi $a wff ( ph -> ps ) $.
+    cdif $a class ( A + B ) $.
+    ax1 $a |- [ x ] $.
+    ax2 $a |- ( x = x -> ph ) $.
+";
+
+#[test]
+fn test_issue_135() {
+    let mut db = mkdb(ISSUE_135);
+    let stmt_parse = db.stmt_parse_pass().clone();
+    let sref = db.statement(b"ax1").unwrap();
+    let formula = stmt_parse.get_formula(&sref).unwrap();
+    assert_eq!(formula.as_ref(&db).as_sexpr(), "(wn (cv vx))");
+    let sref = db.statement(b"ax2").unwrap();
+    let formula = stmt_parse.get_formula(&sref).unwrap();
+    assert_eq!(
+        formula.as_ref(&db).as_sexpr(),
+        "(wi (wceq (cv vx) (cv vx)) wph)"
+    );
+}
 grammar_test!(
     test_missing_float,
     b"$c setvar $. $v x $. vx $a setvar x $.",
@@ -343,6 +376,7 @@ grammar_test!(
     2,
     Diagnostic::GrammarAmbiguous(sa!(2, 1))
 );
+
 grammar_test!(
     test_float_not_var,
     b"$c setvar $. vx $f setvar x $.",
diff --git a/src/lib.rs b/metamath-rs/src/lib.rs
similarity index 88%
rename from src/lib.rs
rename to metamath-rs/src/lib.rs
index 6737f6e..6952610 100644
--- a/src/lib.rs
+++ b/metamath-rs/src/lib.rs
@@ -14,8 +14,7 @@
     trivial_numeric_casts,
     variant_size_differences,
     unreachable_pub,
-    unused,
-    missing_docs
+    unused
 )]
 // all the clippy
 #![warn(clippy::all, clippy::pedantic, clippy::nursery, clippy::cargo)]
@@ -29,14 +28,16 @@
 )]
 // // all the clippy lints we don't want
 #![allow(
-    clippy::blocks_in_if_conditions,
+    clippy::blocks_in_conditions,
     clippy::cast_sign_loss,
     clippy::cast_possible_wrap,
     clippy::enum_glob_use,
     clippy::if_not_else,
     clippy::inline_always,
+    clippy::let_underscore_untyped,
     clippy::missing_errors_doc,
     clippy::module_name_repetitions,
+    clippy::multiple_crate_versions,
     clippy::needless_range_loop,
     clippy::option_if_let_else,
     clippy::redundant_pub_crate,
@@ -53,9 +54,9 @@
 mod bit_set;
 mod segment;
 mod segment_set;
-mod tree;
 mod util;
 
+pub mod axiom_use;
 pub mod comment_parser;
 pub mod database;
 pub mod diag;
@@ -70,10 +71,16 @@ pub mod parser;
 pub mod proof;
 pub mod scopeck;
 pub mod statement;
+pub mod tree;
 pub mod typesetting;
 pub mod verify;
+
+#[cfg(feature = "verify_markup")]
 pub mod verify_markup;
 
+#[cfg(feature = "xml")]
+pub mod export_deps;
+
 #[cfg(test)]
 mod comment_parser_tests;
 #[cfg(test)]
@@ -83,6 +90,8 @@ mod grammar_tests;
 #[cfg(test)]
 mod parser_tests;
 #[cfg(test)]
+mod usage_tests;
+#[cfg(test)]
 mod util_tests;
 
 pub use database::Database;
@@ -90,6 +99,7 @@ pub use formula::Formula;
 pub use formula::FormulaRef;
 pub use formula::Label;
 pub use formula::Symbol;
+pub use parser::is_valid_label;
 pub use segment::Comparer;
 pub use segment_set::SourceInfo;
 pub use statement::as_str;
diff --git a/src/line_cache.rs b/metamath-rs/src/line_cache.rs
similarity index 99%
rename from src/line_cache.rs
rename to metamath-rs/src/line_cache.rs
index ffda91c..84732f0 100644
--- a/src/line_cache.rs
+++ b/metamath-rs/src/line_cache.rs
@@ -2,7 +2,6 @@
 
 use crate::util::HashMap;
 use std::cmp::Ordering;
-use std::convert::TryFrom;
 
 const PAGE: usize = 256;
 
diff --git a/src/nameck.rs b/metamath-rs/src/nameck.rs
similarity index 99%
rename from src/nameck.rs
rename to metamath-rs/src/nameck.rs
index 66c8ad0..d27c666 100644
--- a/src/nameck.rs
+++ b/metamath-rs/src/nameck.rs
@@ -35,7 +35,6 @@ use crate::StatementRef;
 use std::borrow::Borrow;
 use std::hash::Hash;
 use std::sync::Arc;
-use std::u32;
 
 // An earlier version of this module was tasked with detecting duplicate symbol errors;
 // current task is just lookup
@@ -84,7 +83,7 @@ fn slot_remove<A: Eq, V>(slot: &mut NameSlot<A, V>, address: &A) {
 }
 
 fn autoviv<K: Hash + Eq, V: Default>(map: &mut HashMap<K, V>, key: K) -> &mut V {
-    map.entry(key).or_insert_with(Default::default)
+    map.entry(key).or_default()
 }
 
 fn deviv<K, Q, V, F>(map: &mut HashMap<K, V>, key: &Q, fun: F)
@@ -343,7 +342,7 @@ impl Nameset {
     #[must_use]
     pub fn lookup_label(&self, label: TokenPtr<'_>) -> Option<LookupLabel> {
         self.labels.get(label).and_then(|lslot| {
-            lslot.labels.first().map(|&(addr, _)| LookupLabel {
+            lslot.labels.first().map(|&(addr, ())| LookupLabel {
                 atom: lslot.atom,
                 address: addr,
             })
@@ -358,7 +357,7 @@ impl Nameset {
                 stype,
                 atom: syminfo.atom,
                 address: addr,
-                const_address: syminfo.constant.first().map(|&(addr, _)| addr),
+                const_address: syminfo.constant.first().map(|&(addr, ())| addr),
             })
         })
     }
diff --git a/src/outline.rs b/metamath-rs/src/outline.rs
similarity index 100%
rename from src/outline.rs
rename to metamath-rs/src/outline.rs
diff --git a/src/parser.rs b/metamath-rs/src/parser.rs
similarity index 93%
rename from src/parser.rs
rename to metamath-rs/src/parser.rs
index d169bff..0d1e944 100644
--- a/src/parser.rs
+++ b/metamath-rs/src/parser.rs
@@ -30,7 +30,7 @@ use std::collections::hash_map::Entry;
 use std::fmt::Debug;
 use std::mem;
 use std::str;
-use std::sync::Arc;
+use std::sync::{Arc, OnceLock};
 
 /// State used by the scanning process
 #[derive(Default)]
@@ -681,7 +681,10 @@ fn collect_definitions(seg: &mut Segment) {
                     });
                 }
             }
-            continue;
+            // Skip further treatment if the statement is not at top-level, except for $j commands.
+            if stmt.stype != AdditionalInfoComment {
+                continue;
+            }
         }
 
         let math = &seg.span_pool[stmt.math_start..stmt.proof_start];
@@ -756,7 +759,8 @@ fn collect_definitions(seg: &mut Segment) {
 }
 
 /// Metamath spec valid label characters are `[-._a-zA-Z0-9]`
-fn is_valid_label(label: &[u8]) -> bool {
+#[must_use]
+pub fn is_valid_label(label: &[u8]) -> bool {
     label
         .iter()
         .all(|&c| c == b'.' || c == b'-' || c == b'_' || c.is_ascii_alphanumeric())
@@ -893,7 +897,11 @@ impl Iterator for CommandIter<'_> {
                     let ch = self.next_char();
                     self.index += 1;
                     if ch == quote {
-                        break;
+                        if self.has_more() && self.next_char() == quote {
+                            self.index += 1;
+                        } else {
+                            break;
+                        }
                     }
                 }
                 CommandToken::String(Span::new(token_start, self.index - 1))
@@ -1008,7 +1016,7 @@ impl SegmentSet {
 
             let sum = |mut rest: std::slice::Iter<'_, CommandToken>| {
                 let mut span_out = as_string(span, rest.next())?;
-                let mut accum: Vec<u8> = span_out.as_ref(buf).into();
+                let mut accum: Vec<u8> = CommandToken::unescape_string(buf, span_out).into();
                 span_out.start -= 1;
                 loop {
                     match rest.next() {
@@ -1020,7 +1028,7 @@ impl SegmentSet {
                         _ => return Err(Diagnostic::CommandIncomplete(span)),
                     }
                     let span2 = as_string(span, rest.next())?;
-                    accum.extend_from_slice(span2.as_ref(buf));
+                    CommandToken::append_unescaped_string(buf, span2, &mut accum);
                     span_out.end = span2.end
                 }
             };
@@ -1039,7 +1047,7 @@ impl SegmentSet {
                     MarkupKind::AltHtml => &mut data.alt_html_defs,
                     MarkupKind::Latex => &mut data.latex_defs,
                 };
-                match map.entry(sp.as_ref(buf).into()) {
+                match map.entry(CommandToken::unescape_string(buf, sp).into()) {
                     Entry::Occupied(e) => {
                         let (sp2, (id2, _), _) = *e.get();
                         data.diagnostics
@@ -1085,28 +1093,38 @@ impl SegmentSet {
     }
 }
 
-pub(crate) struct HeadingComment {
-    pub(crate) header: Span,
-    pub(crate) content: Span,
+/// A parsed heading comment.
+#[derive(Debug, Clone, Copy)]
+pub struct HeadingComment {
+    /// The header part of the heading comment (the text of the header)
+    pub header: Span,
+    /// The content part of the heading comment (descriptive text regarding the header)
+    pub content: Span,
 }
 
 impl HeadingComment {
-    pub(crate) fn parse(buf: &[u8], lvl: HeadingLevel, sp: Span) -> Option<Self> {
-        lazy_static::lazy_static! {
-            static ref MAJOR_PART: Regex =
-                Regex::new(r"^[ \n]+#{4,}\n *([^\n]*)\n#{4,}\n").unwrap();
-            static ref SECTION: Regex =
-                Regex::new(r"^[ \n]+(?:#\*){2,}#?\n *([^\n]*)\n(?:#\*){2,}#?\n").unwrap();
-            static ref SUBSECTION: Regex =
-                Regex::new(r"^[ \n]+(?:=-){2,}=?\n *([^\n]*)\n(?:=-){2,}=?\n").unwrap();
-            static ref SUBSUBSECTION: Regex =
-                Regex::new(r"^[ \n]+(?:-\.){2,}-?\n *([^\n]*)\n(?:-\.){2,}-?\n").unwrap();
-        }
+    /// Parses a heading comment at the given span in a segment buffer,
+    /// with the specified heading level and span. Returns `None` if this is not a heading comment
+    /// or it is malformed.
+    #[must_use]
+    pub fn parse(buf: &[u8], lvl: HeadingLevel, sp: Span) -> Option<Self> {
+        static MAJOR_PART: OnceLock<Regex> = OnceLock::new();
+        static SECTION: OnceLock<Regex> = OnceLock::new();
+        static SUBSECTION: OnceLock<Regex> = OnceLock::new();
+        static SUBSUBSECTION: OnceLock<Regex> = OnceLock::new();
         let regex = match lvl {
-            HeadingLevel::MajorPart => &*MAJOR_PART,
-            HeadingLevel::Section => &*SECTION,
-            HeadingLevel::SubSection => &*SUBSECTION,
-            HeadingLevel::SubSubSection => &*SUBSUBSECTION,
+            HeadingLevel::MajorPart => MAJOR_PART.get_or_init(|| {
+                Regex::new(r"^[ \r\n]+#{4,}\r?\n *([^\n]*)\r?\n#{4,}\r?\n").unwrap()
+            }),
+            HeadingLevel::Section => SECTION.get_or_init(|| {
+                Regex::new(r"^[ \r\n]+(?:#\*){2,}#?\r?\n *([^\n]*)\r?\n(?:#\*){2,}#?\r?\n").unwrap()
+            }),
+            HeadingLevel::SubSection => SUBSECTION.get_or_init(|| {
+                Regex::new(r"^[ \r\n]+(?:=-){2,}=?\r?\n *([^\n]*)\r?\n(?:=-){2,}=?\r?\n").unwrap()
+            }),
+            HeadingLevel::SubSubSection => SUBSUBSECTION.get_or_init(|| {
+                Regex::new(r"^[ \r\n]+(?:-\.){2,}-?\r?\n *([^\n]*)\r?\n(?:-\.){2,}-?\r?\n").unwrap()
+            }),
             _ => unreachable!(),
         };
         let groups = regex.captures(sp.as_ref(buf))?;
@@ -1117,11 +1135,12 @@ impl HeadingComment {
         })
     }
 
-    pub(crate) fn parse_mathbox_header(&self, buf: &[u8]) -> Option<Span> {
-        lazy_static::lazy_static! {
-            static ref MATHBOX_FOR: Regex = Regex::new(r"^Mathbox for (.*)$").unwrap();
-        }
-        let m = MATHBOX_FOR.captures(self.header.as_ref(buf))?.get(1)?;
+    /// Parses a mathbox heading comment, returning the span of the author name.
+    #[must_use]
+    pub fn parse_mathbox_header(&self, buf: &[u8]) -> Option<Span> {
+        static MATHBOX_FOR: OnceLock<Regex> = OnceLock::new();
+        let mathbox_for = MATHBOX_FOR.get_or_init(|| Regex::new(r"^Mathbox for (.*)$").unwrap());
+        let m = mathbox_for.captures(self.header.as_ref(buf))?.get(1)?;
         Some(Span::new2(
             self.header.start + m.start() as u32,
             self.header.start + m.end() as u32,
diff --git a/src/parser_tests.rs b/metamath-rs/src/parser_tests.rs
similarity index 100%
rename from src/parser_tests.rs
rename to metamath-rs/src/parser_tests.rs
diff --git a/src/proof.rs b/metamath-rs/src/proof.rs
similarity index 99%
rename from src/proof.rs
rename to metamath-rs/src/proof.rs
index a8fef4a..2543b07 100644
--- a/src/proof.rs
+++ b/metamath-rs/src/proof.rs
@@ -9,13 +9,12 @@ use crate::statement::{StatementAddress, TokenPtr};
 use crate::util::HashMap;
 use crate::verify::ProofBuilder;
 use crate::{Database, StatementRef, StatementType};
-use std::cmp::{max, Ord, Ordering, PartialOrd};
+use std::cmp::{max, Ordering};
 use std::collections::hash_map::{DefaultHasher, Entry};
 use std::collections::{BinaryHeap, VecDeque};
 use std::fmt::{self, Write};
 use std::hash::{Hash, Hasher};
 use std::ops::Range;
-use std::u16;
 
 /// A tree structure for storing proofs and grammar derivations.
 #[derive(Clone, Debug, Eq)]
diff --git a/src/scopeck.rs b/metamath-rs/src/scopeck.rs
similarity index 97%
rename from src/scopeck.rs
rename to metamath-rs/src/scopeck.rs
index f8a19a8..10adb82 100644
--- a/src/scopeck.rs
+++ b/metamath-rs/src/scopeck.rs
@@ -2,23 +2,23 @@
 //! can be done at the same time:
 //!
 //! 1. For `$c $v $f` and labelled statements (`$e $f $a $p`): Check for
-//! duplication
+//!    duplication
 //!
-//! 1. For `$e $d $f $a $p`: Check that all used math symbols are active in
-//! scope
+//! 2. For `$e $d $f $a $p`: Check that all used math symbols are active in
+//!    scope
 //!
-//! 1. For `$a $p`: Compute the frame
+//! 3. For `$a $p`: Compute the frame
 //!
 //! Rules of precedence for error detection and recovery:
 //!
 //! 1. Math symbols and labels are actually in separate namespaces.  We warn
-//! about collisions but otherwise do nothing.  Variables have responsibility
-//! for the warning.
+//!    about collisions but otherwise do nothing.  Variables have responsibility
+//!    for the warning.
 //!
-//! 1. When two definitions have overlapping live ranges, the earlier one wins.
+//! 2. When two definitions have overlapping live ranges, the earlier one wins.
 //!
-//! 1. Constant/nested variable collisions are special because they don't
-//! involve scope overlaps. The constant wins, the variable must notify.
+//! 3. Constant/nested variable collisions are special because they don't
+//!    involve scope overlaps. The constant wins, the variable must notify.
 //!
 //! Since this is always run before the verifier, it focuses on supporting the
 //! verifier; things that the verifier won't use mostly aren't done.  This
@@ -124,6 +124,16 @@ pub struct VerifyExpr {
     pub tail: Box<[ExprFragment]>,
 }
 
+impl VerifyExpr {
+    /// Returns an iterator over runs of constants in the expression,
+    /// as references into the constant pool.
+    pub fn const_ranges(&self) -> impl Iterator<Item = Range<usize>> + '_ {
+        (self.tail.iter().map(|e| &e.prefix))
+            .chain(std::iter::once(&self.rump))
+            .cloned()
+    }
+}
+
 /// Representation of a hypothesis in a frame program.
 #[derive(Clone, Debug)]
 pub enum Hyp {
@@ -270,11 +280,7 @@ struct ScopeState<'a> {
 }
 
 fn push_diagnostic(state: &mut ScopeState<'_>, ix: StatementIndex, diag: Diagnostic) {
-    state
-        .diagnostics
-        .entry(ix)
-        .or_insert_with(Vec::new)
-        .push(diag);
+    state.diagnostics.entry(ix).or_default().push(diag);
 }
 
 /// Verifies that this is the true (first) use of a label.  The returned atom
@@ -731,7 +737,9 @@ fn scope_check_float<'a>(state: &mut ScopeState<'a>, sref: StatementRef<'a>) {
     let const_tok = sref.math_at(0);
     let var_tok = sref.math_at(1);
 
-    let Some(l_atom) = check_label_dup(state, sref) else { return };
+    let Some(l_atom) = check_label_dup(state, sref) else {
+        return;
+    };
 
     // $f must be one constant and one variable - parser can't check this
     let mut const_at = Atom::default();
@@ -773,7 +781,7 @@ fn scope_check_float<'a>(state: &mut ScopeState<'a>, sref: StatementRef<'a>) {
         state
             .local_floats
             .entry((*var_tok).into())
-            .or_insert_with(Vec::new)
+            .or_default()
             .push(LocalFloatInfo {
                 typecode: const_at,
                 valid: sref.scope_range(),
@@ -797,10 +805,7 @@ fn maybe_add_local_var(
     s_ref: StatementRef<'_>,
     t_ref: TokenRef<'_>,
 ) -> Option<TokenAddress> {
-    let lv_slot = state
-        .local_vars
-        .entry((*t_ref).into())
-        .or_insert_with(Vec::new);
+    let lv_slot = state.local_vars.entry((*t_ref).into()).or_default();
 
     if let Some(lv_most_recent) = lv_slot.last() {
         if check_endpoint(s_ref.index(), lv_most_recent.end) {
diff --git a/src/segment.rs b/metamath-rs/src/segment.rs
similarity index 100%
rename from src/segment.rs
rename to metamath-rs/src/segment.rs
diff --git a/src/segment_set.rs b/metamath-rs/src/segment_set.rs
similarity index 97%
rename from src/segment_set.rs
rename to metamath-rs/src/segment_set.rs
index 269c2bc..c148d78 100644
--- a/src/segment_set.rs
+++ b/metamath-rs/src/segment_set.rs
@@ -19,12 +19,13 @@
 //! `segment_set` implements two levels of caching:
 //!
 //! 1. When a file is loaded from disk, its pathname and modification time are
-//! saved, along with all of the segments which it generated.  If the file
-//! hasn't changed at all, we can reuse the segments after a single `stat`.
+//!    saved, along with all of the segments which it generated.  If the file
+//!    hasn't changed at all, we can reuse the segments after a single `stat`.
 //!
-//! 1. After a file is loaded and split, slices are cached by content.  This
-//! speeds up operation when local changes are made to large files, or when
-//! modification times cannot be used (such as some language server scenarios).
+//! 2. After a file is loaded and split, slices are cached by content.  This
+//!    speeds up operation when local changes are made to large files, or when
+//!    modification times cannot be used (such as some language server
+//!    scenarios).
 //!
 //! In either case, some care is needed to retain only data which is relevant in
 //! the cache.  The caches are discarded on every read, but any data obtained
@@ -147,7 +148,7 @@ pub(crate) struct SegmentSet {
     /// The work queue for use with this database.
     pub(crate) exec: Executor,
     /// Order structure which records the relative order of segment IDs created
-    /// by the SegmentSet.
+    /// by the `SegmentSet`.
     pub(crate) order: Arc<SegmentOrder>,
     /// Track segment and source info in parallel so they can be updated
     /// independently in the slicing case and if a file is renamed.
@@ -337,10 +338,7 @@ impl SegmentSet {
         // read a file from disk (intercessions have already been checked, but
         // the first cache has not) and split/parse it;
         // returns by Result Error on I/O error
-        fn canonicalize_and_read(
-            state: &mut RecState,
-            path: String,
-        ) -> io::Result<Promise<FileSR>> {
+        fn canonicalize_and_read(state: &RecState, path: String) -> io::Result<Promise<FileSR>> {
             let metadata = fs::metadata(&path)?;
             let time = FileTime::from_last_modification_time(&metadata);
 
diff --git a/src/statement.rs b/metamath-rs/src/statement.rs
similarity index 91%
rename from src/statement.rs
rename to metamath-rs/src/statement.rs
index 0b87056..ada8e3b 100644
--- a/src/statement.rs
+++ b/metamath-rs/src/statement.rs
@@ -31,11 +31,11 @@
 //! `SegmentId` and `SegmentRef` cover the same use cases for segments, although
 //! it makes no sense to have a segment-local segment reference.
 
-use std::ops::Deref;
+use std::{borrow::Cow, ops::Deref};
 
 use crate::{
     comment_parser::{CommentParser, Discouragements, ParentheticalIter},
-    parser::HeadingLevel,
+    parser::{HeadingComment, HeadingLevel},
     segment::SegmentRef,
 };
 
@@ -201,7 +201,7 @@ pub struct GlobalRange {
     /// Since scope braces are not allowed to span segments, if a range ends at
     /// all it must be in the same segment where it started, so this can be a
     /// bare `StatementIndex`.  If the range extends to the logical end of the
-    /// database, that is represented with the NO_STATEMENT constant.
+    /// database, that is represented with the `NO_STATEMENT` constant.
     ///
     /// Since the endpoint always points at a `CloseGroup` statement (or, in
     /// erroneous cases, `Eof` or `FileInclude`) which has no label nor math
@@ -301,6 +301,26 @@ pub struct HeadingDef {
     pub level: HeadingLevel,
 }
 
+#[inline]
+pub(crate) fn unescape(
+    mut buf: &[u8],
+    out: &mut Vec<u8>,
+    is_escape: impl FnOnce(u8) -> bool + Copy,
+) {
+    while let Some(n) = buf.iter().position(|&c| is_escape(c)) {
+        out.extend_from_slice(&buf[..=n]);
+        if buf.get(n + 1) == Some(&buf[n]) {
+            buf = &buf[n + 2..];
+        } else {
+            // this will not normally happen, but in some cases unescaped escapes
+            // are left uninterpreted because they appear in invalid position,
+            // and in that case they should be left as is
+            buf = &buf[n + 1..];
+        }
+    }
+    out.extend_from_slice(buf);
+}
+
 /// An individual symbol in a command, either a string or other keyword.
 #[derive(Clone, Copy, Debug)]
 pub enum CommandToken {
@@ -313,9 +333,10 @@ pub enum CommandToken {
 impl CommandToken {
     /// Get the string corresponding to this token.
     #[must_use]
-    pub fn value(self, buf: &[u8]) -> TokenPtr<'_> {
+    pub fn value(self, buf: &[u8]) -> Cow<'_, [u8]> {
         match self {
-            Self::Keyword(s) | Self::String(s) => s.as_ref(buf),
+            Self::Keyword(s) => Cow::Borrowed(s.as_ref(buf)),
+            Self::String(s) => Self::unescape_string(buf, s),
         }
     }
 
@@ -327,6 +348,26 @@ impl CommandToken {
             Self::String(s) => Span::new2(s.start - 1, s.end + 1),
         }
     }
+
+    /// Remove doubled quote escapes from a [`CommandToken::String`]`(span)`.
+    pub fn append_unescaped_string(buf: &[u8], span: Span, out: &mut Vec<u8>) {
+        let quote = buf[(span.start - 1) as usize];
+        unescape(span.as_ref(buf), out, |c| quote == c)
+    }
+
+    /// Remove doubled quote escapes from a [`CommandToken::String`]`(span)`.
+    #[must_use]
+    pub fn unescape_string(buf: &[u8], span: Span) -> Cow<'_, [u8]> {
+        let quote = buf[(span.start - 1) as usize];
+        let buf = span.as_ref(buf);
+        if buf.contains(&quote) {
+            let mut out = vec![];
+            unescape(span.as_ref(buf), &mut out, |c| quote == c);
+            out.into()
+        } else {
+            Cow::Borrowed(buf)
+        }
+    }
 }
 
 /// Extra information residing in a $j comment
@@ -427,16 +468,16 @@ pub(crate) struct Statement {
     /// at the beginning of the keyword.
     pub(crate) label: Span,
     /// Start of the most deeply nested group for this statment, or
-    /// NO_STATEMENT.
+    /// `NO_STATEMENT`.
     pub(crate) group: StatementIndex,
-    /// End of the most deeply nested group for this statment, or NO_STATEMENT.
+    /// End of the most deeply nested group for this statment, or `NO_STATEMENT`.
     pub(crate) group_end: StatementIndex,
-    /// Index into span_pool of the first math token.
+    /// Index into `span_pool` of the first math token.
     pub(crate) math_start: usize,
-    /// Index into span_pool of the first proof token / after the last math
+    /// Index into `span_pool` of the first proof token / after the last math
     /// token.
     pub(crate) proof_start: usize,
-    /// Index into span_pool one after the last proof token.
+    /// Index into `span_pool` one after the last proof token.
     pub(crate) proof_end: usize,
 }
 
@@ -611,7 +652,7 @@ impl<'a> StatementRef<'a> {
     pub fn use_iter(&self) -> UseIter<'a> {
         let spans = self.proof_spans();
         let mut iter = spans.iter();
-        if spans.get(0).map(|sp| sp.as_ref(&self.segment.buffer)) == Some(b"(") {
+        if spans.first().map(|sp| sp.as_ref(&self.segment.buffer)) == Some(b"(") {
             iter.next();
         }
         UseIter {
@@ -680,7 +721,16 @@ impl<'a> StatementRef<'a> {
     /// in this comment statement.
     #[must_use]
     pub fn parentheticals(&self) -> ParentheticalIter<'a> {
-        ParentheticalIter::new(&self.segment().segment.buffer, self.comment_contents())
+        ParentheticalIter::new(&self.segment.segment.buffer, self.comment_contents())
+    }
+
+    /// Returns a `HeadingComment` object for a heading comment (if it is actually a heading).
+    #[must_use]
+    pub fn as_heading_comment(&self) -> Option<HeadingComment> {
+        let StatementType::HeadingComment(lvl) = self.statement_type() else {
+            return None;
+        };
+        HeadingComment::parse(&self.segment.buffer, lvl, self.comment_contents())
     }
 }
 
diff --git a/src/tree.rs b/metamath-rs/src/tree.rs
similarity index 87%
rename from src/tree.rs
rename to metamath-rs/src/tree.rs
index 4f5e389..a35dd23 100644
--- a/src/tree.rs
+++ b/metamath-rs/src/tree.rs
@@ -121,6 +121,11 @@ impl<TreeItem> Tree<TreeItem> {
             );
         }
     }
+
+    /// Returns an iterator over all the nodes in the tree (in postorder)
+    pub(crate) fn node_iter(&self) -> NodeIter<'_, TreeItem> {
+        NodeIter(self.nodes.iter())
+    }
 }
 
 impl<TreeItem> Index<NodeId> for Tree<TreeItem> {
@@ -172,3 +177,24 @@ impl<TreeItem> Iterator for SiblingIter<'_, TreeItem> {
         std::mem::replace(&mut self.current_id, self.tree.next_sibling(current_id?))
     }
 }
+
+/// An iterator through all nodes
+#[derive(Debug)]
+pub(crate) struct NodeIter<'a, TreeItem>(std::slice::Iter<'a, TreeNode<TreeItem>>);
+
+impl<'a, TreeItem> Iterator for NodeIter<'a, TreeItem> {
+    type Item = &'a TreeItem;
+    fn next(&mut self) -> Option<Self::Item> {
+        self.0.next().map(|node| &node.item)
+    }
+
+    fn size_hint(&self) -> (usize, Option<usize>) {
+        self.0.size_hint()
+    }
+}
+
+impl<'a, TreeItem> ExactSizeIterator for NodeIter<'a, TreeItem> {
+    fn len(&self) -> usize {
+        self.0.len()
+    }
+}
diff --git a/src/typesetting.rs b/metamath-rs/src/typesetting.rs
similarity index 99%
rename from src/typesetting.rs
rename to metamath-rs/src/typesetting.rs
index 799c106..4e3b7e9 100644
--- a/src/typesetting.rs
+++ b/metamath-rs/src/typesetting.rs
@@ -1,7 +1,7 @@
 //! The typesetting data.
 //!
 //! This is the result of parsing a `$t` metamath comment, which contains information
-//! used by the metamath website generator. Although `metamath-knife` tries to be
+//! used by the metamath website generator. Although `metamath-rs` tries to be
 //! generic and so it does not itself contain a website generator, this pass can be
 //! used to collect information for generating HTML in the style of
 //! [`metamath.exe`](https://github.com/metamath/metamath-exe).
diff --git a/metamath-rs/src/usage_tests.rs b/metamath-rs/src/usage_tests.rs
new file mode 100644
index 0000000..cb53d0e
--- /dev/null
+++ b/metamath-rs/src/usage_tests.rs
@@ -0,0 +1,25 @@
+use crate::diag::Diagnostic::UsageViolation;
+use crate::grammar_tests::mkdb;
+use assert_matches::assert_matches;
+
+const USAGE_DB: &[u8] = b"
+$c wff |- > $.  $v a $.
+wa $f |- a $.
+ax-1 $a |- > a $.
+thm1 $p |- > a $= wa ax-1 $.
+$( $j usage 'thm1' avoids 'ax-1'; $)
+thm2 $p |- > a $= ( ax-1 ) AB $.
+$( $j usage 'thm2' avoids 'ax-1'; $)
+";
+
+#[test]
+fn test_usage() {
+    let mut db = mkdb(USAGE_DB);
+    assert_eq!(db.parse_result().parse_diagnostics(), vec![]);
+    let usage = db.verify_usage_pass();
+    let diags = usage.diagnostics();
+
+    assert_eq!(diags.len(), 2);
+    assert_matches!(diags[0], (_, UsageViolation(..)));
+    assert_matches!(diags[1], (_, UsageViolation(..)));
+}
diff --git a/src/util.rs b/metamath-rs/src/util.rs
similarity index 97%
rename from src/util.rs
rename to metamath-rs/src/util.rs
index b039250..c94c6f5 100644
--- a/src/util.rs
+++ b/metamath-rs/src/util.rs
@@ -33,11 +33,7 @@ pub(crate) fn fast_extend<T: Copy>(vec: &mut Vec<T>, other: &[T]) {
     vec.reserve(other.len());
     unsafe {
         let len = vec.len();
-        short_copy(
-            other.get_unchecked(0),
-            vec.get_unchecked_mut(len),
-            other.len(),
-        );
+        short_copy(other.as_ptr(), vec.as_mut_ptr().add(len), other.len());
         vec.set_len(len + other.len());
     }
 }
diff --git a/src/util_tests.rs b/metamath-rs/src/util_tests.rs
similarity index 97%
rename from src/util_tests.rs
rename to metamath-rs/src/util_tests.rs
index ee6a7ff..8ff9718 100644
--- a/src/util_tests.rs
+++ b/metamath-rs/src/util_tests.rs
@@ -2,6 +2,7 @@ use crate::util;
 use std::sync::Arc;
 
 #[test]
+#[allow(clippy::redundant_clone)]
 fn test_ptr_eq() {
     let a1 = Arc::new("Hello, world".to_string());
     let a2 = a1.clone();
@@ -39,6 +40,7 @@ fn test_copy_portion() {
 
 #[test]
 #[should_panic(expected = "out of range")]
+#[allow(clippy::collection_is_never_read)]
 fn test_copy_portion_oob() {
     let mut s = Vec::from(b"Hello world" as &[u8]);
     s.extend_from_within(11..12);
diff --git a/src/verify.rs b/metamath-rs/src/verify.rs
similarity index 99%
rename from src/verify.rs
rename to metamath-rs/src/verify.rs
index fcca7ae..5db52b7 100644
--- a/src/verify.rs
+++ b/metamath-rs/src/verify.rs
@@ -101,9 +101,9 @@ impl ProofBuilder for () {
     type Item = ();
     type Accum = ();
 
-    fn push(&mut self, _: &mut (), _: ()) {}
+    fn push(&mut self, (): &mut (), (): ()) {}
 
-    fn build(&mut self, _: StatementAddress, _: (), _: &[u8], _: Range<usize>) {}
+    fn build(&mut self, _: StatementAddress, (): (), _: &[u8], _: Range<usize>) {}
 }
 
 /// Working memory used by the verifier on a segment.  This expands for the
diff --git a/src/verify_markup.rs b/metamath-rs/src/verify_markup.rs
similarity index 84%
rename from src/verify_markup.rs
rename to metamath-rs/src/verify_markup.rs
index 73b51df..ac1f374 100644
--- a/src/verify_markup.rs
+++ b/metamath-rs/src/verify_markup.rs
@@ -9,7 +9,9 @@
 //! references, because this is what metamath.exe did. (Ideally, most or all of
 //! these hardcoded references can be replaced by `$j` commands in the future.)
 
-use crate::comment_parser::{is_text_escape, CommentItem, CommentParser, Date, Parenthetical};
+use crate::comment_parser::{
+    is_label_escape, is_text_escape, CommentItem, CommentParser, Date, Parenthetical,
+};
 use crate::diag::{BibError, Diagnostic};
 use crate::parser::{HeadingComment, HeadingLevel};
 use crate::scopeck::Hyp;
@@ -18,12 +20,15 @@ use crate::segment_set::SourceInfo;
 use crate::statement::{StatementAddress, NO_STATEMENT};
 use crate::util::{HashMap, HashSet};
 use crate::{Database, Span, StatementRef, StatementType};
+use html5ever::tendril::{stream::Utf8LossyDecoder, Tendril, TendrilSink as _};
 use regex::bytes::Regex;
 use std::ops::Range;
+use std::sync::OnceLock;
 
-lazy_static::lazy_static! {
-    static ref WINDOWS_RESERVED_NAMES: Regex =
-        Regex::new("(?i-u)^(?:CON|PRN|AUX|NUL|(?:COM|LPT)[1-9])$").unwrap();
+fn windows_reserved_names() -> &'static Regex {
+    static WINDOWS_RESERVED_NAMES: OnceLock<Regex> = OnceLock::new();
+    WINDOWS_RESERVED_NAMES
+        .get_or_init(|| Regex::new("(?i-u)^(?:CON|PRN|AUX|NUL|(?:COM|LPT)[1-9])$").unwrap())
 }
 
 impl Database {
@@ -67,7 +72,7 @@ impl Database {
                     stmt.address(),
                     Diagnostic::MMReservedLabel(stmt.label_span()),
                 ))
-            } else if WINDOWS_RESERVED_NAMES.is_match(stmt.label()) {
+            } else if windows_reserved_names().is_match(stmt.label()) {
                 diags.push((
                     stmt.address(),
                     Diagnostic::WindowsReservedLabel(stmt.label_span()),
@@ -284,6 +289,15 @@ impl Database {
                         eol_check(&mut diags, &seg, line_start, i);
                         line_start = i + 1;
                     }
+                    b'\r' => {
+                        eol_check(&mut diags, &seg, line_start, i);
+                        line_start = if seg.buffer.get(i + 1) == Some(&b'\n') {
+                            iter.next();
+                            i + 2
+                        } else {
+                            i + 1
+                        }
+                    }
                     b'\t' => {
                         let count = seg.buffer[i..].iter().take_while(|&&c| c == b'\t').count();
                         for _ in 1..count {
@@ -389,11 +403,16 @@ fn verify_markup_comment(
         }
     }
 
-    fn check_uninterpreted_escapes(buf: &[u8], sp: Span, mut diag: impl FnMut(u8, Diagnostic)) {
+    fn check_uninterpreted_escapes(
+        buf: &[u8],
+        sp: Span,
+        escape: impl Fn(u8) -> bool,
+        mut diag: impl FnMut(u8, Diagnostic),
+    ) {
         let mut i = sp.start as usize;
         while i < sp.end as usize {
             let c = buf[i];
-            if is_text_escape(c) {
+            if escape(c) {
                 if buf.get(i + 1) == Some(&c) {
                     i += 1;
                 } else {
@@ -405,12 +424,11 @@ fn verify_markup_comment(
     }
 
     fn check_uninterpreted_html(buf: &[u8], sp: Span, diag: &mut impl FnMut(Diagnostic)) {
-        lazy_static::lazy_static! {
-            static ref HTML: Regex = Regex::new("(?i-u)</?HTML>").unwrap();
-        }
+        static HTML: OnceLock<Regex> = OnceLock::new();
+        let html = HTML.get_or_init(|| Regex::new("(?i-u)</?HTML>").unwrap());
         let text = sp.as_ref(buf);
-        if HTML.is_match(text) {
-            if let Some(m) = HTML.find(text) {
+        if html.is_match(text) {
+            if let Some(m) = html.find(text) {
                 diag(Diagnostic::UninterpretedHtml(Span::new2(
                     sp.start + m.start() as u32,
                     sp.start + m.end() as u32,
@@ -421,17 +439,21 @@ fn verify_markup_comment(
 
     let mut temp_buffer = vec![];
     let mut in_math = None;
-    let mut in_html = None;
+    let mut in_html = None::<HtmlParser>;
     for item in CommentParser::new(buf, span) {
         match item {
             CommentItem::Text(sp) => {
-                check_uninterpreted_escapes(buf, sp, |c, d| {
+                let escape = |c| is_text_escape(in_html.is_some(), c);
+                check_uninterpreted_escapes(buf, sp, escape, |c, d| {
                     // Don't report on unescaped [ in regular text
                     if c != b'[' {
                         diag(d)
                     }
                 });
                 check_uninterpreted_html(buf, sp, &mut diag);
+                if let Some(parser) = &mut in_html {
+                    parser.feed(sp.as_ref(buf))
+                }
             }
             CommentItem::StartMathMode(i) => {
                 in_math = Some(i);
@@ -451,20 +473,20 @@ fn verify_markup_comment(
             CommentItem::Label(i, sp) | CommentItem::Url(i, sp) => {
                 ensure_space_before(buf, i, &mut diag);
                 ensure_space_after(buf, i, &mut diag);
-                check_uninterpreted_escapes(buf, sp, |_, d| diag(d));
+                check_uninterpreted_escapes(buf, sp, is_label_escape, |_, d| diag(d));
                 check_uninterpreted_html(buf, sp, &mut diag);
                 if matches!(item, CommentItem::Label(..)) {
                     temp_buffer.clear();
-                    CommentItem::unescape_text(sp.as_ref(buf), &mut temp_buffer);
+                    CommentItem::unescape_label(sp.as_ref(buf), &mut temp_buffer);
                     if temp_buffer.is_empty() {
                         diag(Diagnostic::EmptyLabel(i as u32))
                     } else if db.name_result().lookup_label(&temp_buffer).is_none() {
-                        diag(Diagnostic::UndefinedToken(sp, (&*temp_buffer).into()))
+                        diag(Diagnostic::UnknownLabel(sp))
                     }
                 }
             }
-            CommentItem::StartHtml(i) => in_html = Some(i),
-            CommentItem::EndHtml(_) => in_html = None,
+            CommentItem::StartHtml(i) => in_html = Some(HtmlParser::new(i)),
+            CommentItem::EndHtml(i) => in_html.take().unwrap().validate(i + 7, &mut diag),
             CommentItem::LineBreak(_)
             | CommentItem::StartSubscript(_)
             | CommentItem::EndSubscript(_)
@@ -489,8 +511,8 @@ fn verify_markup_comment(
     if let Some(i) = in_math {
         diag(Diagnostic::UnclosedMathMarkup(i as u32, span.end))
     }
-    if let Some(i) = in_html {
-        diag(Diagnostic::UnclosedHtml(i as u32, span.end))
+    if let Some(parser) = in_html {
+        diag(Diagnostic::UnclosedHtml(parser.start as u32, span.end))
     }
 }
 
@@ -504,9 +526,9 @@ pub struct Bibliography(HashSet<Box<[u8]>>);
 /// A pair of bibliography files. This is used to support `set.mm`, which
 /// contains two separate-ish databases inside one metamath file. Bibliography
 /// references in the first part of the file refer to the
-/// [`TypesettingData::html_bibliography`],
-/// while references after the [`TypesettingData::ext_html_label`] go to the
-/// [`TypesettingData::ext_html_bibliography`].
+/// [`html_bibliography`][crate::typesetting::TypesettingData::html_bibliography],
+/// while references after the [`ext_html_label`][crate::typesetting::TypesettingData::ext_html_label] go to the
+/// [`ext_html_bibliography`][crate::typesetting::TypesettingData::ext_html_bibliography].
 #[derive(Debug)]
 pub struct Bibliography2 {
     /// The main bibliography file.
@@ -525,12 +547,13 @@ impl Bibliography {
     /// Parse bibliography file data out of the given [`SourceInfo`], and put
     /// any parse errors in `diags`.
     pub fn parse<'a>(source: &'a SourceInfo, diags: &mut Vec<(&'a SourceInfo, BibError)>) -> Self {
-        lazy_static::lazy_static! {
-            static ref A_NAME: Regex =
-                Regex::new("(?i-u)<a[[:space:]]name=['\"]?([^&>]*?)['\"]?>").unwrap();
-        }
+        static A_NAME: OnceLock<Regex> = OnceLock::new();
+        let a_name = A_NAME.get_or_init(|| {
+            #[allow(clippy::invalid_regex)] // https://github.com/rust-lang/rust-clippy/issues/10825
+            Regex::new("(?i-u)<a[[:space:]]name=['\"]?([^&>]*?)['\"]?>").unwrap()
+        });
         let mut bib = HashMap::default();
-        for captures in A_NAME.captures_iter(&source.text) {
+        for captures in a_name.captures_iter(&source.text) {
             let m = captures.get(0).unwrap();
             let sp = Span::new(m.start(), m.end());
             if let Some(sp2) = bib.insert(captures.get(1).unwrap().as_bytes().into(), sp) {
@@ -546,3 +569,46 @@ impl Bibliography {
         self.0.contains(tag)
     }
 }
+
+struct HtmlParser {
+    start: usize,
+    parser: Utf8LossyDecoder<html5ever::Parser<scraper::Html>>,
+    string: String,
+}
+
+impl HtmlParser {
+    fn new(start: usize) -> Self {
+        use html5ever::{local_name, namespace_url, ns};
+        let parser = html5ever::driver::parse_fragment(
+            scraper::Html::new_fragment(),
+            html5ever::ParseOpts::default(),
+            html5ever::QualName::new(None, ns!(html), local_name!("div")),
+            vec![],
+        );
+        Self {
+            start,
+            parser: parser.from_utf8(),
+            string: String::new(),
+        }
+    }
+
+    fn feed(&mut self, text: &[u8]) {
+        self.parser.process(Tendril::from_slice(text));
+        self.string += crate::as_str(text);
+    }
+
+    fn validate(self, end: usize, diag: &mut impl FnMut(Diagnostic)) {
+        let mut errors = self.parser.finish().errors;
+        if !errors.is_empty() {
+            // html5ever has garbage error messages (https://github.com/servo/html5ever/issues/492)
+            // but apparently there aren't any other HTML validators and I'm not going to write one
+            // myself
+            errors.sort();
+            errors.dedup();
+            diag(Diagnostic::HtmlParseError(
+                Span::new(self.start, end),
+                errors,
+            ))
+        }
+    }
+}
diff --git a/src/main.rs b/src/main.rs
deleted file mode 100644
index f001fda..0000000
--- a/src/main.rs
+++ /dev/null
@@ -1,221 +0,0 @@
-//! A library for manipulating [Metamath](http://us.metamath.org/#faq)
-//! databases.  The entry point for all API operations is in the `database`
-//! module, as is a discussion of the data representation.
-
-use annotate_snippets::display_list::DisplayList;
-use clap::{clap_app, crate_version};
-use metamath_knife::database::{Database, DbOptions};
-use metamath_knife::diag::{BibError, DiagnosticClass};
-use metamath_knife::statement::StatementAddress;
-use metamath_knife::verify_markup::{Bibliography, Bibliography2};
-use metamath_knife::SourceInfo;
-use simple_logger::SimpleLogger;
-use std::fs::File;
-use std::io::{self, BufWriter};
-use std::mem;
-use std::str::FromStr;
-use std::sync::Arc;
-
-fn positive_integer(val: String) -> Result<(), String> {
-    u32::from_str(&val).map(|_| ()).map_err(|e| format!("{e}"))
-}
-
-fn main() {
-    let app = clap_app!(("smetamath-knife") =>
-        (version: crate_version!())
-        (about: "A Metamath database verifier and processing tool")
-        (@arg DATABASE: required_unless("TEXT") "Database file to load")
-        (@arg TEXT: --text value_names(&["NAME", "TEXT"]) ...
-            "Provide raw database content on the command line")
-        (@arg split: --split "Process files > 1 MiB in multiple segments")
-        (@arg timing: --timing "Print milliseconds after each stage")
-        (@arg verify: -v --verify "Check proof validity")
-        (@arg verify_markup: -m --("verify-markup") "Check comment markup")
-        (@arg discouraged: -D --discouraged [FILE] "Regenerate `discouraged` file")
-        (@arg outline: -O --outline "Show database outline")
-        (@arg print_typesetting: --("dump-typesetting") "Show typesetting information")
-        (@arg parse_typesetting: -t --("parse-typesetting") "Parse typesetting information")
-        (@arg grammar: -g --grammar "Check grammar")
-        (@arg parse_stmt: -p --("parse-stmt")
-            "Parse all statements according to the database's grammar")
-        (@arg verify_parse_stmt: --("verify-parse-stmt")
-            "Check that printing parsed statements gives back the original formulas")
-        (@arg print_grammar: -G --("print-grammar") "Print the database's grammar")
-        (@arg print_formula: -F --("print-formula") "Dump the formulas of this database")
-        (@arg debug: --debug
-            "Activate debug logs, including for the grammar building and statement parsing")
-        (@arg trace_recalc: --("trace-recalc") "Print segments as they are recalculated")
-        (@arg free: --free "Explicitly deallocate working memory before exit")
-        (@arg repeat: --repeat "Demonstrate incremental verifier")
-        (@arg jobs: -j --jobs +takes_value validator(positive_integer)
-            "Number of threads to use for verification")
-        (@arg export: -e --export [LABEL] ... "Output a proof file")
-        (@arg biblio: --biblio [FILE] ... "Supply a bibliography file for verify-markup\n\
-            Can be used one or two times; the second is for exthtml processing")
-    );
-
-    #[cfg(feature = "dot")]
-    let app = clap_app!(@app (app)
-        (@arg export_grammar_dot: -E --("export-grammar-dot")
-            "Export the database's grammar in Graphviz DOT format for visualization")
-    );
-
-    let matches = app.get_matches();
-
-    let options = DbOptions {
-        autosplit: matches.is_present("split"),
-        timing: matches.is_present("timing"),
-        trace_recalc: matches.is_present("trace_recalc"),
-        incremental: matches.is_present("repeat")
-            || matches.is_present("grammar")
-            || matches.is_present("parse_stmt")
-            || matches.is_present("verify_parse_stmt")
-            || matches.is_present("export_grammar_dot")
-            || matches.is_present("print_grammar")
-            || matches.is_present("print_formula"),
-        jobs: usize::from_str(matches.value_of("jobs").unwrap_or("1"))
-            .expect("validator should check this"),
-    };
-
-    if matches.is_present("debug") {
-        SimpleLogger::new().init().unwrap();
-    }
-
-    let mut db = Database::new(options);
-
-    let mut data = Vec::new();
-    if let Some(tvals) = matches.values_of_lossy("TEXT") {
-        for kv in tvals.chunks(2) {
-            data.push((kv[0].clone(), kv[1].clone().into_bytes()));
-        }
-    }
-    let start = matches
-        .value_of("DATABASE")
-        .map(|x| x.to_owned())
-        .unwrap_or_else(|| data[0].0.clone());
-
-    loop {
-        db.parse(start.clone(), data.clone());
-
-        let mut types = vec![DiagnosticClass::Parse];
-
-        if !matches.is_present("discouraged") {
-            types.push(DiagnosticClass::Scope);
-        }
-
-        if matches.is_present("verify") {
-            types.push(DiagnosticClass::Verify);
-        }
-
-        if matches.is_present("grammar") {
-            types.push(DiagnosticClass::Grammar);
-        }
-
-        if matches.is_present("parse_stmt") {
-            types.push(DiagnosticClass::StmtParse);
-        }
-
-        if matches.is_present("parse_typesetting") {
-            types.push(DiagnosticClass::Typesetting);
-        }
-
-        if matches.is_present("verify_parse_stmt") {
-            db.stmt_parse_pass();
-            db.verify_parse_stmt();
-        }
-
-        let mut diags = db.diag_notations(&types);
-
-        if matches.is_present("discouraged") {
-            File::create(matches.value_of("discouraged").unwrap())
-                .and_then(|file| db.write_discouraged(&mut BufWriter::new(file)))
-                .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
-        }
-
-        let mut count = db
-            .render_diags(diags, |snippet| {
-                println!("{}", DisplayList::from(snippet));
-            })
-            .len();
-
-        if matches.is_present("verify_markup") {
-            db.scope_pass();
-            db.typesetting_pass();
-
-            let sources = matches.values_of("biblio").map_or_else(Vec::new, |vals| {
-                assert!(vals.len() <= 2, "expected at most 2 bibliography files");
-                vals.map(|val| {
-                    let file = std::fs::read(val).unwrap();
-                    SourceInfo::new(val.to_owned(), Arc::new(file))
-                })
-                .collect()
-            });
-            let mut bib_diags = vec![];
-            let mut bibs = sources
-                .iter()
-                .map(|source| Bibliography::parse(source, &mut bib_diags));
-            let bib = bibs.next().map(|base| Bibliography2 {
-                base,
-                ext: bibs.next(),
-            });
-
-            count += BibError::render_list(&bib_diags, |snippet| {
-                println!("{}", DisplayList::from(snippet));
-            })
-            .len();
-
-            let diags = db.verify_markup(bib.as_ref());
-            count += db
-                .render_diags(diags, |snippet| {
-                    println!("{}", DisplayList::from(snippet));
-                })
-                .len();
-        }
-
-        println!("{count} diagnostics issued.");
-
-        if matches.is_present("print_grammar") {
-            db.print_grammar();
-        }
-
-        #[cfg(feature = "dot")]
-        if matches.is_present("export_grammar_dot") {
-            db.export_grammar_dot();
-        }
-
-        if matches.is_present("print_formula") {
-            db.print_formula();
-        }
-
-        if matches.is_present("outline") {
-            db.outline_pass();
-            db.print_outline();
-        }
-
-        if matches.is_present("print_typesetting") {
-            db.typesetting_pass();
-            db.print_typesetting();
-        }
-
-        if let Some(exps) = matches.values_of_lossy("export") {
-            for file in exps {
-                db.export(&file);
-            }
-        }
-
-        if matches.is_present("repeat") {
-            let mut input = String::new();
-            if io::stdin().read_line(&mut input).unwrap() == 0 {
-                break;
-            }
-        } else {
-            if !matches.is_present("free") {
-                mem::forget(db);
-            }
-
-            // Exit with code 1 if any warning or error were encountered
-            let code = if count > 0 { 1 } else { 0 };
-            std::process::exit(code);
-        }
-    }
-}