*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Newlines in antiquotation output*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Sat, 23 Jun 2012 11:25:53 +0900*In-reply-to*: <87vcijcc0u.fsf@schoepe.localhost>*References*: <87vcijcc0u.fsf@schoepe.localhost>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:13.0) Gecko/20120605 Thunderbird/13.0

Hi,

http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Monad_Syntax.html

For a full example consider the attached file. cheers chris On 06/23/2012 05:44 AM, Daniel Schoepe wrote:

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

theory Test imports Main "~~/src/HOL/Library/Monad_Syntax" begin 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}*} end

**Follow-Ups**:**Re: [isabelle] Newlines in antiquotation output***From:*Daniel Schoepe

**References**:**[isabelle] Newlines in antiquotation output***From:*Daniel Schoepe

- Previous by Date: [isabelle] Newlines in antiquotation output
- Next by Date: Re: [isabelle] Newlines in antiquotation output
- Previous by Thread: [isabelle] Newlines in antiquotation output
- Next by Thread: Re: [isabelle] Newlines in antiquotation output
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list