search

banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link

QuickLaTeX backend howto? #127

Open pnlph opened 4 years ago

pnlph commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

Does the issue #agda/agda#4507 help?

banacorn commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

Yes that would be possible!