Re: [isabelle] Newlines in antiquotation output


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:

(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.



On 06/23/2012 05:44 AM, Daniel Schoepe wrote:

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

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

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.


theory Test

definition double :: "nat option \<Rightarrow> nat option" where
  "double m \<equiv> do {
    x \<leftarrow> m;
    let d = x*2;
    Some d

thm double_def
thm (do_notation) double_def
text {* at {thm [display,margin=40,mode=do_notation] double_def}*}

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