QuickLaTeX backend howto?

[pnlph]

Hi,

is it possible from the Atom's agda-mode to access the QuickLaTeX backend to load a scope-checked version of the code?

[banacorn]

Hmm, I don't know.

First I tried agda --latex somefile.lagda in the terminal (without the --only-scope-checking flag). It said it typed checked the file, but then in the next line it failed with

kpsewhich: readCreateProcessWithExitCode: runInteractiveProcess:
exec: does not exist (No such file or directory)

Am I doing this right?

[pnlph]

Does the issue #agda/agda#4507 help?

[banacorn]

Thanks, found it!

https://github.com/agda/agda/blob/8c30a29fd73f4b19f2866f31712be102929dbfe5/src/full/Agda/Interaction/Base.hs#L407-L413

So it turned out to be a backend itself, and it's not available from the Atom's agda-mode yet. It shouldn't be difficult to add a new backend option to the settings, but perhaps we need a new field for specifying arguments?

[pnlph]

Would this be available as a keybinding? Maybe it is also an option not having QuickLaTeX as a setting, because otherwise to scope check and then load the file, one has to:

1. change the setting Backend to QuickLaTeX
2. use the keybinding to scope check
3. change the setting back to GHC
4. C-c C-l

It would be better that when using the keybinding of the scope check, one has not to change the backend in settings, is this possible?

[banacorn]

Yes that would be possible!