Julian Berman (Dec 21 2020 at 17:58):
If anyone else likes/uses
bat (https://github.com/sharkdp/bat/ -- a
cat replacement), it was pretty easy to add Lean syntax support to it. The file is here: https://gist.github.com/Julian/062e5ae6a6a5edfea23f8c89a7ff5d41 which was just converted from the vscode-lean file. Stick it in
$(bat --config-dir)/syntaxes, run
bat cache --build and yeah should work then. Trying to see if a PR to bat would succeed but will see if it meets their inclusion criteria.
Kevin Buzzard (Dec 21 2020 at 19:05):
What does it _do_? A clueless mathematician.
Julian Berman (Dec 21 2020 at 19:09):
cat is a program whose function is essentially "print the contents of a file" (technically I'm lying, its real purpose is "conCATenate" a bunch of files together, but everyone uses it essentially for the former).
cat but with modernities like "highlight the file you outputted". Basically you use either one when you want to view stuff and aren't sitting inside an editor already (or when say, you are piping outputs from some commands to each other, which seems a bit less likely in this case).
Julian Berman (Jan 02 2021 at 15:25):
This got merged, yay: https://github.com/sharkdp/bat/pull/1446
Last updated: May 17 2021 at 22:15 UTC