diff options
author | Hans Hagen <pragma@wxs.nl> | 2022-07-06 22:05:18 +0200 |
---|---|---|
committer | Context Git Mirror Bot <phg@phi-gamma.net> | 2022-07-06 22:05:18 +0200 |
commit | 82c674fdcf5bcff4ad0dc0936d638fc729145616 (patch) | |
tree | 6ab4ee4417aa22180cd5b3c50ede6a031f8ce3f9 /doc/context/sources/general/manuals/luametatex/luametatex-differences.tex | |
parent | 3a55e11c7295abf8f2dfe5e9d1c8b153f4518824 (diff) | |
download | context-82c674fdcf5bcff4ad0dc0936d638fc729145616.tar.gz |
2022-07-06 21:35:00
Diffstat (limited to 'doc/context/sources/general/manuals/luametatex/luametatex-differences.tex')
-rw-r--r-- | doc/context/sources/general/manuals/luametatex/luametatex-differences.tex | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/doc/context/sources/general/manuals/luametatex/luametatex-differences.tex b/doc/context/sources/general/manuals/luametatex/luametatex-differences.tex index 3da557f40..8dcd2f2d1 100644 --- a/doc/context/sources/general/manuals/luametatex/luametatex-differences.tex +++ b/doc/context/sources/general/manuals/luametatex/luametatex-differences.tex @@ -279,6 +279,19 @@ end if luatex and luametatex then + local match = string.match + + local index = structures.registers.collected and structures.registers.collected.luatexindex + local found = { } + + if index then + local data = index.entries + for i=1,#data do + found[match(data[i].list[1][1],"\\tex%s*{(.-)}") or ""] = true + end + -- inspect(found) + end + luatex = table.tohash(luatex) luametatex = table.tohash(luametatex) @@ -291,6 +304,9 @@ if luatex and luametatex then context.startcolumns { n = 2 } for k, v in table.sortedhash(luatex) do if not luametatex[k] then + if not found[k] then + context.dontleavehmode() + end context.type(k) context.crlf() end @@ -307,6 +323,10 @@ if luatex and luametatex then context.startcolumns { n = 2 } for k, v in table.sortedhash(luametatex) do if not luatex[k] then + if not found[k] then + context.dontleavehmode() + context.llap("\\infofont[todo] ") + end context.type(k) context.crlf() end |