engrave region

AlexD97 commented

2022-12-05 17:21:27 +00:00

(Migrated from github.com)

Is it somehow possible to export only a region of the current buffer like in htmlize? And is it possible to prevent engrave-faces from creating a new temporary buffer/using a new mode (I would like to use engrave-faces in agda2-mode, not in org-mode).

tecosaur commented

2022-12-05 17:36:37 +00:00

(Migrated from github.com)

Not currently, but I think narrowing may work, which would make doing so fairly trivial.

With regard to running it using a temporary buffer, sure, you're just going to need to take care of that yourself. I'm not sure that complexity belongs in this package (but I'm open to further discussion).

Not currently, but I think narrowing may work, which would make doing so fairly trivial. With regard to running it using a temporary buffer, sure, you're just going to need to take care of that yourself. I'm not sure that complexity belongs in this package (but I'm open to further discussion).

AlexD97 commented

2022-12-05 21:20:48 +00:00

(Migrated from github.com)

The problem with org-mode-only is that agda does not play very well with org mode: there is no syntax highlighting in src blocks.
Since htmlize works well with any buffer I thought this might be the case here as well.

The problem with org-mode-only is that agda does not play very well with org mode: there is no syntax highlighting in src blocks. Since htmlize works well with any buffer I thought this might be the case here as well.

tecosaur commented

2023-01-15 08:07:24 +00:00

(Migrated from github.com)

Taking a look at this again, ti think it could be helpful to explain your use case a bit more.

AlexD97 commented

2023-01-19 10:48:05 +00:00

(Migrated from github.com)

I wanted to have the possibility to export regions of an Agda buffer to a latex file. The problem was/is that engrave-faces creates a new buffer where the syntax highlighting from Agda is lost. Moreover, I wanted to have the possibility to just export a snippet and not the whole file.

tecosaur commented

2023-01-19 11:17:57 +00:00

(Migrated from github.com)

Does narrow-to-region + engrave-faces-latex-buffer not work for you?

Does `narrow-to-region` + `engrave-faces-latex-buffer` not work for you?

AlexD97 commented

2023-01-19 11:24:01 +00:00

(Migrated from github.com)

Unfortunately not, since the syntax highlighting is somehow lost when invoking engrave-faces-latex-buffer.

Unfortunately not, since the syntax highlighting is somehow lost when invoking `engrave-faces-latex-buffer`.

tecosaur commented

2023-01-19 13:21:40 +00:00