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
