[isabelle] Quoted parameters to interpretation in LaTeX output



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.






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