Email Gateway (May 23 2026 at 00:22): Email Gateway (May 23 2026 at 00:22):From: Andras Salamon <cl-isabelle-users@lists.cam.ac.uk>
I notice that @{thm[source] X} makes clickable hyperlinks in jEdit/VSCode but not in the generated PDF.
In text blocks, @{thm[source] X} renders in the PDF as static \mbox{\isa{...}} with no \hyperlink, even though pdfsetup.sty loads hyperref by default. So the name is just text, and moreover does not get wrapped because of how the macro is expanded. File "$ISABELLE_HOME/src/Doc/antiquote_setup.ML" has relevant \hyperlink/\hypertarget machinery but it only applies to Doc/ and the standard @{thm} conversion don't use this approach.
On 2021-01-01 (in isabelle-dev thread "Incoherent use of file name hoare_syntax.ML", Message-ID <10e1e928-136a-24fc-e0ae-25d6ae34393e@sketis.net>), Makarius wrote:
At a later stage, I should probably merge ideas from
"$ISABELLE_HOME/src/Doc/antiquote_setup.ML" back into more
official antiquotations in Isabelle/Pure.
Is now a reasonable such "later stage"? I would be happy to prepare a patch as an opt-in path (for instance \isabellestyle{linked} or similar) if this would be useful. I saw comments in the mailing list archives that seem to indicate that the TeX document output is a low priority so I am posting first.
András Salamon
Last updated: May 23 2026 at 03:31 UTC