[isabelle] Newlines in antiquotation output



Hi,

I was wondering if there was a way to have more fine-grained control
over how newlines are inserted when using antiquotations:
When using something like @{thm foo} (or @{thm foo_def}) in my case,
no newlines are inserted at all. This can be corrected by
using [display] as an option to the antiquotation, but this causes
the newlines to be inserted at places that seem to be chosen
automatically.

This result is not always ideal: In my specific case, I'm trying to
get nice-looking representation of terms in a programming language whose
terms are represented by an Isabelle data type with some infix
annotations. For example, I'd like a term like the following to be
printed with linebreaks at the same position as in the Isabelle/HOL
source.

definition foo :: Stmt
  where "foo =
x <- 1;
y <- 2;
z <- x + y"

(where -> and ; are infix notations for constructors of Stmt)

I'd like to keep these definitions separate from the place where I am
using the antiquotation, so putting the definition in the place of the
antiquotation is not an ideal solution for me. Of course, I could copy
the generated latex output into my document manually, but this is
horrible in terms of maintainability. Using some perl to automate this
may be an option, but I'm hoping that there's a more elegant way.

Regards,
Daniel





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