In fact I wouldn't need a new overload; if I could just get the
pretty-printer to print the empty list as "NIL" I would be fine.
But I haven't been able to do that. How do you get the pretty-printer to
stop using the add_listform rule for NIL while retaining it for non-empty
lists?
I tried prefer_form_with_tok but it didn't work.
On Thu, Jul 24, 2014 at 3:47 PM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:
> The latter is how I've done this in the past.
>
> Michael
>
> > On 24 Jul 2014, at 22:16, "Ramana Kumar" <ramana.ku...@cl.cam.ac.uk>
> wrote:
> >
> > HOL's pretty-printer usually prints the empty list as "[]", which I
> believe is produced by two separate tokens (one for each bracket) via a
> "listform" parsing/printing rule.
> >
> > In LaTeX math mode (generated using HOL's math mode munger) "[]" does
> not look nice: it needs a bit of space inside. What would be the best
> approach to making the printer generate such space? Could I, perhaps,
> override the empty list (but not other lists) with a special token that I
> can then override to some custom LaTeX? Or perhaps there's a better way?
> >
> ------------------------------------------------------------------------------
> > Want fast and easy access to all the code in your enterprise? Index and
> > search up to 200,000 lines of code with a free copy of Black Duck
> > Code Sight - the same software that powers the world's largest code
> > search on Ohloh, the Black Duck Open Hub! Try it now.
> > http://p.sf.net/sfu/bds
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
>
> ________________________________
>
> The information in this e-mail may be confidential and subject to legal
> professional privilege and/or copyright. National ICT Australia Limited
> accepts no liability for any damage caused by this email or its attachments.
>
------------------------------------------------------------------------------
Want fast and easy access to all the code in your enterprise? Index and
search up to 200,000 lines of code with a free copy of Black Duck
Code Sight - the same software that powers the world's largest code
search on Ohloh, the Black Duck Open Hub! Try it now.
http://p.sf.net/sfu/bds
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
