diff options
author | Hans Hagen <pragma@wxs.nl> | 2020-07-30 17:51:33 +0200 |
---|---|---|
committer | Context Git Mirror Bot <phg@phi-gamma.net> | 2020-07-30 17:51:33 +0200 |
commit | 4619c6e66ef47e8e4953142a5c65467a6b0a2c01 (patch) | |
tree | 68b96931ee0c1373695ef0a0f85d1c6433febc45 /scripts | |
parent | 54af717a5c864e61d2ccd773457af149a90d900a (diff) | |
download | context-4619c6e66ef47e8e4953142a5c65467a6b0a2c01.tar.gz |
2020-07-30 16:52:00
Diffstat (limited to 'scripts')
-rw-r--r-- | scripts/context/lua/mtx-interface.lua | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/scripts/context/lua/mtx-interface.lua b/scripts/context/lua/mtx-interface.lua index 85ccb3ca0..0d3f05f7d 100644 --- a/scripts/context/lua/mtx-interface.lua +++ b/scripts/context/lua/mtx-interface.lua @@ -36,6 +36,7 @@ local helpinfo = [[ <flag name="raw"><short>report commands to the console</short></flag> <flag name="check"><short>generate check file</short></flag> <flag name="meaning"><short>report the mening of commands</short></flag> + <flag name="tokens"><short>show the internal representation of commands</short></flag> </subcategory> <subcategory> <flag name="toutf"><short>replace named characters by utf</short></flag> @@ -690,6 +691,26 @@ function scripts.interface.meaning() end end +function scripts.interface.tokens() + local runner = "mtxrun --silent --script context --extra=meaning --tokens --once --noconsole --nostatistics" + local pattern = environment.arguments.pattern + local files = environment.files + if type(pattern) == "string" then + runner = runner .. ' --pattern="' .. pattern .. '"' + elseif files and #files > 0 then + for i=1,#files do + runner = runner .. ' "' .. files[i] .. '"' + end + else + return + end + local r = os.resultof(runner) + if type(r) == "string" then + r = gsub(r,"^.-(tokens%s+>)","\n%1") + print(r) + end +end + local ea = environment.argument if ea("mkii") then @@ -698,6 +719,8 @@ elseif ea("preprocess") then scripts.interface.preprocess() elseif ea("meaning") then scripts.interface.meaning() +elseif ea("tokens") then + scripts.interface.tokens() elseif ea("toutf") then scripts.interface.toutf() elseif ea("bidi") then |