1
0
mirror of synced 2026-03-21 00:58:00 +00:00
Files
Interlisp.medley/library
Matt Heffron 08a1d79265 If CADR of a TEDIT.ABBREVS entry is LITATOM that can CHARCODE.DECODE (i.e., it's on CHARACTERNAMES), use it.
Clear the TEdit prompt window if \TEDIT.ABBREV.EXPAND finds an expansion in TEDIT.ABBREVS.

"=" is duplicated as an expansion KEY, so modified TEDIT.ABBREVS entry:
("=" "357,121")
to
("lra" "357,121"  ; U+21C6 Leftwards Arrow Over Rightwards Arrow ("lra" is "left-right-arrow")
                )
because "=" is also the KEY in entry:
("=" NONBREAKING-HYPHEN)
which was never seen as a possibility (the above was earlier in the ALIST).
(This change exposed the issue with LITATOM as CADR of entry.)

Cleaned up some comments, typos. Added a few more TEDIT.ABBREVS entries.
2025-12-01 20:52:27 -08:00
..
2025-02-15 17:53:46 -08:00
2025-09-25 08:14:56 +02:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2021-04-28 15:36:03 -07:00
2021-04-28 15:36:03 -07:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2021-04-28 15:36:03 -07:00
2020-11-15 19:22:14 -08:00
2021-04-28 15:36:03 -07:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2021-04-28 15:36:03 -07:00
2020-11-15 19:22:14 -08:00
2021-03-15 13:04:02 -07:00
2020-11-15 19:22:14 -08:00
2021-04-28 15:36:03 -07:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2021-04-28 15:36:03 -07:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2021-04-28 15:36:03 -07:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2023-01-16 00:36:39 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2020-11-15 19:22:14 -08:00
2021-03-10 13:59:38 -08:00
2020-11-15 19:22:14 -08:00