2011-06-19 wenzelm discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);
2011-06-19 wenzelm added glyphs 21e0..21e4, 21e6..21e9, 2759 from DejaVuSansMono;
2011-06-19 wenzelm names for control symbols without "^", which is relevant for completion;
2011-06-19 wenzelm some unicode chars for special control symbols;
2011-06-18 wenzelm tuned;
2011-06-18 wenzelm tuned markup;
Loading...
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip