Email Gateway (Aug 18 2022 at 20:10): Email Gateway (Aug 18 2022 at 20:10):From: Daniel Schoepe <daniel@schoepe.org>
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
Email Gateway (Aug 18 2022 at 20:11):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Hi,
you can read the section on Inner syntax of the Isabelle Reference
Manual (isabelle doc isar-ref). There it is described how to use mixfix
annotations (which can be installed just for certain output modes, e.g.,
like (latex)) to configure pretty printing. Something very similar to
your example is available as part of Monad_Syntax.thy from
Isabelle/HOL's library:
http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Monad_Syntax.html
(note that you have to use the output mode "do_notation" to actually
activate this syntax in your output).
For a full example consider the attached file.
cheers
chris
Test.thy
Email Gateway (Aug 18 2022 at 20:11):From: Daniel Schoepe <daniel@schoepe.org>
Hi Chris,
Thank you, that seems work nicely. I ended up defining the notations I
wanted myself instead of using do notation though, but the Monad_Syntax
theory is a nice example of how to do that.
Regards,
Daniel
Last updated: Apr 25 2024 at 04:18 UTC