No, the overload_on approach works. It works because the handling of list$NIL chooses the name "LaTeXNIL" for it, and this isn't then picked up by the concrete syntax phase (only "NIL" is).
Normal lists will print as per the list-form rule. Michael On 25/07/14 16:10, Ramana Kumar wrote: > I am already using a special "pretty-printing" theory when creating my munger, > but I still don't know what to put in it to change printing of the empty list. > (In your email you explained why all the code snippets you provided don't > work.) > > It sounds like there's no way to change how the empty list is printed without > removing the listform rule (and can it even be removed?), but of course I want > the listform rule for non-empty lists. > > I think the tiny-space idea sounds like too much of a special case. What we > would want is general mechanisms for overriding the printer's behaviour that > don't have to anticipate why we want to do it. > > If I understand correctly, what is missing is some way to give preference to > an > overload over a listform. > > > On Fri, Jul 25, 2014 at 3:22 AM, Michael Norrish <michael.norr...@nicta.com.au > <mailto:michael.norr...@nicta.com.au>> wrote: > > When the term list$NIL is encountered, the first phase of turning this > into a > string is to figure out which name to render it with. The overload data > structure says that "NIL" should be used. The concrete syntax grammar is > then > consulted for rules pertaining to NIL. The only rule it will find is the > list-form version, and this will be used. > > Unfortunately, if there is a list rule for a bare term (like NIL) it will > always > be used in preference to any other possible rules. So, even if you did > something like > > add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)), > fixity = Closefix, > paren_style = OnlyIfNecessary, > pp_elements = [TOK "fooNIL"], term_name = "NIL"}; > > it wouldn’t work, and you’d still get “[]”. Given the wordiness of the > above, > even if it worked, I’d have thought that > > val _ = overload_on("LaTeXNIL", ``[]``); > val _ = TeX_notation {hol = "LaTeXNil", TeX = ("\\ensuremath{[\,]}", > 2)}; > > would be preferable. You still need to do the analogue of the second > line above > for the first solution too. > > I take the point that nice LaTeX for [] would be preferable without > having to do > anything at all. > > One option might be to have the pretty-printing backends provide a > “tiny-space” > API point. All but the TeX backends would do nothing with this, but the > TeX > backend could generate a \, or whatever. The pretty-printer could then be > relied to generate a tiny-space every time two tokens followed each other > without interruption. Or perhaps the tiny-space would only appear > between > list-form delimiters. Or perhaps users could call for it explicitly in > grammar > rules... > > Another option would be to maintain a set of TeX deltas (accompanying > theories > as they were saved and loaded). These deltas could be overlaid on the > standard > grammar when TeX-pretty-printing was due to happen. This would allow > maximum > flexibility because the normal-use grammars wouldn’t get contaminated at > all, > and weird pretty-printing stuff could be kept in its own silo. You can > emulate > this a little at the moment by creating parallel PrettyPrinting theories > that > only get pulled in when creating a TeX munger. > > Michael > > > On 25/07/14 03:54, Ramana Kumar wrote: > > 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 <mailto:michael.norr...@nicta.com.au> > > <mailto:michael.norr...@nicta.com.au > <mailto: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 > <mailto:ramana.ku...@cl.cam.ac.uk> > > <mailto:ramana.ku...@cl.cam.ac.uk > <mailto: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 > <mailto:hol-info@lists.sourceforge.net> > <mailto:hol-info@lists.sourceforge.net > <mailto: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. > > ________________________________ > > 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 > ________________________________ 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
