diff options
| author | terru | 2026-06-15 23:57:03 +0200 |
|---|---|---|
| committer | terru | 2026-06-16 12:00:46 +0200 |
| commit | 7dba866d6a42bafb39455d853ac6672cc91e0132 (patch) | |
| tree | dd78586a4f006e0045c978a7d0172adf8b2919d3 | |
simple clobbered-together implementation
| -rw-r--r-- | isabelle_new_embed.svg | 478 | ||||
| -rw-r--r-- | manifest.json | 24 | ||||
| -rw-r--r-- | src/background.html | 4 | ||||
| -rw-r--r-- | src/background.js | 25 | ||||
| -rw-r--r-- | src/message-unescape.js | 543 | ||||
| -rw-r--r-- | src/popup.js | 569 |
6 files changed, 1643 insertions, 0 deletions
diff --git a/isabelle_new_embed.svg b/isabelle_new_embed.svg new file mode 100644 index 0000000..a03abf7 --- /dev/null +++ b/isabelle_new_embed.svg @@ -0,0 +1,478 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="582.80566" + height="518.08588" + id="svg13549" + version="1.1" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="isabelle_new_embed.svg" + inkscape:export-filename="/home/manuel/Pictures/isabelle_logo/isabelle.png" + inkscape:export-xdpi="11.484688" + inkscape:export-ydpi="11.484688" + xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape" + xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd" + xmlns="http://www.w3.org/2000/svg" + xmlns:svg="http://www.w3.org/2000/svg" + xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" + xmlns:cc="http://creativecommons.org/ns#" + xmlns:dc="http://purl.org/dc/elements/1.1/"> + <defs + id="defs13551" /> + <sodipodi:namedview + id="base" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:pageopacity="0.0" + inkscape:pageshadow="2" + inkscape:zoom="1.4" + inkscape:cx="423.92857" + inkscape:cy="222.14286" + inkscape:document-units="px" + inkscape:current-layer="layer1" + showgrid="false" + inkscape:window-width="3840" + inkscape:window-height="2096" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + fit-margin-top="0" + fit-margin-left="0" + fit-margin-right="0" + fit-margin-bottom="0" + inkscape:showpageshadow="0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" /> + <metadata + id="metadata13554"> + <rdf:RDF> + <cc:Work + rdf:about=""> + <dc:format>image/svg+xml</dc:format> + <dc:type + rdf:resource="http://purl.org/dc/dcmitype/StillImage" /> + </cc:Work> + </rdf:RDF> + </metadata> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + transform="translate(-83.035087,-277.12837)"> + <path + style="fill:#fff000;fill-opacity:1;stroke:none" + d="m 512.3913,390.68749 91.71878,40.19475 -60.65321,53.65516 -59.69976,-27.07561 -0.50567,-43.67372 z" + id="rect9114-6-7-2" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cccccc" /> + <path + style="fill:#f89c0e;fill-opacity:1;stroke:none" + d="m 603.33647,430.54925 -59.78421,52.28831 v 95.51943 l 8.14537,1.50967 49.15192,-47.24787 z" + id="rect8567-7-3-9-7-4" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cccccc" /> + <path + style="fill:#fff000;fill-opacity:1;stroke:none" + d="m 397.0725,345.95698 86.51471,39.0796 -57.47673,53.00299 -92.86147,-39.92919 z" + id="rect9114-6-7" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccc" /> + <path + style="fill:#fff000;fill-opacity:1;stroke:none" + d="m 414.30565,494.34789 81.95057,36.45028 -65.19735,57.78102 -84.35231,-37.61041 z" + id="rect9114-6" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccc" /> + <path + style="fill:#f89c0e;fill-opacity:1;stroke:none" + d="m 482.31356,385.69483 -56.55822,51.47336 -0.21474,95.72372 23.0141,-23.23313 33.75886,-28.21361 z" + id="rect8567-7-3-9-7" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cccccc" /> + <path + style="fill:#fbc707;fill-opacity:1;stroke:none" + d="m 333.48247,395.51544 92.64083,41.25393 v 61.22994 l -0.66495,37.52631 -41.77518,-22.35044 -48.79886,-18.75529 z" + id="rect8567-9-3" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccc" /> + <path + style="fill:#f89c0e;fill-opacity:1;stroke:none" + d="m 496.63662,530.3642 -65.65114,58.08677 -0.7123,95.48173 65.85903,-55.84978 z" + id="rect8567-7-3-9" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccc" /> + <path + style="fill:#fbc707;fill-opacity:1;stroke:none" + d="m 346.74794,549.57322 84.28767,38.83562 v 95.22807 l -85.27894,-37.81253 z" + id="rect8567-9" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccc" /> + <path + style="fill:#d7705a;fill-opacity:1;stroke:none" + d="m 483.94324,478.4691 -0.36119,-19.61016 8.05958,2.17134 49.97968,25.31226 -48.53859,43.91141 -45.23677,-21.36756 z" + id="rect8567-7-0-2-5" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccc" /> + <path + style="fill:#be161c;fill-opacity:1;stroke:none" + d="m 541.25576,484.48998 -48.57784,44.28385 2.96068,1.01572 2.3293,81.87701 43.34431,-34.48218 z" + id="rect8567-7-3-2-6-8" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cccccc" /> + <path + style="fill:#d7705a;fill-opacity:1;stroke:none" + d="m 603.4907,529.34166 -0.44259,-23.97905 61.27326,27.17777 -59.29138,56.05874 -40.50555,-20.14094 z" + id="rect8567-7-0-2-9" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cccccc" /> + <path + style="fill:#be161c;fill-opacity:1;stroke:none" + d="m 661.57067,532.19333 -58.76819,52.39378 -0.12393,99.76805 58.58929,-51.82991 z" + id="rect8567-7-3-2-6" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccc" /> + <path + style="fill:#ce4e33;fill-opacity:1;stroke:none" + d="m 540.65976,577.05074 8.0486,3.19032 16.06614,-14.70942 38.49858,19.13014 v 98.58304 C 574.84975,666.94288 582.7842,674.77548 554.0064,659.10491 l -1.15528,-29.00904 -46.91916,-22.99464 z" + id="rect8567-7-0-8" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccccc" /> + <path + style="fill:none;stroke:#940808;stroke-width:5.26672;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 354.97642,779.86311 0.0472,-111.78758" + id="path14272-8-5-2" + inkscape:connector-curvature="0" + transform="matrix(1.0680649,0.03325035,4.5061323e-4,0.84385781,224.28481,9.9317178)" + sodipodi:nodetypes="cc" /> + <g + aria-label="α" + transform="matrix(0.94592587,0.48665862,0,1.0571653,0,0)" + id="text4644-9-3" + style="line-height:0%;font-family:'TeX Gyre Pagella';-inkscape-font-specification:'TeX Gyre Pagella';letter-spacing:0px;word-spacing:0px"> + <path + d="m 565.5018,319.49596 c 0.44505,2.44777 2.22525,5.71148 4.00545,5.71148 3.04117,0 5.26642,-1.48351 7.34332,-3.18953 2.81865,-2.6703 5.71148,-6.00818 7.7142,-8.6043 2.22525,7.7142 5.26643,11.79383 8.23343,11.79383 1.70602,0 3.8571,-1.26098 6.08235,-3.41206 l 3.2637,-3.2637 -0.96428,-1.40932 c -2.44777,2.29942 -4.22797,2.89282 -5.48895,2.89282 -1.1868,0 -2.15107,-0.22252 -3.18952,-1.63185 -0.96428,-1.40932 -2.44778,-4.52467 -3.18953,-6.74992 l -1.1868,-3.48623 c 1.85438,-2.967 3.5604,-6.2307 4.37633,-7.86255 0.81592,-1.55767 2.967,-6.00817 3.11535,-7.49167 -0.5934,-0.81593 -1.03845,-1.4835 -1.63185,-2.59613 -0.2967,-0.14835 -0.96428,-0.37087 -1.26098,-0.51922 -0.74175,6.15652 -1.40932,8.23342 -3.48622,12.60975 -0.22253,0.44505 -1.1868,2.29942 -1.85438,3.5604 l -4.59885,-13.57403 c -1.26097,-3.33787 -3.48622,-3.63457 -5.11807,-3.63457 -1.70603,0.0742 -4.07963,1.33515 -6.2307,3.63457 -1.63185,1.63185 -2.74448,3.5604 -3.70875,5.85983 -2.29943,6.60157 -3.2637,15.4284 -2.22525,21.3624 z m 5.48895,-2.44778 c -0.81593,-4.7472 -0.96428,-12.7581 0.51922,-18.91462 0.5934,-2.44778 2.15108,-4.59885 3.8571,-4.59885 2.29943,0 3.33788,1.33515 4.37633,4.59885 l 4.07962,12.98062 c -1.7802,2.52195 -3.63457,4.7472 -5.3406,6.30488 -2.0769,1.92855 -4.1538,2.59612 -5.56312,2.59612 -0.96428,0 -1.55768,-1.03845 -1.92855,-2.967 z" + style="font-size:74.175px;line-height:1.25" + id="path641" /> + </g> + <path + style="fill:#d7705a;fill-opacity:1;stroke:none" + d="m 496.63373,624.56756 1.21588,-12.42574 8.76049,-4.48739 48.05216,23.73519 -58.17622,59.15639 -45.08643,-26.92724 z" + id="rect8567-7-0-2" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccc" /> + <path + style="fill:#be161c;fill-opacity:1;stroke:none" + d="m 553.18646,629.34 -57.03349,51.1151 -0.61953,101.77726 58.7044,-57.10655 z" + id="rect8567-7-3-2" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccc" /> + <path + style="fill:#ce4e33;fill-opacity:1;stroke:none" + d="m 404.19947,672.19261 26.52971,10.95712 24.13185,-23.77283 41.65271,20.72481 v 101.11612 l -92.31169,-42.46424 z" + id="rect8567-7-0" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccc" /> + <path + style="fill:none;stroke:#9f2929;stroke-width:5.26672;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 354.97642,779.86311 0.0472,-111.78758" + id="path14272-8-5" + inkscape:connector-curvature="0" + transform="matrix(1.0680649,0.03325035,4.5061323e-4,0.84385781,116.76073,107.66685)" + sodipodi:nodetypes="cc" /> + <path + style="fill:#c8bee4;fill-opacity:1;stroke:none" + d="m 316.20218,451.80568 19.01993,8.73809 -0.97805,32.71122 49.2792,24.35913 -35.5362,36.01647 -95.17469,-47.06166 z" + id="rect9114-42" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccc" /> + <path + style="fill:#9c8dce;fill-opacity:1;stroke:none" + d="m 253.34907,507.37925 93.22789,41.79662 3.53906,55.2883 -3.39069,39.87938 -93.73675,-46.07157 z" + id="rect8567-8" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cccccc" /> + <path + style="fill:#c8bee4;fill-opacity:1;stroke:none" + d="m 299.1678,622.3081 48.00943,21.2396 1.91744,0.47137 33.88065,15.24447 -27.28695,26.33995 -88.86643,-37.42401 z" + id="rect9114-4" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccc" /> + <path + style="fill:#c8bee4;fill-opacity:1;stroke:none" + d="m 239.88726,553.543 13.91824,5.9578 -0.0852,34.1398 45.87878,23.02474 -30.76143,36.55824 -92.63387,-42.41805 z" + id="rect9114" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccc" /> + <path + style="fill:#9c8dce;fill-opacity:1;stroke:none" + d="m 270.52405,650.92321 84.13775,37.11673 -0.56821,102.0511 -85.22133,-39.53939 z" + id="rect8567-7" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccc" /> + <path + style="fill:#42386d;fill-opacity:1;stroke:none" + d="m 381.43462,662.44827 -27.01103,24.60672 -0.0631,101.38558 51.9085,-49.33761 -0.31241,-65.73475 z" + id="rect8567-7-3" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cccccc" /> + <path + style="fill:none;stroke:#593e6a;stroke-width:5.26672;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 354.97238,789.43979 0.0491,-116.28546" + id="path14272-8" + inkscape:connector-curvature="0" + transform="matrix(1.0680649,0.03325035,4.5061323e-4,0.84385781,-24.821129,108.52891)" + sodipodi:nodetypes="cc" /> + <path + style="fill:#9c8dce;fill-opacity:1;stroke:none" + d="m 175.45284,608.0143 93.37233,43.07259 -1.86472,94.6443 -13.15495,-1.23808 -78.35266,-41.80476 z" + id="rect8567" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cccccc" /> + <g + id="g4628" + transform="matrix(3.4157835,0,0,3.4157835,-543.12322,-747.81068)"> + <path + inkscape:connector-curvature="0" + id="path1648" + d="m 267.59375,390.94199 v 13.125 l 1.5,0.61602 v -13.125 z" + style="color:#000000;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:medium;line-height:normal;font-family:Sans;-inkscape-font-specification:Sans;text-indent:0;text-align:start;text-decoration:none;text-decoration-line:none;letter-spacing:normal;word-spacing:normal;text-transform:none;writing-mode:lr-tb;direction:ltr;baseline-shift:baseline;text-anchor:start;display:inline;overflow:visible;visibility:visible;fill:#231f20;fill-opacity:1;stroke:none;stroke-width:1.5;marker:none;enable-background:accumulate" /> + <path + sodipodi:nodetypes="ccccc" + inkscape:connector-curvature="0" + id="path1650" + d="m 268.96875,396.87058 -0.0156,1.68749 10.03125,4.75 -0.0156,-1.68749 z" + style="color:#000000;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:medium;line-height:normal;font-family:Sans;-inkscape-font-specification:Sans;text-indent:0;text-align:start;text-decoration:none;text-decoration-line:none;letter-spacing:normal;word-spacing:normal;text-transform:none;writing-mode:lr-tb;direction:ltr;baseline-shift:baseline;text-anchor:start;display:inline;overflow:visible;visibility:visible;fill:#231f20;fill-opacity:1;stroke:none;stroke-width:1.5;marker:none;enable-background:accumulate" /> + </g> + <g + id="g3888" + transform="translate(0,1.0714286)"> + <g + transform="translate(0,6.0609153)" + id="g3883"> + <g + id="g4632" + transform="matrix(2.8036733,0,0,2.8036733,-386.24828,-506.22786)"> + <path + sodipodi:nodetypes="ccccc" + inkscape:connector-curvature="0" + id="path1650-4" + d="m 236.6054,374.04877 -0.0173,1.87384 15.61542,7.426 -0.0173,-1.87384 z" + style="color:#000000;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:medium;line-height:normal;font-family:Sans;-inkscape-font-specification:Sans;text-indent:0;text-align:start;text-decoration:none;text-decoration-line:none;letter-spacing:normal;word-spacing:normal;text-transform:none;writing-mode:lr-tb;direction:ltr;baseline-shift:baseline;text-anchor:start;display:inline;overflow:visible;visibility:visible;fill:#231f20;fill-opacity:1;stroke:none;stroke-width:1.5;marker:none;enable-background:accumulate" /> + <path + sodipodi:nodetypes="ccccc" + inkscape:connector-curvature="0" + id="path1650-4-6" + d="m 236.6054,381.71767 -0.0173,1.87384 15.61542,7.426 -0.0173,-1.87384 z" + style="color:#000000;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:medium;line-height:normal;font-family:Sans;-inkscape-font-specification:Sans;text-indent:0;text-align:start;text-decoration:none;text-decoration-line:none;letter-spacing:normal;word-spacing:normal;text-transform:none;writing-mode:lr-tb;direction:ltr;baseline-shift:baseline;text-anchor:start;display:inline;overflow:visible;visibility:visible;fill:#231f20;fill-opacity:1;stroke:none;stroke-width:1.5;marker:none;enable-background:accumulate" /> + </g> + </g> + </g> + <text + xml:space="preserve" + style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none" + x="216.63254" + y="442.97165" + id="text3630-9" + transform="matrix(0.92733873,0.42936984,-0.14430118,1.0115413,0,0)" + inkscape:transform-center-y="3.0109114" + inkscape:transform-center-x="-0.21772724"><tspan + sodipodi:role="line" + id="tspan3632-2" + x="216.63254" + y="442.97165" + style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:74.2908px;line-height:1.25;font-family:'TeX Gyre Pagella';-inkscape-font-specification:'TeX Gyre Pagella'"> </tspan></text> + <g + aria-label="A" + transform="matrix(-1.0033569,-0.47426264,-0.01242653,-1.0025281,0,0)" + id="text4640" + style="line-height:0%;letter-spacing:0px;word-spacing:0px"> + <path + d="m -370.89152,-309.62559 -10.45269,28.34436 h 20.94354 z m -4.34893,-7.59155 h 8.73602 l 21.70651,56.95576 h -8.01119 l -5.1882,-14.61089 h -25.67396 l -5.18821,14.61089 h -8.12563 z" + style="font-size:78.1282px;line-height:1.25;font-family:'Droid Sans';-inkscape-font-specification:'Droid Sans'" + id="path638" /> + </g> + <g + aria-label="β" + transform="matrix(0.95142085,0.47582633,0.01207069,1.0570964,0,0)" + id="text4644" + style="line-height:0%;font-family:'TeX Gyre Pagella';-inkscape-font-specification:'TeX Gyre Pagella';letter-spacing:0px;word-spacing:0px"> + <path + d="m 309.77971,527.0366 0.26859,43.10947 1.14153,0.53719 c 1.67872,-0.53719 2.21591,-0.87294 4.16322,-1.14153 -0.60434,-5.97623 -1.61157,-13.56404 -1.41012,-18.80164 3.02169,1.47728 5.77479,2.08161 9.40082,2.08161 10.74379,0 18.06299,-7.38635 16.31713,-16.51857 -0.67149,-3.49174 -2.21591,-5.43905 -5.03615,-7.18492 -1.94732,-1.20867 -3.62603,-1.81301 -7.11777,-2.61879 l -0.0671,-0.33575 c 0,-0.87293 0.33574,-1.67872 1.20867,-3.08884 0.20145,-0.26859 0.47004,-0.67149 0.60434,-0.94008 3.55888,-5.2376 4.56611,-7.31921 3.89463,-11.01239 -0.73864,-3.69317 -4.23037,-6.78201 -7.8564,-6.78201 -2.8874,0 -7.58781,2.14875 -11.07954,5.1033 -3.49173,2.88739 -4.02892,5.23759 -4.16322,9.19937 z m 4.36466,13.89979 0.67149,-14.30268 c 0.20145,-6.78202 0.40289,-11.95247 0.60434,-13.42974 0.60434,-3.49173 3.22314,-5.50619 6.71487,-5.50619 3.49173,0 6.31198,2.3502 7.05061,5.77479 0.53719,2.95454 -0.20144,4.70041 -3.02169,9.93801 -1.67872,1.67871 -2.7531,2.55165 -5.64049,2.55165 -0.60434,0 -1.27583,0 -1.54442,-0.0671 -0.53719,-0.0671 -0.87293,-0.0671 -1.61157,-0.0671 l -0.67149,2.88739 0.53719,0.80579 c 2.41736,-0.87294 3.55888,-1.07438 5.2376,-1.07438 6.11053,0 10.13946,2.6188 11.21383,8.32644 0.80579,4.09607 -0.0671,8.12499 -2.41735,10.87808 -1.54442,1.94732 -3.82747,2.8874 -6.84917,2.8874 -5.30474,0 -9.13222,-2.7531 -10.00515,-7.18491 -0.0671,-0.67149 -0.20145,-1.34298 -0.2686,-2.41735 z" + style="font-size:67.1487px;line-height:1.25" + id="path644" /> + </g> + <g + aria-label="λ" + transform="matrix(0.94592587,0.48665862,0,1.0571653,0,0)" + id="text4644-9" + style="line-height:0%;font-family:'TeX Gyre Pagella';-inkscape-font-specification:'TeX Gyre Pagella';letter-spacing:0px;word-spacing:0px"> + <path + d="m 210.91093,558.61036 1.85438,1.63185 c 1.26097,-0.66757 2.29942,-1.03845 4.07962,-1.63185 3.93128,-11.20042 6.2307,-18.02452 13.0548,-30.11505 l 10.82955,29.44748 c 0.44505,1.26097 1.4835,2.0769 2.74448,2.0769 1.92855,0 4.4505,-1.63185 10.90373,-6.97245 l -0.96428,-1.33515 -1.7802,1.26097 c -2.00273,1.4835 -3.70875,2.22525 -4.37633,2.22525 -0.2967,0 -0.5934,0 -1.70602,-1.40932 -0.74175,-0.8901 -1.4835,-2.6703 -2.6703,-5.19225 l -9.64275,-25.88708 c -3.8571,-10.3845 -7.49168,-15.65093 -11.2746,-16.09598 -1.7802,1.63185 -4.52468,3.48623 -6.00818,4.52468 l 0.0742,1.7802 c 1.40932,-0.51923 3.5604,-1.40933 4.22797,-1.40933 2.0769,0 4.67303,3.33788 6.2307,7.64003 l 2.52195,6.89828 c -5.19225,8.0109 -15.1317,26.62882 -18.0987,32.56282 z" + style="font-size:74.175px;line-height:1.25" + id="path647" /> + </g> + <g + aria-label="→" + transform="matrix(0.94592587,0.43528282,0,1.0571653,0,0)" + id="text4644-8" + style="line-height:0%;font-family:'TeX Gyre Pagella';-inkscape-font-specification:'TeX Gyre Pagella';letter-spacing:0px;word-spacing:0px"> + <path + d="m 450.25327,478.53142 h 41.90079 c -2.41735,2.48451 -4.63326,5.17045 -6.64772,8.05785 0.73864,-0.1343 1.41012,-0.20145 2.14876,-0.20145 0.73863,0 1.41012,0.0672 2.14876,0.20145 3.42458,-3.76033 7.3192,-7.11776 11.48242,-10.07231 -4.16322,-2.95454 -8.05784,-6.31197 -11.48242,-10.0723 -0.73864,0.1343 -1.41013,0.20145 -2.14876,0.20145 -0.73864,0 -1.41012,-0.0672 -2.14876,-0.20145 2.01446,2.88739 4.23037,5.57334 6.64772,8.05784 h -41.90079 c 0.1343,0.67149 0.20145,1.34298 0.20145,2.01446 0,0.67149 -0.0672,1.34298 -0.20145,2.01446 z" + style="font-size:67.1487px;line-height:1.25" + id="path650" /> + </g> + <g + aria-label="Isabelle" + transform="matrix(0.69382762,-0.76328282,0.48011419,0.91310446,0,0)" + id="text1654" + style="line-height:0%"> + <path + d="m -181.66019,510.86905 q 0.59284,-7.2757 0.86231,-15.68317 0.32336,-8.40747 0.32336,-21.93487 0,-13.09626 -0.32336,-21.93488 -0.26947,-8.89252 -0.86231,-15.84485 2.37134,0.32337 4.74268,0.53894 2.42523,0.16169 4.85046,0.16169 2.42523,0 4.79657,-0.16169 2.37134,-0.21557 4.68878,-0.53894 -0.64672,7.06012 -0.97009,15.95264 -0.26947,8.89252 -0.26947,21.82709 0,14.06634 0.26947,22.41992 0.32337,8.29968 0.9162,15.19812 -2.64081,-0.26947 -5.01215,-0.37726 -2.31744,-0.16168 -4.41931,-0.16168 -2.20965,0 -4.58099,0.16168 -2.31744,0.10779 -5.01215,0.37726 z" + style="font-weight:bold;font-size:110.375px;line-height:1.25;font-family:'ZapfHumnst BT';-inkscape-font-specification:'ZapfHumnst BT';fill:#231f20" + id="path572" /> + <path + d="m -147.46411,495.72482 h 1.56293 q 1.7785,5.4433 5.49719,8.40747 3.77258,2.96418 8.73083,2.96418 3.93427,0 6.09003,-1.94019 2.15576,-1.94019 2.15576,-5.4433 0,-4.4732 -10.67102,-8.89251 -1.45514,-0.59284 -2.20965,-0.9162 -7.59906,-3.17975 -10.50934,-6.52118 -2.85639,-3.39533 -2.85639,-8.62305 0,-8.08411 5.4972,-13.04236 5.55108,-4.95825 14.71307,-4.95825 4.25763,0 8.19189,1.18567 3.93427,1.13177 7.70685,3.44922 -1.13177,2.53302 -1.94018,5.11993 -0.80841,2.58692 -1.29346,5.28162 h -1.07788 q -2.42523,-5.06604 -5.71277,-7.59906 -3.23364,-2.53302 -7.32959,-2.53302 -3.44922,0 -5.71277,1.94018 -2.20965,1.88629 -2.20965,4.90436 0,2.47913 1.61682,4.14984 1.61682,1.61682 7.76074,3.98816 12.01837,4.68878 14.98254,8.03021 3.01807,3.34143 3.01807,8.83863 0,8.40747 -5.82056,13.63519 -5.76666,5.17383 -15.14422,5.17383 -5.17383,0 -9.16199,-1.07788 -3.98816,-1.02399 -7.2757,-3.23365 0.26947,-1.99407 1.18567,-10.29376 z" + style="font-weight:bold;font-size:110.375px;line-height:1.25;font-family:'ZapfHumnst BT';-inkscape-font-specification:'ZapfHumnst BT';fill:#231f20" + id="path574" /> + <path + d="m -72.49865,503.91672 q -2.371337,3.98816 -6.251709,6.14392 -3.826477,2.15576 -8.67694,2.15576 -6.952332,0 -10.940491,-4.09595 -3.93427,-4.14984 -3.93427,-11.26385 0,-5.22772 2.802495,-8.62305 2.80249,-3.39532 8.784729,-5.3894 1.940185,-0.64673 5.60498,-1.77851 8.623047,-2.58691 11.802796,-4.74267 0.05389,-0.32337 0.05389,-0.70063 0.05389,-0.43115 0.05389,-1.18566 0,-5.01215 -2.856384,-7.97632 -2.856385,-2.96417 -7.59906,-2.96417 -3.718689,0 -6.79065,2.10186 -3.018066,2.10187 -5.60498,6.41339 -0.808411,-2.58691 -1.347351,-4.14984 -0.538941,-1.56292 -1.077881,-2.91028 4.904358,-4.25762 9.700927,-6.3056 4.79657,-2.10187 9.970398,-2.10187 9.916504,0 15.19812,4.581 5.335511,4.58099 5.335511,13.09625 v 0.53894 l -0.323365,19.24017 v 2.10187 q 0,6.73676 1.45514,8.67694 1.509033,1.88629 5.820556,1.88629 h 0.323365 v 2.7486 q -2.802491,1.18567 -5.820557,1.7785 -3.018066,0.64673 -5.766663,0.64673 -3.988159,0 -6.521179,-1.99408 -2.53302,-2.04797 -3.395325,-5.92834 z m -0.485046,-22.09656 q -7.652954,1.56293 -11.048279,4.74268 -3.395324,3.17974 -3.395324,8.83862 0,4.74267 1.724609,7.11401 1.724609,2.37134 5.119934,2.37134 3.664795,0 5.60498,-2.64081 1.99408,-2.64081 1.99408,-7.59906 z" + style="font-weight:bold;font-size:110.375px;line-height:1.25;font-family:'ZapfHumnst BT';-inkscape-font-specification:'ZapfHumnst BT';fill:#231f20" + id="path576" /> + <path + d="m -17.028576,463.28061 q -5.766662,0 -8.299683,5.17383 -2.479125,5.11993 -2.479125,17.46167 0,11.42553 2.317443,16.16821 2.317444,4.68878 7.706849,4.68878 5.87445,0 8.4074702,-5.28161 2.53302,-5.33551 2.53302,-18.00061 0,-11.04828 -2.3713379,-15.62928 -2.3174443,-4.58099 -7.8146363,-4.58099 z m -26.030823,47.58844 q 0.592835,-7.2218 0.862305,-16.92273 0.26947,-9.75482 0.26947,-24.4679 0,-14.71307 -0.26947,-24.414 -0.26947,-9.75482 -0.862305,-16.97662 2.748597,0.43115 4.634888,0.59283 1.940186,0.16169 3.664795,0.16169 1.724609,0 3.664795,-0.16169 1.994079,-0.21557 4.473205,-0.59283 -0.26947,5.06604 -0.431152,9.32367 -0.107788,4.20373 -0.107788,8.138 v 17.94672 q 3.018066,-3.55701 6.628967,-5.17383 3.610901,-1.67072 8.623047,-1.67072 9.6470339,0 15.3598024,7.06012 5.7127686,7.06012 5.7127686,19.0246 0,13.5274 -6.7906494,21.55762 -6.7367554,8.03021 -18.0545046,8.03021 -4.850464,0 -8.623047,-1.8324 -3.772583,-1.8324 -7.167907,-5.82056 -2.802491,1.34736 -5.173829,2.91028 -2.371337,1.50904 -4.419311,3.28754 z" + style="font-weight:bold;font-size:110.375px;line-height:1.25;font-family:'ZapfHumnst BT';-inkscape-font-specification:'ZapfHumnst BT';fill:#231f20" + id="path578" /> + <path + d="m 32.866235,484.62265 q 0,9.53925 4.527099,15.14423 4.580994,5.60498 12.287842,5.60498 3.826477,0 7.32959,-1.29346 3.503113,-1.29346 6.790649,-3.93427 l 1.077881,0.80842 -2.425232,6.2517 q -3.449218,2.42524 -8.138,3.71869 -4.634888,1.29346 -10.078186,1.29346 -12.880676,0 -20.210266,-7.59906 -7.275696,-7.59906 -7.275696,-21.01868 0,-12.07226 7.275696,-19.50964 7.275696,-7.43738 19.240173,-7.43738 11.371643,0 17.407776,6.3056 6.090027,6.30561 6.090027,18.1084 0,1.40125 -0.05389,2.15577 0,0.75451 -0.05389,1.34735 z m 0,-5.4433 h 18.701233 q 0,-0.59283 0.05389,-1.45514 0.05389,-0.9162 0.05389,-1.18567 0,-7.49127 -2.209656,-11.31775 -2.155762,-3.82647 -6.413391,-3.82647 -4.850464,0 -7.545166,4.36542 -2.640808,4.36541 -2.640808,12.44952 z" + style="font-weight:bold;font-size:110.375px;line-height:1.25;font-family:'ZapfHumnst BT';-inkscape-font-specification:'ZapfHumnst BT';fill:#231f20" + id="path580" /> + <path + d="m 76.59774,510.86905 q 0.431153,-9.32367 0.646729,-19.45575 0.215576,-10.13208 0.215576,-21.7193 0,-12.28784 -0.215576,-22.41992 -0.215576,-10.18598 -0.646729,-19.18628 2.640808,0.43115 4.5271,0.59283 1.886291,0.16169 3.664795,0.16169 1.778503,0 3.772583,-0.16169 1.994079,-0.21557 4.473205,-0.59283 -0.431152,9.32367 -0.646728,19.45575 -0.215576,10.13208 -0.215576,21.7193 0,12.28784 0.215576,22.47381 0.215576,10.13208 0.646728,19.13239 -1.832397,-0.37726 -3.880371,-0.53894 -2.047973,-0.21558 -4.257629,-0.21558 -2.209656,0 -4.25763,0.21558 -2.047973,0.16168 -4.042053,0.53894 z" + style="font-weight:bold;font-size:110.375px;line-height:1.25;font-family:'ZapfHumnst BT';-inkscape-font-specification:'ZapfHumnst BT';fill:#231f20" + id="path582" /> + <path + d="m 106.73016,510.86905 q 0.43115,-9.32367 0.64672,-19.45575 0.21558,-10.13208 0.21558,-21.7193 0,-12.28784 -0.21558,-22.41992 -0.21557,-10.18598 -0.64672,-19.18628 2.6408,0.43115 4.5271,0.59283 1.88629,0.16169 3.66479,0.16169 1.7785,0 3.77258,-0.16169 1.99408,-0.21557 4.47321,-0.59283 -0.43115,9.32367 -0.64673,19.45575 -0.21558,10.13208 -0.21558,21.7193 0,12.28784 0.21558,22.47381 0.21558,10.13208 0.64673,19.13239 -1.8324,-0.37726 -3.88037,-0.53894 -2.04798,-0.21558 -4.25763,-0.21558 -2.20966,0 -4.25763,0.21558 -2.04797,0.16168 -4.04205,0.53894 z" + style="font-weight:bold;font-size:110.375px;line-height:1.25;font-family:'ZapfHumnst BT';-inkscape-font-specification:'ZapfHumnst BT';fill:#231f20" + id="path584" /> + <path + d="m 149.31227,484.62265 q 0,9.53925 4.5271,15.14423 4.58099,5.60498 12.28784,5.60498 3.82648,0 7.32959,-1.29346 3.50312,-1.29346 6.79065,-3.93427 l 1.07788,0.80842 -2.42523,6.2517 q -3.44922,2.42524 -8.138,3.71869 -4.63489,1.29346 -10.07819,1.29346 -12.88067,0 -20.21026,-7.59906 -7.2757,-7.59906 -7.2757,-21.01868 0,-12.07226 7.2757,-19.50964 7.27569,-7.43738 19.24017,-7.43738 11.37164,0 17.40778,6.3056 6.09002,6.30561 6.09002,18.1084 0,1.40125 -0.0539,2.15577 0,0.75451 -0.0539,1.34735 z m 0,-5.4433 h 18.70123 q 0,-0.59283 0.0539,-1.45514 0.0539,-0.9162 0.0539,-1.18567 0,-7.49127 -2.20965,-11.31775 -2.15577,-3.82647 -6.41339,-3.82647 -4.85047,0 -7.54517,4.36542 -2.64081,4.36541 -2.64081,12.44952 z" + style="font-weight:bold;font-size:110.375px;line-height:1.25;font-family:'ZapfHumnst BT';-inkscape-font-specification:'ZapfHumnst BT';fill:#231f20" + id="path586" /> + </g> + <path + style="fill:none;stroke:#ebb11f;stroke-width:5.42158;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 354.97642,779.86311 0.0472,-111.78758" + id="path14272-8-8" + inkscape:connector-curvature="0" + transform="matrix(1.0680649,0.03137802,4.5061323e-4,0.79634018,52.296445,45.589981)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#ebb11f;stroke-width:6.50941;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 354.95192,837.92235 0.0717,-169.84682" + id="path14272-8-8-9" + inkscape:connector-curvature="0" + transform="matrix(1.0680649,0.02176674,4.5061323e-4,0.55241636,46.225016,60.238211)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#f6f69f;stroke-width:6.03389;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 355,779.86218 0.0147,-113.26655" + id="path14272-4-0" + inkscape:connector-curvature="0" + transform="matrix(-0.68013133,-0.69915023,0.52081234,-0.47423207,325.9157,1150.957)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#e9ddfc;stroke-width:5;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 380.87819,663.81103 -26.36395,24.41941" + id="path14272-4" + inkscape:connector-curvature="0" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#e9ddfc;stroke-width:5.37005;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 355.01911,904.60038 355,668.07646" + id="path14272-1" + inkscape:connector-curvature="0" + transform="matrix(0.46724158,-0.97914515,0.73110264,0.32332687,-472.78971,743.30514)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#e9ddfc;stroke-width:5.0136;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 350.9947,778.5365 V 666.75078" + id="path14272-1-8" + inkscape:connector-curvature="0" + transform="matrix(0.49932689,-1.0511443,0.78130719,0.34710196,-439.69297,646.68794)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#f6f69f;stroke-width:6.03389;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 355,779.86218 V 668.07646" + id="path14272-4-0-8" + inkscape:connector-curvature="0" + transform="matrix(-0.68013133,-0.69915023,0.52081234,-0.47423207,435.88827,1049.1627)" /> + <path + style="fill:none;stroke:#f6f69f;stroke-width:6.32745;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 355,779.86218 0.13674,-112.35385" + id="path14272-4-0-1" + inkscape:connector-curvature="0" + transform="matrix(-0.64870168,-0.66658539,0.496745,-0.45214342,324.21149,975.44506)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#f6f69f;stroke-width:5.58442;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 355,779.86218 0.003,-113.40213" + id="path14272-1-8-0" + inkscape:connector-curvature="0" + transform="matrix(0.44991982,-0.94027428,0.70399892,0.3104912,-277.16301,678.31473)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#f6f69f;stroke-width:5.1577;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 355.12294,780.56223 355,668.07646" + id="path14272-1-8-0-5" + inkscape:connector-curvature="0" + transform="matrix(0.48582149,-1.0208367,0.76017501,0.33709398,-340.52398,536.3385)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#f4af92;stroke-width:12.1715;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 355,779.86218 0.0822,-114.26" + id="path14272-1-8-0-0" + inkscape:connector-curvature="0" + transform="matrix(0.23222996,-0.40349326,0.33248482,0.14898077,154.01474,708.1133)" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#f4af92;stroke-width:6.65085;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 355,779.86218 V 668.07646" + id="path14272-4-8" + inkscape:connector-curvature="0" + transform="matrix(-0.61829193,-0.63300976,0.47345866,-0.42936913,399.22409,1192.6629)" /> + <path + style="fill:none;stroke:#f4af92;stroke-width:13.5922;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 355,779.86218 V 668.07646" + id="path14272-1-8-0-0-7" + inkscape:connector-curvature="0" + transform="matrix(0.20957423,-0.35852802,0.30004849,0.13237837,294.8988,607.38216)" /> + <path + style="fill:none;stroke:#f4af92;stroke-width:6.65085;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 355,779.86218 V 668.07646" + id="path14272-4-8-0" + inkscape:connector-curvature="0" + transform="matrix(-0.61829193,-0.63300976,0.47345866,-0.42936913,506.74817,1094.9278)" /> + <path + style="fill:none;stroke:#f4af92;stroke-width:8.65263;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 355,779.86218 V 668.07646" + id="path14272-4-8-0-9" + inkscape:connector-curvature="0" + transform="matrix(-0.47589389,-0.48590517,0.36441699,-0.32958841,421.60388,918.00221)" /> + <path + id="path7649" + style="fill:none;stroke:#000000;stroke-width:2.49672;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="m 281.36237,419.41257 v 24.5231 l 32.90922,15.12153 20.75374,-18.71124 V 416.1035 m 17.09377,-55.02117 21.356,9.65374 -0.25,35.27102 -20.89285,18.51339 -17.30692,-8.41698 v -10.95495 l -17.7408,-8.10792 m -7.44988,-53.19425 -0.0524,-13.96278 9.88668,-9.82262 32.45019,14.79137 v 26.21926 l -0.0833,9.34489 -18.80608,17.30556 -3.0026,-1.34164 -12.94258,10.66021 -2.83247,2.56409 v 3.51844 l -23.3731,20.77037 -9.71662,-4.48096 -20.29799,-9.99116 -0.58548,-32.13418 14.23527,-12.60482 m 14.44143,6.2527 -32.67508,-14.40908 v -11.65867 l -3.5e-4,-22.98278 21.89097,-18.29019 31.33851,14.47705 v 11.82131 m -11.03913,32.66435 15.73738,7.26176 0.0442,29.78586 m -25.22721,-28.61266 20.60977,-19.26611 v -7.87957 l 20.39245,9.63592 v 32.89812 m -73.74654,-41.51306 -6.42507,-3.37242 -22.38393,20.24107 -0.0221,18.03453 m 53.7129,64.16513 -17.41086,19.00778 -31.32458,-14.91339 0.22321,-35.67058 11.59485,-10.57313 m 46.62849,22.0488 -63.46887,-30.26397 0.0449,-13.80064 -5.07612,-2.19199 -22.58035,19.87145 v 35.13298 l 33.96548,16.08314" + inkscape:connector-curvature="0" + sodipodi:nodetypes="ccccccccccccccccccccccccscccccccccccccccccccccccccccccccccc" + transform="matrix(2.8036733,0,0,2.8036733,-384.76141,-506.22786)" /> + <path + style="fill:none;stroke:#ff0000;stroke-width:0.2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" + d="M 83.392857,327.99353 283.75,416.56496" + id="path3815" + inkscape:connector-curvature="0" + transform="translate(83.035003,277.12812)" + sodipodi:nodetypes="cc" /> + </g> +</svg> diff --git a/manifest.json b/manifest.json new file mode 100644 index 0000000..dd6e7dd --- /dev/null +++ b/manifest.json @@ -0,0 +1,24 @@ +{ + "manifest_version": 2, + "version": "0.1", + "author": "terru", + "name": "Isabelle markup expander", + "description": "Parse Isabelle escape codes and replace them by unicode representation", + "browser_specific_settings": { + "gecko": { + "id": "messageDisplayScript@mv2.sample.extensions.thunderbird.net" + } + }, + "background": { + "page": "src/background.html" + }, + "message_display_action": { + "default_title": "Isabelle", + "default_icon": "isabelle_new_embed.svg" + }, + "permissions": [ + "messagesUpdate", + "messagesModify", + "messagesRead" + ] +} diff --git a/src/background.html b/src/background.html new file mode 100644 index 0000000..2e5e3d6 --- /dev/null +++ b/src/background.html @@ -0,0 +1,4 @@ +<!DOCTYPE html> +<html> + <script type="module" src="background.js"></script> +</html> diff --git a/src/background.js b/src/background.js new file mode 100644 index 0000000..3f40e88 --- /dev/null +++ b/src/background.js @@ -0,0 +1,25 @@ + +browser.messageDisplayAction.onClicked.addListener(async () => { + let tabs = await messenger.tabs.query({ active: true, currentWindow: true }); + + // taken from tutorial + for (let messageTab of tabs) { + // Make sure the tab is displaying a single message. The mail tab could also + // display a content page or multiple messages, which will cause an error. + if (messageTab.type == "mail") { + let messages = await browser.messageDisplay.getDisplayedMessages( + messageTab.id + ); + if (messages.length != 1) { + continue; + } + } + browser.tabs.executeScript(messageTab.id, { + file: "message-unescape.js" + }); + + } +}); + + +console.log("registered") diff --git a/src/message-unescape.js b/src/message-unescape.js new file mode 100644 index 0000000..39197c8 --- /dev/null +++ b/src/message-unescape.js @@ -0,0 +1,543 @@ + +// 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 + +\\<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() + + +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); + } + } +} + +fmap(document.body); diff --git a/src/popup.js b/src/popup.js new file mode 100644 index 0000000..0dae0b2 --- /dev/null +++ b/src/popup.js @@ -0,0 +1,569 @@ + +// 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 + +\\<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() + + +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); + } + } +} + +// The user clicked our button, get the active tab in the current window using +// the tabs API. +let tabs = await messenger.tabs.query({ active: true, currentWindow: true }); + +// Get the message currently displayed in the active tab, using the +// messageDisplay API. Note: This needs the messagesRead permission. +// The returned message is a MessageHeader object with the most relevant +// information. +let message = await messenger.messageDisplay.getDisplayedMessage(tabs[0].id); + +for (let messageTab of tabs) { + // Make sure the tab is displaying a single message. The mail tab could also + // display a content page or multiple messages, which will cause an error. + if (messageTab.type == "mail") { + let messages = await browser.messageDisplay.getDisplayedMessages( + messageTab.id + ); + if (messages.length != 1) { + continue; + } + } + browser.tabs.executeScript(messageTab.id, { + file: "message-unescape.js" + }); +} +// fmap(document.body); +//message.body.innerText = "hello"; |
