Email Gateway (Aug 22 2022 at 20:50): Email Gateway (Aug 22 2022 at 20:50):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
When an interpretation with quoted parameters appears in the Isar source, e.g.:
interpretation foo "x y" z
in the LaTeX output there are no delimiters to separate the quoted parameter
from the others, so the output appears like:
interpretation foo x y z
which is ambiguous to the human reader. It is not clear that there is a way
to rectify this at the source level and I am in any case hesitant to try to
hack my source to work around something that seems to be an issue with
document processing. I would think that the system should determine that the
piece of inner syntax "x y" ought to be parenthesized in the document output,
in order to remove ambiguity.
Email Gateway (Aug 22 2022 at 20:50):From: Peter Gammie <peteg42@gmail.com>
Eugene,
As I remarked to you off-list, I think you’re best off using cartouches/guillemots everywhere you can these days.
However if you really do prefer to use symbols that are marked on your keyboard, Section 4.2.2 “General Options” (in Chapter 4 “Document Preparation”) suggests you might have some luck with the “quotes” option. I’d suggest you try adding that in a ROOT file — see the ones in the Isabelle distribution and/or the AFP for examples of the syntax. Note the caveat that this option may yet get trumped by LaTeX styling.
Seeing as the absence of quotes seems to work OK elsewhere, you might instead adopt something like:
interpretation foo
“x y"
z
cheers,
peter
Last updated: Apr 26 2024 at 16:20 UTC