summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorterru2026-06-16 12:00:51 +0200
committerterru2026-06-16 12:00:51 +0200
commit637871e36a4df96e6fc7529b1356da59a1d32b8b (patch)
tree7f89a80ce84a225442f4e9bfda8fc2e8c04fd73b
parent7dba866d6a42bafb39455d853ac6672cc91e0132 (diff)
don't fail on repeated useHEADmain
Diffstat
-rw-r--r--src/message-unescape.js1071
1 files changed, 537 insertions, 534 deletions
diff --git a/src/message-unescape.js b/src/message-unescape.js
index 39197c8..984a5ad 100644
--- a/src/message-unescape.js
+++ b/src/message-unescape.js
@@ -1,543 +1,546 @@
-// content of etc/symbols in Isabelle
-// Copyright (c) 1986-2026,
-// University of Cambridge,
-// Technische Universitaet Muenchen,
-// and contributors.
-const symbols_file = `
-# Default interpretation of some Isabelle symbols
+if (typeof symbols_file === typeof undefined) {
+ // content of etc/symbols in Isabelle
+ // Copyright (c) 1986-2026,
+ // University of Cambridge,
+ // Technische Universitaet Muenchen,
+ // and contributors.
+ let symbols_file = `
+ # Default interpretation of some Isabelle symbols
-\\<zero> code: 0x01d7ec group: digit
-\\<one> code: 0x01d7ed group: digit
-\\<two> code: 0x01d7ee group: digit
-\\<three> code: 0x01d7ef group: digit
-\\<four> code: 0x01d7f0 group: digit
-\\<five> code: 0x01d7f1 group: digit
-\\<six> code: 0x01d7f2 group: digit
-\\<seven> code: 0x01d7f3 group: digit
-\\<eight> code: 0x01d7f4 group: digit
-\\<nine> code: 0x01d7f5 group: digit
-\\<A> code: 0x01d49c group: letter
-\\<B> code: 0x00212c group: letter
-\\<C> code: 0x01d49e group: letter
-\\<D> code: 0x01d49f group: letter
-\\<E> code: 0x002130 group: letter
-\\<F> code: 0x002131 group: letter
-\\<G> code: 0x01d4a2 group: letter
-\\<H> code: 0x00210b group: letter
-\\<I> code: 0x002110 group: letter
-\\<J> code: 0x01d4a5 group: letter
-\\<K> code: 0x01d4a6 group: letter
-\\<L> code: 0x002112 group: letter
-\\<M> code: 0x002133 group: letter
-\\<N> code: 0x01d4a9 group: letter
-\\<O> code: 0x01d4aa group: letter
-\\<P> code: 0x01d4ab group: letter
-\\<Q> code: 0x01d4ac group: letter
-\\<R> code: 0x00211b group: letter
-\\<S> code: 0x01d4ae group: letter
-\\<T> code: 0x01d4af group: letter
-\\<U> code: 0x01d4b0 group: letter
-\\<V> code: 0x01d4b1 group: letter
-\\<W> code: 0x01d4b2 group: letter
-\\<X> code: 0x01d4b3 group: letter
-\\<Y> code: 0x01d4b4 group: letter
-\\<Z> code: 0x01d4b5 group: letter
-\\<a> code: 0x01d5ba group: letter
-\\<b> code: 0x01d5bb group: letter
-\\<c> code: 0x01d5bc group: letter
-\\<d> code: 0x01d5bd group: letter
-\\<e> code: 0x01d5be group: letter
-\\<f> code: 0x01d5bf group: letter
-\\<g> code: 0x01d5c0 group: letter
-\\<h> code: 0x01d5c1 group: letter
-\\<i> code: 0x01d5c2 group: letter
-\\<j> code: 0x01d5c3 group: letter
-\\<k> code: 0x01d5c4 group: letter
-\\<l> code: 0x01d5c5 group: letter
-\\<m> code: 0x01d5c6 group: letter
-\\<n> code: 0x01d5c7 group: letter
-\\<o> code: 0x01d5c8 group: letter
-\\<p> code: 0x01d5c9 group: letter
-\\<q> code: 0x01d5ca group: letter
-\\<r> code: 0x01d5cb group: letter
-\\<s> code: 0x01d5cc group: letter
-\\<t> code: 0x01d5cd group: letter
-\\<u> code: 0x01d5ce group: letter
-\\<v> code: 0x01d5cf group: letter
-\\<w> code: 0x01d5d0 group: letter
-\\<x> code: 0x01d5d1 group: letter
-\\<y> code: 0x01d5d2 group: letter
-\\<z> code: 0x01d5d3 group: letter
-\\<AA> code: 0x01d504 group: letter
-\\<BB> code: 0x01d505 group: letter
-\\<CC> code: 0x00212d group: letter
-\\<DD> code: 0x01d507 group: letter
-\\<EE> code: 0x01d508 group: letter
-\\<FF> code: 0x01d509 group: letter
-\\<GG> code: 0x01d50a group: letter
-\\<HH> code: 0x00210c group: letter
-\\<II> code: 0x002111 group: letter
-\\<JJ> code: 0x01d50d group: letter
-\\<KK> code: 0x01d50e group: letter
-\\<LL> code: 0x01d50f group: letter
-\\<MM> code: 0x01d510 group: letter
-\\<NN> code: 0x01d511 group: letter
-\\<OO> code: 0x01d512 group: letter
-\\<PP> code: 0x01d513 group: letter
-\\<QQ> code: 0x01d514 group: letter
-\\<RR> code: 0x00211c group: letter
-\\<SS> code: 0x01d516 group: letter
-\\<TT> code: 0x01d517 group: letter
-\\<UU> code: 0x01d518 group: letter
-\\<VV> code: 0x01d519 group: letter
-\\<WW> code: 0x01d51a group: letter
-\\<XX> code: 0x01d51b group: letter
-\\<YY> code: 0x01d51c group: letter
-\\<ZZ> code: 0x002128 group: letter
-\\<aa> code: 0x01d51e group: letter
-\\<bb> code: 0x01d51f group: letter
-\\<cc> code: 0x01d520 group: letter
-\\<dd> code: 0x01d521 group: letter
-\\<ee> code: 0x01d522 group: letter
-\\<ff> code: 0x01d523 group: letter
-\\<gg> code: 0x01d524 group: letter
-\\<hh> code: 0x01d525 group: letter
-\\<ii> code: 0x01d526 group: letter
-\\<jj> code: 0x01d527 group: letter
-\\<kk> code: 0x01d528 group: letter
-\\<ll> code: 0x01d529 group: letter
-\\<mm> code: 0x01d52a group: letter
-\\<nn> code: 0x01d52b group: letter
-\\<oo> code: 0x01d52c group: letter
-\\<pp> code: 0x01d52d group: letter
-\\<qq> code: 0x01d52e group: letter
-\\<rr> code: 0x01d52f group: letter
-\\<ss> code: 0x01d530 group: letter
-\\<tt> code: 0x01d531 group: letter
-\\<uu> code: 0x01d532 group: letter
-\\<vv> code: 0x01d533 group: letter
-\\<ww> code: 0x01d534 group: letter
-\\<xx> code: 0x01d535 group: letter
-\\<yy> code: 0x01d536 group: letter
-\\<zz> code: 0x01d537 group: letter
-\\<alpha> code: 0x0003b1 group: greek
-\\<beta> code: 0x0003b2 group: greek
-\\<gamma> code: 0x0003b3 group: greek
-\\<delta> code: 0x0003b4 group: greek
-\\<epsilon> code: 0x0003b5 group: greek
-\\<zeta> code: 0x0003b6 group: greek
-\\<eta> code: 0x0003b7 group: greek
-\\<theta> code: 0x0003b8 group: greek
-\\<iota> code: 0x0003b9 group: greek
-\\<kappa> code: 0x0003ba group: greek
-\\<lambda> code: 0x0003bb group: greek abbrev: %
-\\<mu> code: 0x0003bc group: greek
-\\<nu> code: 0x0003bd group: greek
-\\<xi> code: 0x0003be group: greek
-\\<pi> code: 0x0003c0 group: greek
-\\<rho> code: 0x0003c1 group: greek
-\\<sigma> code: 0x0003c3 group: greek
-\\<tau> code: 0x0003c4 group: greek
-\\<upsilon> code: 0x0003c5 group: greek
-\\<phi> code: 0x0003c6 group: greek
-\\<chi> code: 0x0003c7 group: greek
-\\<psi> code: 0x0003c8 group: greek
-\\<omega> code: 0x0003c9 group: greek
-\\<Gamma> code: 0x000393 group: greek
-\\<Delta> code: 0x000394 group: greek
-\\<Theta> code: 0x000398 group: greek
-\\<Lambda> code: 0x00039b group: greek
-\\<Xi> code: 0x00039e group: greek
-\\<Pi> code: 0x0003a0 group: greek
-\\<Sigma> code: 0x0003a3 group: greek
-\\<Upsilon> code: 0x0003a5 group: greek
-\\<Phi> code: 0x0003a6 group: greek
-\\<Psi> code: 0x0003a8 group: greek
-\\<Omega> code: 0x0003a9 group: greek
-\\<bbbA> code: 0x01D538 group: letter group: Z_Notation
-\\<bool> code: 0x01d539 group: letter group: Z_Notation
-\\<complex> code: 0x002102 group: letter
-\\<bbbD> code: 0x01D53B group: letter
-\\<bbbE> code: 0x01D53C group: letter
-\\<bbbF> code: 0x01D53D group: letter group: Z_Notation
-\\<bbbG> code: 0x01D53E group: letter
-\\<bbbH> code: 0x00210D group: letter
-\\<bbbI> code: 0x01D540 group: letter
-\\<bbbJ> code: 0x01D541 group: letter
-\\<bbbK> code: 0x01D542 group: letter
-\\<bbbL> code: 0x01D543 group: letter
-\\<bbbM> code: 0x01D544 group: letter
-\\<nat> code: 0x002115 group: letter group: Z_Notation
-\\<bbbO> code: 0x01D546 group: letter
-\\<bbbP> code: 0x002119 group: letter group: Z_Notation
-\\<rat> code: 0x00211a group: letter
-\\<real> code: 0x00211d group: letter group: Z_Notation
-\\<bbbS> code: 0x01D54A group: letter
-\\<bbbT> code: 0x01D54B group: letter
-\\<bbbU> code: 0x01D54C group: letter group: Z_Notation
-\\<bbbV> code: 0x01D54D group: letter
-\\<bbbW> code: 0x01D54E group: letter group: Z_Notation
-\\<bbbX> code: 0x01D54F group: letter
-\\<bbbY> code: 0x01D550 group: letter
-\\<int> code: 0x002124 group: letter
-\\<leftarrow> code: 0x002190 group: arrow abbrev: <.
-\\<longleftarrow> code: 0x0027f5 group: arrow abbrev: <.
-\\<longlongleftarrow> code: 0x00290e group: arrow abbrev: <.
-\\<longlonglongleftarrow> code: 0x0021e0 group: arrow abbrev: <.
-\\<rightarrow> code: 0x002192 group: arrow group: Z_Notation abbrev: .> abbrev: ->
-\\<longrightarrow> code: 0x0027f6 group: arrow abbrev: .> abbrev: -->
-\\<longlongrightarrow> code: 0x00290f group: arrow abbrev: .> abbrev: --->
-\\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .> abbrev: --->
-\\<Leftarrow> code: 0x0021d0 group: arrow abbrev: <.
-\\<Longleftarrow> code: 0x0027f8 group: arrow abbrev: <.
-\\<Lleftarrow> code: 0x0021da group: arrow abbrev: <.
-\\<Rightarrow> code: 0x0021d2 group: arrow abbrev: .> abbrev: =>
-\\<Longrightarrow> code: 0x0027f9 group: arrow abbrev: .> abbrev: ==>
-\\<Rrightarrow> code: 0x0021db group: arrow abbrev: .>
-\\<leftrightarrow> code: 0x002194 group: arrow group: Z_Notation abbrev: <> abbrev: <->
-\\<longleftrightarrow> code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <-->
-\\<Leftrightarrow> code: 0x0021d4 group: arrow abbrev: <>
-\\<Longleftrightarrow> code: 0x0027fa group: arrow abbrev: <>
-\\<mapsto> code: 0x0021a6 group: arrow group: Z_Notation abbrev: .> abbrev: |->
-\\<longmapsto> code: 0x0027fc group: arrow abbrev: .> abbrev: |-->
-\\<midarrow> code: 0x002500 group: arrow abbrev: <>
-\\<Midarrow> code: 0x002550 group: arrow abbrev: <>
-\\<hookleftarrow> code: 0x0021a9 group: arrow abbrev: <.
-\\<hookrightarrow> code: 0x0021aa group: arrow abbrev: .>
-\\<leftharpoondown> code: 0x0021bd group: arrow abbrev: <.
-\\<rightharpoondown> code: 0x0021c1 group: arrow abbrev: .>
-\\<leftharpoonup> code: 0x0021bc group: arrow abbrev: <.
-\\<rightharpoonup> code: 0x0021c0 group: arrow abbrev: .>
-\\<rightleftharpoons> code: 0x0021cc group: arrow abbrev: <> abbrev: ==
-\\<leadsto> code: 0x00219d group: arrow group: Z_Notation abbrev: .> abbrev: ~>
-\\<downharpoonleft> code: 0x0021c3 group: arrow
-\\<downharpoonright> code: 0x0021c2 group: arrow
-\\<upharpoonleft> code: 0x0021bf group: arrow group: Z_Notation
-#\\<upharpoonright> code: 0x0021be group: arrow
-\\<restriction> code: 0x0021be group: operator group: Z_Notation
-\\<Colon> code: 0x002237 group: punctuation
-\\<up> code: 0x002191 group: arrow
-\\<Up> code: 0x0021d1 group: arrow
-\\<down> code: 0x002193 group: arrow
-\\<Down> code: 0x0021d3 group: arrow
-\\<updown> code: 0x002195 group: arrow
-\\<Updown> code: 0x0021d5 group: arrow
-\\<langle> code: 0x0027e8 group: punctuation group: Z_Notation abbrev: <<
-\\<rangle> code: 0x0027e9 group: punctuation group: Z_Notation abbrev: >>
-\\<llangle> code: 0x0027ea group: punctuation group: Z_Notation abbrev: <<
-\\<rrangle> code: 0x0027eb group: punctuation group: Z_Notation abbrev: >>
-\\<lceil> code: 0x002308 group: punctuation abbrev: [.
-\\<rceil> code: 0x002309 group: punctuation abbrev: .]
-\\<lfloor> code: 0x00230a group: punctuation abbrev: [.
-\\<rfloor> code: 0x00230b group: punctuation abbrev: .]
-\\<lparr> code: 0x002987 group: punctuation group: Z_Notation abbrev: (|
-\\<rparr> code: 0x002988 group: punctuation group: Z_Notation abbrev: |)
-\\<lbrakk> code: 0x0027e6 group: punctuation group: Z_Notation abbrev: [|
-\\<rbrakk> code: 0x0027e7 group: punctuation group: Z_Notation abbrev: |]
-\\<lbrace> code: 0x002983 group: punctuation abbrev: {|
-\\<rbrace> code: 0x002984 group: punctuation abbrev: |}
-\\<lblot> code: 0x002989 group: punctuation group: Z_Notation abbrev: <<
-\\<rblot> code: 0x00298A group: punctuation group: Z_Notation abbrev: >>
-\\<guillemotleft> code: 0x0000ab group: punctuation abbrev: <<
-\\<guillemotright> code: 0x0000bb group: punctuation abbrev: >>
-\\<bottom> code: 0x0022a5 group: logic
-\\<top> code: 0x0022a4 group: logic
-\\<and> code: 0x002227 group: logic abbrev: /\\ abbrev: &
-\\<And> code: 0x0022c0 group: logic abbrev: !!
-\\<or> code: 0x002228 group: logic abbrev: \\/ abbrev: |
-\\<Or> code: 0x0022c1 group: logic abbrev: ??
-\\<forall> code: 0x002200 group: logic abbrev: ! abbrev: ALL
-\\<exists> code: 0x002203 group: logic abbrev: ? abbrev: EX
-\\<nexists> code: 0x002204 group: logic abbrev: ~?
-\\<not> code: 0x0000ac group: logic abbrev: ~
-\\<circle> code: 0x0025cb group: logic
-\\<box> code: 0x0025a1 group: logic
-\\<diamond> code: 0x0025c7 group: logic
-\\<diamondop> code: 0x0022c4 group: operator
-\\<turnstile> code: 0x0022a2 group: relation abbrev: |-
-\\<Turnstile> code: 0x0022a8 group: relation abbrev: |=
-\\<tturnstile> code: 0x0022a9 group: relation abbrev: |-
-\\<TTurnstile> code: 0x0022ab group: relation abbrev: |=
-\\<stileturn> code: 0x0022a3 group: relation abbrev: -|
-\\<surd> code: 0x00221a group: relation
-\\<le> code: 0x002264 group: relation abbrev: <=
-\\<ge> code: 0x002265 group: relation abbrev: >=
-\\<lless> code: 0x00226a group: relation abbrev: <<
-\\<ggreater> code: 0x00226b group: relation abbrev: >>
-\\<lesssim> code: 0x002272 group: relation
-\\<greatersim> code: 0x002273 group: relation
-\\<lessapprox> code: 0x002a85 group: relation
-\\<greaterapprox> code: 0x002a86 group: relation
-\\<in> code: 0x002208 group: relation abbrev: :
-\\<notin> code: 0x002209 group: relation abbrev: ~:
-\\<subset> code: 0x002282 group: relation
-\\<supset> code: 0x002283 group: relation
-\\<subseteq> code: 0x002286 group: relation abbrev: (=
-\\<supseteq> code: 0x002287 group: relation abbrev: )=
-\\<sqsubset> code: 0x00228f group: relation
-\\<sqsupset> code: 0x002290 group: relation
-\\<sqsubseteq> code: 0x002291 group: relation abbrev: [=
-\\<sqsupseteq> code: 0x002292 group: relation abbrev: ]=
-\\<inter> code: 0x002229 group: operator abbrev: Int
-\\<Inter> code: 0x0022c2 group: operator abbrev: Inter abbrev: INT
-\\<union> code: 0x00222a group: operator abbrev: Un
-\\<Union> code: 0x0022c3 group: operator abbrev: Union abbrev: UN
-\\<squnion> code: 0x002294 group: operator
-\\<Squnion> code: 0x002a06 group: operator abbrev: SUP
-\\<sqinter> code: 0x002293 group: operator
-\\<Sqinter> code: 0x002a05 group: operator abbrev: INF
-\\<setminus> code: 0x002216 group: operator
-\\<propto> code: 0x00221d group: operator
-\\<uplus> code: 0x00228e group: operator group: Z_Notation
-\\<Uplus> code: 0x002a04 group: operator
-\\<noteq> code: 0x002260 group: relation abbrev: ~=
-\\<sim> code: 0x00223c group: relation
-\\<doteq> code: 0x002250 group: relation abbrev: .=
-\\<simeq> code: 0x002243 group: relation
-\\<approx> code: 0x002248 group: relation
-\\<asymp> code: 0x00224d group: relation
-\\<cong> code: 0x002245 group: relation
-\\<smile> code: 0x002323 group: relation
-\\<equiv> code: 0x002261 group: relation abbrev: ==
-\\<frown> code: 0x002322 group: relation
-\\<Join> code: 0x0022c8
-\\<bowtie> code: 0x002a1d
-\\<prec> code: 0x00227a group: relation
-\\<succ> code: 0x00227b group: relation
-\\<preceq> code: 0x00227c group: relation
-\\<succeq> code: 0x00227d group: relation
-\\<parallel> code: 0x002225 group: relation abbrev: ||
-\\<Parallel> code: 0x002016 group: relation abbrev: ||
-\\<interleave> code: 0x002af4 group: relation abbrev: ||
-\\<sslash> code: 0x002afd group: relation abbrev: ||
-\\<bar> code: 0x0000a6 group: punctuation abbrev: ||
-\\<bbar> code: 0x002aff group: punctuation abbrev: ||
-\\<plusminus> code: 0x0000b1 group: operator
-\\<minusplus> code: 0x002213 group: operator
-\\<times> code: 0x0000d7 group: operator abbrev: <*>
-\\<div> code: 0x0000f7 group: operator
-\\<cdot> code: 0x0022c5 group: operator
-\\<star> code: 0x0022c6 group: operator
-\\<bullet> code: 0x002219 group: operator
-\\<circ> code: 0x002218 group: operator
-\\<dagger> code: 0x002020
-\\<ddagger> code: 0x002021
-\\<lhd> code: 0x0022b2 group: relation
-\\<rhd> code: 0x0022b3 group: relation
-\\<unlhd> code: 0x0022b4 group: relation
-\\<unrhd> code: 0x0022b5 group: relation
-\\<triangleleft> code: 0x0025c3 group: relation
-\\<triangleright> code: 0x0025b9 group: relation
-\\<triangle> code: 0x0025b3 group: relation
-\\<triangleq> code: 0x00225c group: relation
-\\<oplus> code: 0x002295 group: operator group: Z_Notation
-\\<Oplus> code: 0x002a01 group: operator
-\\<otimes> code: 0x002297 group: operator
-\\<Otimes> code: 0x002a02 group: operator
-\\<odot> code: 0x002299 group: operator
-\\<Odot> code: 0x002a00 group: operator
-\\<ominus> code: 0x002296 group: operator
-\\<oslash> code: 0x002298 group: operator
-\\<dots> code: 0x002026 group: punctuation abbrev: ...
-\\<cdots> code: 0x0022ef group: punctuation
-\\<Sum> code: 0x002211 group: operator abbrev: SUM
-\\<Prod> code: 0x00220f group: operator abbrev: PROD
-\\<Coprod> code: 0x002210 group: operator
-\\<infinity> code: 0x00221e
-\\<integral> code: 0x00222b group: operator
-\\<ointegral> code: 0x00222e group: operator
-\\<clubsuit> code: 0x002663
-\\<diamondsuit> code: 0x002662
-\\<heartsuit> code: 0x002661
-\\<spadesuit> code: 0x002660
-\\<aleph> code: 0x002135
-\\<emptyset> code: 0x002205
-\\<nabla> code: 0x002207
-\\<partial> code: 0x002202
-\\<flat> code: 0x00266d
-\\<natural> code: 0x00266e
-\\<sharp> code: 0x00266f group: Z_Notation
-\\<angle> code: 0x002220
-\\<copyright> code: 0x0000a9
-\\<registered> code: 0x0000ae
-\\<hyphen> code: 0x002010 group: punctuation
-\\<inverse> code: 0x0000af group: operator
-\\<sqdot> code: 0x0000b7 group: punctuation
-\\<onequarter> code: 0x0000bc group: digit
-\\<onehalf> code: 0x0000bd group: digit
-\\<threequarters> code: 0x0000be group: digit
-\\<ordfeminine> code: 0x0000aa
-\\<ordmasculine> code: 0x0000ba
-\\<section> code: 0x0000a7
-\\<paragraph> code: 0x0000b6
-\\<exclamdown> code: 0x0000a1
-\\<questiondown> code: 0x0000bf
-\\<euro> code: 0x0020ac
-\\<pounds> code: 0x0000a3
-\\<yen> code: 0x0000a5
-\\<cent> code: 0x0000a2
-\\<currency> code: 0x0000a4
-\\<degree> code: 0x0000b0
-\\<amalg> code: 0x002a3f group: operator
-\\<mho> code: 0x002127 group: operator
-\\<lozenge> code: 0x0025ca
-\\<wp> code: 0x002118
-\\<wrong> code: 0x002240 group: relation
-\\<acute> code: 0x0000b4
-\\<index> code: 0x000131
-\\<dieresis> code: 0x0000a8
-\\<cedilla> code: 0x0000b8
-\\<hungarumlaut> code: 0x0002dd
-\\<bind> code: 0x00291c group: operator abbrev: >>=
-\\<then> code: 0x002aa2 group: operator group: Z_Notation abbrev: >>
-\\<some> code: 0x0003f5
-\\<Zcomp> code: 0x002A3E group: Z_Notation group: punctuation
-\\<Zinj> code: 0x0021A3 group: Z_Notation group: arrow abbrev: .>
-\\<Zpinj> code: 0x002914 group: Z_Notation group: arrow abbrev: .>
-\\<Zfinj> code: 0x002915 group: Z_Notation group: arrow abbrev: .>
-\\<Zsurj> code: 0x0021A0 group: Z_Notation group: arrow abbrev: .>
-\\<Zpsurj> code: 0x002900 group: Z_Notation group: arrow abbrev: .>
-\\<Zbij> code: 0x002916 group: Z_Notation group: arrow abbrev: .>
-\\<Zpfun> code: 0x0021F8 group: Z_Notation group: arrow abbrev: .>
-\\<Zffun> code: 0x0021FB group: Z_Notation group: arrow abbrev: .>
-\\<Zdres> code: 0x0025C1 group: Z_Notation group: relation
-\\<Zndres> code: 0x002A64 group: Z_Notation group: relation
-\\<Zrres> code: 0x0025B7 group: Z_Notation group: relation
-\\<Znrres> code: 0x002A65 group: Z_Notation group: relation
-\\<Zspot> code: 0x002981 group: Z_Notation group: punctuation
-\\<Zsemi> code: 0x002A1F group: Z_Notation
-\\<Zproject> code: 0x002A21 group: Z_Notation group: operator
-\\<Ztypecolon> code: 0x002982 group: Z_Notation group: relation
-\\<Zhide> code: 0x0029F9 group: Z_Notation group: operator
-\\<Zcat> code: 0x002040 group: Z_Notation group: operator
-\\<Zinbag> code: 0x0022FF group: Z_Notation group: relation
-\\<Zprime> code: 0x002032 group: Z_Notation group: punctuation
-\\<hole> code: 0x002311
-\\<newline> code: 0x0023ce
-\\<comment> code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^latex> group: document argument: cartouche
-\\<^marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<checkmark> code: 0x002713
-\\<crossmark> code: 0x002717
-\\<open> code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: <<
-\\<close> code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >>
-\\<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^undefined> code: 0x002756 font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^noindent> code: 0x0021e4 group: document font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^smallskip> code: 0x002508 group: document font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^medskip> code: 0x002509 group: document font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^bigskip> code: 0x002501 group: document font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^item> code: 0x0025aa group: document font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^enum> code: 0x0025b8 group: document font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^descr> code: 0x0027a7 group: document font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^footnote> code: 0x00204b group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^verbatim> code: 0x0025a9 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^theory_text> code: 0x002b1a group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^emph> code: 0x002217 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^bold> code: 0x002759 group: control argument: cartouche group: document font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^sub> code: 0x0021e9 group: control font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^sup> code: 0x0021e7 group: control font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^bsub> code: 0x0021d8 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_(
-\\<^esub> code: 0x0021d9 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_)
-\\<^bsup> code: 0x0021d7 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^(
-\\<^esup> code: 0x0021d6 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^)
-\\<^file> code: 0x01F5CF group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^dir> code: 0x01F5C0 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^url> code: 0x01F310 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^doc> code: 0x01F4D3 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\\<^assert>
-\\<^binding> argument: cartouche
-\\<^bundle> argument: cartouche
-\\<^can> argument: cartouche
-\\<^class> argument: cartouche
-\\<^class_syntax> argument: cartouche
-\\<^command_keyword> argument: cartouche
-\\<^const> argument: cartouche
-\\<^const_abbrev> argument: cartouche
-\\<^const_name> argument: cartouche
-\\<^const_syntax> argument: cartouche
-\\<^context>
-\\<^cprop> argument: cartouche
-\\<^cterm> argument: cartouche
-\\<^ctyp> argument: cartouche
-\\<^instantiate> argument: cartouche
-\\<^keyword> argument: cartouche
-\\<^locale> argument: cartouche
-\\<^make_judgment>
-\\<^dest_judgment>
-\\<^make_string>
-\\<^method> argument: cartouche
-\\<^named_theorems> argument: cartouche
-\\<^nonterminal> argument: cartouche
-\\<^path> argument: cartouche
-\\<^path_binding> argument: cartouche
-\\<^plugin> argument: cartouche
-\\<^print>
-\\<^prop> argument: cartouche
-\\<^bash_function> argument: cartouche
-\\<^scala> argument: cartouche
-\\<^scala_function> argument: cartouche
-\\<^scala_method> argument: cartouche
-\\<^scala_object> argument: cartouche
-\\<^scala_thread> argument: cartouche
-\\<^scala_type> argument: cartouche
-\\<^session> argument: cartouche
-\\<^simproc> argument: cartouche
-\\<^simproc_setup> argument: cartouche
-\\<^sort> argument: cartouche
-\\<^syntax_const> argument: cartouche
-\\<^system_option> argument: cartouche
-\\<^term> argument: cartouche
-\\<^theory> argument: cartouche
-\\<^theory_context> argument: cartouche
-\\<^tool> argument: cartouche
-\\<^try> argument: cartouche
-\\<^tvar> argument: cartouche
-\\<^typ> argument: cartouche
-\\<^type_abbrev> argument: cartouche
-\\<^type_name> argument: cartouche
-\\<^type_syntax> argument: cartouche
-\\<^var> argument: cartouche
-\\<^oracle_name> argument: cartouche
-\\<^Const> argument: cartouche
-\\<^Const_> argument: cartouche
-\\<^Const_fn> argument: cartouche
-\\<^Type> argument: cartouche
-\\<^Type_fn> argument: cartouche
-\\<^code> argument: cartouche
-\\<^computation> argument: cartouche
-\\<^computation_conv> argument: cartouche
-\\<^computation_check> argument: cartouche
-\\<^if_linux> argument: cartouche
-\\<^if_macos> argument: cartouche
-\\<^if_windows> argument: cartouche
-\\<^if_unix> argument: cartouche
-\\<^if_none> argument: cartouche
-\\<^cite> argument: cartouche
-\\<^nocite> argument: cartouche
-\\<^citet> argument: cartouche
-\\<^citep> argument: cartouche
-`
+ \\<zero> code: 0x01d7ec group: digit
+ \\<one> code: 0x01d7ed group: digit
+ \\<two> code: 0x01d7ee group: digit
+ \\<three> code: 0x01d7ef group: digit
+ \\<four> code: 0x01d7f0 group: digit
+ \\<five> code: 0x01d7f1 group: digit
+ \\<six> code: 0x01d7f2 group: digit
+ \\<seven> code: 0x01d7f3 group: digit
+ \\<eight> code: 0x01d7f4 group: digit
+ \\<nine> code: 0x01d7f5 group: digit
+ \\<A> code: 0x01d49c group: letter
+ \\<B> code: 0x00212c group: letter
+ \\<C> code: 0x01d49e group: letter
+ \\<D> code: 0x01d49f group: letter
+ \\<E> code: 0x002130 group: letter
+ \\<F> code: 0x002131 group: letter
+ \\<G> code: 0x01d4a2 group: letter
+ \\<H> code: 0x00210b group: letter
+ \\<I> code: 0x002110 group: letter
+ \\<J> code: 0x01d4a5 group: letter
+ \\<K> code: 0x01d4a6 group: letter
+ \\<L> code: 0x002112 group: letter
+ \\<M> code: 0x002133 group: letter
+ \\<N> code: 0x01d4a9 group: letter
+ \\<O> code: 0x01d4aa group: letter
+ \\<P> code: 0x01d4ab group: letter
+ \\<Q> code: 0x01d4ac group: letter
+ \\<R> code: 0x00211b group: letter
+ \\<S> code: 0x01d4ae group: letter
+ \\<T> code: 0x01d4af group: letter
+ \\<U> code: 0x01d4b0 group: letter
+ \\<V> code: 0x01d4b1 group: letter
+ \\<W> code: 0x01d4b2 group: letter
+ \\<X> code: 0x01d4b3 group: letter
+ \\<Y> code: 0x01d4b4 group: letter
+ \\<Z> code: 0x01d4b5 group: letter
+ \\<a> code: 0x01d5ba group: letter
+ \\<b> code: 0x01d5bb group: letter
+ \\<c> code: 0x01d5bc group: letter
+ \\<d> code: 0x01d5bd group: letter
+ \\<e> code: 0x01d5be group: letter
+ \\<f> code: 0x01d5bf group: letter
+ \\<g> code: 0x01d5c0 group: letter
+ \\<h> code: 0x01d5c1 group: letter
+ \\<i> code: 0x01d5c2 group: letter
+ \\<j> code: 0x01d5c3 group: letter
+ \\<k> code: 0x01d5c4 group: letter
+ \\<l> code: 0x01d5c5 group: letter
+ \\<m> code: 0x01d5c6 group: letter
+ \\<n> code: 0x01d5c7 group: letter
+ \\<o> code: 0x01d5c8 group: letter
+ \\<p> code: 0x01d5c9 group: letter
+ \\<q> code: 0x01d5ca group: letter
+ \\<r> code: 0x01d5cb group: letter
+ \\<s> code: 0x01d5cc group: letter
+ \\<t> code: 0x01d5cd group: letter
+ \\<u> code: 0x01d5ce group: letter
+ \\<v> code: 0x01d5cf group: letter
+ \\<w> code: 0x01d5d0 group: letter
+ \\<x> code: 0x01d5d1 group: letter
+ \\<y> code: 0x01d5d2 group: letter
+ \\<z> code: 0x01d5d3 group: letter
+ \\<AA> code: 0x01d504 group: letter
+ \\<BB> code: 0x01d505 group: letter
+ \\<CC> code: 0x00212d group: letter
+ \\<DD> code: 0x01d507 group: letter
+ \\<EE> code: 0x01d508 group: letter
+ \\<FF> code: 0x01d509 group: letter
+ \\<GG> code: 0x01d50a group: letter
+ \\<HH> code: 0x00210c group: letter
+ \\<II> code: 0x002111 group: letter
+ \\<JJ> code: 0x01d50d group: letter
+ \\<KK> code: 0x01d50e group: letter
+ \\<LL> code: 0x01d50f group: letter
+ \\<MM> code: 0x01d510 group: letter
+ \\<NN> code: 0x01d511 group: letter
+ \\<OO> code: 0x01d512 group: letter
+ \\<PP> code: 0x01d513 group: letter
+ \\<QQ> code: 0x01d514 group: letter
+ \\<RR> code: 0x00211c group: letter
+ \\<SS> code: 0x01d516 group: letter
+ \\<TT> code: 0x01d517 group: letter
+ \\<UU> code: 0x01d518 group: letter
+ \\<VV> code: 0x01d519 group: letter
+ \\<WW> code: 0x01d51a group: letter
+ \\<XX> code: 0x01d51b group: letter
+ \\<YY> code: 0x01d51c group: letter
+ \\<ZZ> code: 0x002128 group: letter
+ \\<aa> code: 0x01d51e group: letter
+ \\<bb> code: 0x01d51f group: letter
+ \\<cc> code: 0x01d520 group: letter
+ \\<dd> code: 0x01d521 group: letter
+ \\<ee> code: 0x01d522 group: letter
+ \\<ff> code: 0x01d523 group: letter
+ \\<gg> code: 0x01d524 group: letter
+ \\<hh> code: 0x01d525 group: letter
+ \\<ii> code: 0x01d526 group: letter
+ \\<jj> code: 0x01d527 group: letter
+ \\<kk> code: 0x01d528 group: letter
+ \\<ll> code: 0x01d529 group: letter
+ \\<mm> code: 0x01d52a group: letter
+ \\<nn> code: 0x01d52b group: letter
+ \\<oo> code: 0x01d52c group: letter
+ \\<pp> code: 0x01d52d group: letter
+ \\<qq> code: 0x01d52e group: letter
+ \\<rr> code: 0x01d52f group: letter
+ \\<ss> code: 0x01d530 group: letter
+ \\<tt> code: 0x01d531 group: letter
+ \\<uu> code: 0x01d532 group: letter
+ \\<vv> code: 0x01d533 group: letter
+ \\<ww> code: 0x01d534 group: letter
+ \\<xx> code: 0x01d535 group: letter
+ \\<yy> code: 0x01d536 group: letter
+ \\<zz> code: 0x01d537 group: letter
+ \\<alpha> code: 0x0003b1 group: greek
+ \\<beta> code: 0x0003b2 group: greek
+ \\<gamma> code: 0x0003b3 group: greek
+ \\<delta> code: 0x0003b4 group: greek
+ \\<epsilon> code: 0x0003b5 group: greek
+ \\<zeta> code: 0x0003b6 group: greek
+ \\<eta> code: 0x0003b7 group: greek
+ \\<theta> code: 0x0003b8 group: greek
+ \\<iota> code: 0x0003b9 group: greek
+ \\<kappa> code: 0x0003ba group: greek
+ \\<lambda> code: 0x0003bb group: greek abbrev: %
+ \\<mu> code: 0x0003bc group: greek
+ \\<nu> code: 0x0003bd group: greek
+ \\<xi> code: 0x0003be group: greek
+ \\<pi> code: 0x0003c0 group: greek
+ \\<rho> code: 0x0003c1 group: greek
+ \\<sigma> code: 0x0003c3 group: greek
+ \\<tau> code: 0x0003c4 group: greek
+ \\<upsilon> code: 0x0003c5 group: greek
+ \\<phi> code: 0x0003c6 group: greek
+ \\<chi> code: 0x0003c7 group: greek
+ \\<psi> code: 0x0003c8 group: greek
+ \\<omega> code: 0x0003c9 group: greek
+ \\<Gamma> code: 0x000393 group: greek
+ \\<Delta> code: 0x000394 group: greek
+ \\<Theta> code: 0x000398 group: greek
+ \\<Lambda> code: 0x00039b group: greek
+ \\<Xi> code: 0x00039e group: greek
+ \\<Pi> code: 0x0003a0 group: greek
+ \\<Sigma> code: 0x0003a3 group: greek
+ \\<Upsilon> code: 0x0003a5 group: greek
+ \\<Phi> code: 0x0003a6 group: greek
+ \\<Psi> code: 0x0003a8 group: greek
+ \\<Omega> code: 0x0003a9 group: greek
+ \\<bbbA> code: 0x01D538 group: letter group: Z_Notation
+ \\<bool> code: 0x01d539 group: letter group: Z_Notation
+ \\<complex> code: 0x002102 group: letter
+ \\<bbbD> code: 0x01D53B group: letter
+ \\<bbbE> code: 0x01D53C group: letter
+ \\<bbbF> code: 0x01D53D group: letter group: Z_Notation
+ \\<bbbG> code: 0x01D53E group: letter
+ \\<bbbH> code: 0x00210D group: letter
+ \\<bbbI> code: 0x01D540 group: letter
+ \\<bbbJ> code: 0x01D541 group: letter
+ \\<bbbK> code: 0x01D542 group: letter
+ \\<bbbL> code: 0x01D543 group: letter
+ \\<bbbM> code: 0x01D544 group: letter
+ \\<nat> code: 0x002115 group: letter group: Z_Notation
+ \\<bbbO> code: 0x01D546 group: letter
+ \\<bbbP> code: 0x002119 group: letter group: Z_Notation
+ \\<rat> code: 0x00211a group: letter
+ \\<real> code: 0x00211d group: letter group: Z_Notation
+ \\<bbbS> code: 0x01D54A group: letter
+ \\<bbbT> code: 0x01D54B group: letter
+ \\<bbbU> code: 0x01D54C group: letter group: Z_Notation
+ \\<bbbV> code: 0x01D54D group: letter
+ \\<bbbW> code: 0x01D54E group: letter group: Z_Notation
+ \\<bbbX> code: 0x01D54F group: letter
+ \\<bbbY> code: 0x01D550 group: letter
+ \\<int> code: 0x002124 group: letter
+ \\<leftarrow> code: 0x002190 group: arrow abbrev: <.
+ \\<longleftarrow> code: 0x0027f5 group: arrow abbrev: <.
+ \\<longlongleftarrow> code: 0x00290e group: arrow abbrev: <.
+ \\<longlonglongleftarrow> code: 0x0021e0 group: arrow abbrev: <.
+ \\<rightarrow> code: 0x002192 group: arrow group: Z_Notation abbrev: .> abbrev: ->
+ \\<longrightarrow> code: 0x0027f6 group: arrow abbrev: .> abbrev: -->
+ \\<longlongrightarrow> code: 0x00290f group: arrow abbrev: .> abbrev: --->
+ \\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .> abbrev: --->
+ \\<Leftarrow> code: 0x0021d0 group: arrow abbrev: <.
+ \\<Longleftarrow> code: 0x0027f8 group: arrow abbrev: <.
+ \\<Lleftarrow> code: 0x0021da group: arrow abbrev: <.
+ \\<Rightarrow> code: 0x0021d2 group: arrow abbrev: .> abbrev: =>
+ \\<Longrightarrow> code: 0x0027f9 group: arrow abbrev: .> abbrev: ==>
+ \\<Rrightarrow> code: 0x0021db group: arrow abbrev: .>
+ \\<leftrightarrow> code: 0x002194 group: arrow group: Z_Notation abbrev: <> abbrev: <->
+ \\<longleftrightarrow> code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <-->
+ \\<Leftrightarrow> code: 0x0021d4 group: arrow abbrev: <>
+ \\<Longleftrightarrow> code: 0x0027fa group: arrow abbrev: <>
+ \\<mapsto> code: 0x0021a6 group: arrow group: Z_Notation abbrev: .> abbrev: |->
+ \\<longmapsto> code: 0x0027fc group: arrow abbrev: .> abbrev: |-->
+ \\<midarrow> code: 0x002500 group: arrow abbrev: <>
+ \\<Midarrow> code: 0x002550 group: arrow abbrev: <>
+ \\<hookleftarrow> code: 0x0021a9 group: arrow abbrev: <.
+ \\<hookrightarrow> code: 0x0021aa group: arrow abbrev: .>
+ \\<leftharpoondown> code: 0x0021bd group: arrow abbrev: <.
+ \\<rightharpoondown> code: 0x0021c1 group: arrow abbrev: .>
+ \\<leftharpoonup> code: 0x0021bc group: arrow abbrev: <.
+ \\<rightharpoonup> code: 0x0021c0 group: arrow abbrev: .>
+ \\<rightleftharpoons> code: 0x0021cc group: arrow abbrev: <> abbrev: ==
+ \\<leadsto> code: 0x00219d group: arrow group: Z_Notation abbrev: .> abbrev: ~>
+ \\<downharpoonleft> code: 0x0021c3 group: arrow
+ \\<downharpoonright> code: 0x0021c2 group: arrow
+ \\<upharpoonleft> code: 0x0021bf group: arrow group: Z_Notation
+ #\\<upharpoonright> code: 0x0021be group: arrow
+ \\<restriction> code: 0x0021be group: operator group: Z_Notation
+ \\<Colon> code: 0x002237 group: punctuation
+ \\<up> code: 0x002191 group: arrow
+ \\<Up> code: 0x0021d1 group: arrow
+ \\<down> code: 0x002193 group: arrow
+ \\<Down> code: 0x0021d3 group: arrow
+ \\<updown> code: 0x002195 group: arrow
+ \\<Updown> code: 0x0021d5 group: arrow
+ \\<langle> code: 0x0027e8 group: punctuation group: Z_Notation abbrev: <<
+ \\<rangle> code: 0x0027e9 group: punctuation group: Z_Notation abbrev: >>
+ \\<llangle> code: 0x0027ea group: punctuation group: Z_Notation abbrev: <<
+ \\<rrangle> code: 0x0027eb group: punctuation group: Z_Notation abbrev: >>
+ \\<lceil> code: 0x002308 group: punctuation abbrev: [.
+ \\<rceil> code: 0x002309 group: punctuation abbrev: .]
+ \\<lfloor> code: 0x00230a group: punctuation abbrev: [.
+ \\<rfloor> code: 0x00230b group: punctuation abbrev: .]
+ \\<lparr> code: 0x002987 group: punctuation group: Z_Notation abbrev: (|
+ \\<rparr> code: 0x002988 group: punctuation group: Z_Notation abbrev: |)
+ \\<lbrakk> code: 0x0027e6 group: punctuation group: Z_Notation abbrev: [|
+ \\<rbrakk> code: 0x0027e7 group: punctuation group: Z_Notation abbrev: |]
+ \\<lbrace> code: 0x002983 group: punctuation abbrev: {|
+ \\<rbrace> code: 0x002984 group: punctuation abbrev: |}
+ \\<lblot> code: 0x002989 group: punctuation group: Z_Notation abbrev: <<
+ \\<rblot> code: 0x00298A group: punctuation group: Z_Notation abbrev: >>
+ \\<guillemotleft> code: 0x0000ab group: punctuation abbrev: <<
+ \\<guillemotright> code: 0x0000bb group: punctuation abbrev: >>
+ \\<bottom> code: 0x0022a5 group: logic
+ \\<top> code: 0x0022a4 group: logic
+ \\<and> code: 0x002227 group: logic abbrev: /\\ abbrev: &
+ \\<And> code: 0x0022c0 group: logic abbrev: !!
+ \\<or> code: 0x002228 group: logic abbrev: \\/ abbrev: |
+ \\<Or> code: 0x0022c1 group: logic abbrev: ??
+ \\<forall> code: 0x002200 group: logic abbrev: ! abbrev: ALL
+ \\<exists> code: 0x002203 group: logic abbrev: ? abbrev: EX
+ \\<nexists> code: 0x002204 group: logic abbrev: ~?
+ \\<not> code: 0x0000ac group: logic abbrev: ~
+ \\<circle> code: 0x0025cb group: logic
+ \\<box> code: 0x0025a1 group: logic
+ \\<diamond> code: 0x0025c7 group: logic
+ \\<diamondop> code: 0x0022c4 group: operator
+ \\<turnstile> code: 0x0022a2 group: relation abbrev: |-
+ \\<Turnstile> code: 0x0022a8 group: relation abbrev: |=
+ \\<tturnstile> code: 0x0022a9 group: relation abbrev: |-
+ \\<TTurnstile> code: 0x0022ab group: relation abbrev: |=
+ \\<stileturn> code: 0x0022a3 group: relation abbrev: -|
+ \\<surd> code: 0x00221a group: relation
+ \\<le> code: 0x002264 group: relation abbrev: <=
+ \\<ge> code: 0x002265 group: relation abbrev: >=
+ \\<lless> code: 0x00226a group: relation abbrev: <<
+ \\<ggreater> code: 0x00226b group: relation abbrev: >>
+ \\<lesssim> code: 0x002272 group: relation
+ \\<greatersim> code: 0x002273 group: relation
+ \\<lessapprox> code: 0x002a85 group: relation
+ \\<greaterapprox> code: 0x002a86 group: relation
+ \\<in> code: 0x002208 group: relation abbrev: :
+ \\<notin> code: 0x002209 group: relation abbrev: ~:
+ \\<subset> code: 0x002282 group: relation
+ \\<supset> code: 0x002283 group: relation
+ \\<subseteq> code: 0x002286 group: relation abbrev: (=
+ \\<supseteq> code: 0x002287 group: relation abbrev: )=
+ \\<sqsubset> code: 0x00228f group: relation
+ \\<sqsupset> code: 0x002290 group: relation
+ \\<sqsubseteq> code: 0x002291 group: relation abbrev: [=
+ \\<sqsupseteq> code: 0x002292 group: relation abbrev: ]=
+ \\<inter> code: 0x002229 group: operator abbrev: Int
+ \\<Inter> code: 0x0022c2 group: operator abbrev: Inter abbrev: INT
+ \\<union> code: 0x00222a group: operator abbrev: Un
+ \\<Union> code: 0x0022c3 group: operator abbrev: Union abbrev: UN
+ \\<squnion> code: 0x002294 group: operator
+ \\<Squnion> code: 0x002a06 group: operator abbrev: SUP
+ \\<sqinter> code: 0x002293 group: operator
+ \\<Sqinter> code: 0x002a05 group: operator abbrev: INF
+ \\<setminus> code: 0x002216 group: operator
+ \\<propto> code: 0x00221d group: operator
+ \\<uplus> code: 0x00228e group: operator group: Z_Notation
+ \\<Uplus> code: 0x002a04 group: operator
+ \\<noteq> code: 0x002260 group: relation abbrev: ~=
+ \\<sim> code: 0x00223c group: relation
+ \\<doteq> code: 0x002250 group: relation abbrev: .=
+ \\<simeq> code: 0x002243 group: relation
+ \\<approx> code: 0x002248 group: relation
+ \\<asymp> code: 0x00224d group: relation
+ \\<cong> code: 0x002245 group: relation
+ \\<smile> code: 0x002323 group: relation
+ \\<equiv> code: 0x002261 group: relation abbrev: ==
+ \\<frown> code: 0x002322 group: relation
+ \\<Join> code: 0x0022c8
+ \\<bowtie> code: 0x002a1d
+ \\<prec> code: 0x00227a group: relation
+ \\<succ> code: 0x00227b group: relation
+ \\<preceq> code: 0x00227c group: relation
+ \\<succeq> code: 0x00227d group: relation
+ \\<parallel> code: 0x002225 group: relation abbrev: ||
+ \\<Parallel> code: 0x002016 group: relation abbrev: ||
+ \\<interleave> code: 0x002af4 group: relation abbrev: ||
+ \\<sslash> code: 0x002afd group: relation abbrev: ||
+ \\<bar> code: 0x0000a6 group: punctuation abbrev: ||
+ \\<bbar> code: 0x002aff group: punctuation abbrev: ||
+ \\<plusminus> code: 0x0000b1 group: operator
+ \\<minusplus> code: 0x002213 group: operator
+ \\<times> code: 0x0000d7 group: operator abbrev: <*>
+ \\<div> code: 0x0000f7 group: operator
+ \\<cdot> code: 0x0022c5 group: operator
+ \\<star> code: 0x0022c6 group: operator
+ \\<bullet> code: 0x002219 group: operator
+ \\<circ> code: 0x002218 group: operator
+ \\<dagger> code: 0x002020
+ \\<ddagger> code: 0x002021
+ \\<lhd> code: 0x0022b2 group: relation
+ \\<rhd> code: 0x0022b3 group: relation
+ \\<unlhd> code: 0x0022b4 group: relation
+ \\<unrhd> code: 0x0022b5 group: relation
+ \\<triangleleft> code: 0x0025c3 group: relation
+ \\<triangleright> code: 0x0025b9 group: relation
+ \\<triangle> code: 0x0025b3 group: relation
+ \\<triangleq> code: 0x00225c group: relation
+ \\<oplus> code: 0x002295 group: operator group: Z_Notation
+ \\<Oplus> code: 0x002a01 group: operator
+ \\<otimes> code: 0x002297 group: operator
+ \\<Otimes> code: 0x002a02 group: operator
+ \\<odot> code: 0x002299 group: operator
+ \\<Odot> code: 0x002a00 group: operator
+ \\<ominus> code: 0x002296 group: operator
+ \\<oslash> code: 0x002298 group: operator
+ \\<dots> code: 0x002026 group: punctuation abbrev: ...
+ \\<cdots> code: 0x0022ef group: punctuation
+ \\<Sum> code: 0x002211 group: operator abbrev: SUM
+ \\<Prod> code: 0x00220f group: operator abbrev: PROD
+ \\<Coprod> code: 0x002210 group: operator
+ \\<infinity> code: 0x00221e
+ \\<integral> code: 0x00222b group: operator
+ \\<ointegral> code: 0x00222e group: operator
+ \\<clubsuit> code: 0x002663
+ \\<diamondsuit> code: 0x002662
+ \\<heartsuit> code: 0x002661
+ \\<spadesuit> code: 0x002660
+ \\<aleph> code: 0x002135
+ \\<emptyset> code: 0x002205
+ \\<nabla> code: 0x002207
+ \\<partial> code: 0x002202
+ \\<flat> code: 0x00266d
+ \\<natural> code: 0x00266e
+ \\<sharp> code: 0x00266f group: Z_Notation
+ \\<angle> code: 0x002220
+ \\<copyright> code: 0x0000a9
+ \\<registered> code: 0x0000ae
+ \\<hyphen> code: 0x002010 group: punctuation
+ \\<inverse> code: 0x0000af group: operator
+ \\<sqdot> code: 0x0000b7 group: punctuation
+ \\<onequarter> code: 0x0000bc group: digit
+ \\<onehalf> code: 0x0000bd group: digit
+ \\<threequarters> code: 0x0000be group: digit
+ \\<ordfeminine> code: 0x0000aa
+ \\<ordmasculine> code: 0x0000ba
+ \\<section> code: 0x0000a7
+ \\<paragraph> code: 0x0000b6
+ \\<exclamdown> code: 0x0000a1
+ \\<questiondown> code: 0x0000bf
+ \\<euro> code: 0x0020ac
+ \\<pounds> code: 0x0000a3
+ \\<yen> code: 0x0000a5
+ \\<cent> code: 0x0000a2
+ \\<currency> code: 0x0000a4
+ \\<degree> code: 0x0000b0
+ \\<amalg> code: 0x002a3f group: operator
+ \\<mho> code: 0x002127 group: operator
+ \\<lozenge> code: 0x0025ca
+ \\<wp> code: 0x002118
+ \\<wrong> code: 0x002240 group: relation
+ \\<acute> code: 0x0000b4
+ \\<index> code: 0x000131
+ \\<dieresis> code: 0x0000a8
+ \\<cedilla> code: 0x0000b8
+ \\<hungarumlaut> code: 0x0002dd
+ \\<bind> code: 0x00291c group: operator abbrev: >>=
+ \\<then> code: 0x002aa2 group: operator group: Z_Notation abbrev: >>
+ \\<some> code: 0x0003f5
+ \\<Zcomp> code: 0x002A3E group: Z_Notation group: punctuation
+ \\<Zinj> code: 0x0021A3 group: Z_Notation group: arrow abbrev: .>
+ \\<Zpinj> code: 0x002914 group: Z_Notation group: arrow abbrev: .>
+ \\<Zfinj> code: 0x002915 group: Z_Notation group: arrow abbrev: .>
+ \\<Zsurj> code: 0x0021A0 group: Z_Notation group: arrow abbrev: .>
+ \\<Zpsurj> code: 0x002900 group: Z_Notation group: arrow abbrev: .>
+ \\<Zbij> code: 0x002916 group: Z_Notation group: arrow abbrev: .>
+ \\<Zpfun> code: 0x0021F8 group: Z_Notation group: arrow abbrev: .>
+ \\<Zffun> code: 0x0021FB group: Z_Notation group: arrow abbrev: .>
+ \\<Zdres> code: 0x0025C1 group: Z_Notation group: relation
+ \\<Zndres> code: 0x002A64 group: Z_Notation group: relation
+ \\<Zrres> code: 0x0025B7 group: Z_Notation group: relation
+ \\<Znrres> code: 0x002A65 group: Z_Notation group: relation
+ \\<Zspot> code: 0x002981 group: Z_Notation group: punctuation
+ \\<Zsemi> code: 0x002A1F group: Z_Notation
+ \\<Zproject> code: 0x002A21 group: Z_Notation group: operator
+ \\<Ztypecolon> code: 0x002982 group: Z_Notation group: relation
+ \\<Zhide> code: 0x0029F9 group: Z_Notation group: operator
+ \\<Zcat> code: 0x002040 group: Z_Notation group: operator
+ \\<Zinbag> code: 0x0022FF group: Z_Notation group: relation
+ \\<Zprime> code: 0x002032 group: Z_Notation group: punctuation
+ \\<hole> code: 0x002311
+ \\<newline> code: 0x0023ce
+ \\<comment> code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^latex> group: document argument: cartouche
+ \\<^marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<checkmark> code: 0x002713
+ \\<crossmark> code: 0x002717
+ \\<open> code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: <<
+ \\<close> code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >>
+ \\<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^undefined> code: 0x002756 font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^noindent> code: 0x0021e4 group: document font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^smallskip> code: 0x002508 group: document font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^medskip> code: 0x002509 group: document font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^bigskip> code: 0x002501 group: document font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^item> code: 0x0025aa group: document font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^enum> code: 0x0025b8 group: document font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^descr> code: 0x0027a7 group: document font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^footnote> code: 0x00204b group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^verbatim> code: 0x0025a9 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^theory_text> code: 0x002b1a group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^emph> code: 0x002217 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^bold> code: 0x002759 group: control argument: cartouche group: document font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^sub> code: 0x0021e9 group: control font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^sup> code: 0x0021e7 group: control font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^bsub> code: 0x0021d8 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_(
+ \\<^esub> code: 0x0021d9 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_)
+ \\<^bsup> code: 0x0021d7 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^(
+ \\<^esup> code: 0x0021d6 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^)
+ \\<^file> code: 0x01F5CF group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^dir> code: 0x01F5C0 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^url> code: 0x01F310 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^doc> code: 0x01F4D3 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+ \\<^assert>
+ \\<^binding> argument: cartouche
+ \\<^bundle> argument: cartouche
+ \\<^can> argument: cartouche
+ \\<^class> argument: cartouche
+ \\<^class_syntax> argument: cartouche
+ \\<^command_keyword> argument: cartouche
+ \\<^const> argument: cartouche
+ \\<^const_abbrev> argument: cartouche
+ \\<^const_name> argument: cartouche
+ \\<^const_syntax> argument: cartouche
+ \\<^context>
+ \\<^cprop> argument: cartouche
+ \\<^cterm> argument: cartouche
+ \\<^ctyp> argument: cartouche
+ \\<^instantiate> argument: cartouche
+ \\<^keyword> argument: cartouche
+ \\<^locale> argument: cartouche
+ \\<^make_judgment>
+ \\<^dest_judgment>
+ \\<^make_string>
+ \\<^method> argument: cartouche
+ \\<^named_theorems> argument: cartouche
+ \\<^nonterminal> argument: cartouche
+ \\<^path> argument: cartouche
+ \\<^path_binding> argument: cartouche
+ \\<^plugin> argument: cartouche
+ \\<^print>
+ \\<^prop> argument: cartouche
+ \\<^bash_function> argument: cartouche
+ \\<^scala> argument: cartouche
+ \\<^scala_function> argument: cartouche
+ \\<^scala_method> argument: cartouche
+ \\<^scala_object> argument: cartouche
+ \\<^scala_thread> argument: cartouche
+ \\<^scala_type> argument: cartouche
+ \\<^session> argument: cartouche
+ \\<^simproc> argument: cartouche
+ \\<^simproc_setup> argument: cartouche
+ \\<^sort> argument: cartouche
+ \\<^syntax_const> argument: cartouche
+ \\<^system_option> argument: cartouche
+ \\<^term> argument: cartouche
+ \\<^theory> argument: cartouche
+ \\<^theory_context> argument: cartouche
+ \\<^tool> argument: cartouche
+ \\<^try> argument: cartouche
+ \\<^tvar> argument: cartouche
+ \\<^typ> argument: cartouche
+ \\<^type_abbrev> argument: cartouche
+ \\<^type_name> argument: cartouche
+ \\<^type_syntax> argument: cartouche
+ \\<^var> argument: cartouche
+ \\<^oracle_name> argument: cartouche
+ \\<^Const> argument: cartouche
+ \\<^Const_> argument: cartouche
+ \\<^Const_fn> argument: cartouche
+ \\<^Type> argument: cartouche
+ \\<^Type_fn> argument: cartouche
+ \\<^code> argument: cartouche
+ \\<^computation> argument: cartouche
+ \\<^computation_conv> argument: cartouche
+ \\<^computation_check> argument: cartouche
+ \\<^if_linux> argument: cartouche
+ \\<^if_macos> argument: cartouche
+ \\<^if_windows> argument: cartouche
+ \\<^if_unix> argument: cartouche
+ \\<^if_none> argument: cartouche
+ \\<^cite> argument: cartouche
+ \\<^nocite> argument: cartouche
+ \\<^citet> argument: cartouche
+ \\<^citep> argument: cartouche
+ `
-const symbols = symbols_file.matchAll(/\\<(\w+)>\s*code:\s0x([a-f0-9]+)\s/g).toArray()
+ const symbols = symbols_file.matchAll(/\\<(\w+)>\s*code:\s0x([a-f0-9]+)\s/g).toArray()
-function fmap(node) {
- if (node.nodeType === Node.TEXT_NODE) {
- node.data = node.data.replaceAll(/\\<(\w+)>/g, (match, group) => {
+ function fmap(node) {
+ if (node.nodeType === Node.TEXT_NODE) {
+ node.data = node.data.replaceAll(/\\<(\w+)>/g, (match, group) => {
- let code = symbols.find((sym) => sym[1] == group)[2]
- return String.fromCodePoint(parseInt(code, 16))
- });
- // TODO: call external? do inside JS?
- } else if (node.nodeType === Node.ELEMENT_NODE) {
- for (const child of node.childNodes) {
- fmap(child);
- }
- }
+ let code = symbols.find((sym) => sym[1] == group)[2]
+ return String.fromCodePoint(parseInt(code, 16))
+ });
+ // TODO: call external? do inside JS?
+ } else if (node.nodeType === Node.ELEMENT_NODE) {
+ for (const child of node.childNodes) {
+ fmap(child);
+ }
+ }
+ }
}
fmap(document.body);
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-09 19:16:39 +0000