The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/27/2015 08:16 PM, Jason Gross wrote:
> You can insert two linebreaks by guessing a value for the widest buffer
> your users will have, and insert that many spaces, like:
>
> fail 0 "aasdf" "
>                                           " "adsf".
>
> If you can accept extra quotations, and a possible %string if string_scope
> is closed, you can do
>
> Require Import Coq.Strings.String.
> Local Open Scope string_scope.
> Definition NEWLINE := String (Ascii.Ascii false true false true false false
> false false) EmptyString.
> Goal True.
>    let nl := (eval unfold NEWLINE in NEWLINE) in
>    fail 0 "asdf" nl "asdf".

OK - so I guess the answer is "no".

It's the age of Twitter.  All msgs should fit on 1 line.  GWTP, else TMI.

- J

> On Fri, Mar 27, 2015 at 6:52 PM, Jonathan Leivent 
> <jonikelee AT gmail.com>
> wrote:
>
> > Is there any way to compose a single fail message from multiple strings
> > and terms with explicit line breaks inserted at certain points?  I tried
> > "\n" (eg. below) and various direct ascii characters, but they all just
> > printed out without being interpreted as line breaks.  Also, putting the
> > fail args on separate lines doesn't change things.
> >
> >    fail 0 "mytactic failure:" term1 "\ndid not work with" term2
> >
> >
> > -- Jonathan