Re: [isabelle] Quoted parameters to interpretation in LaTeX output


> On 27 Oct 2019, at 01:10, Eugene W. Stark <isabelle-users at> wrote:
> 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.

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"



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.